Dataflow synthesis and verification for parallel object-oriented programming languages

Abstract

The HARPO project aims to develop a methodology to generate and verify hardware configurations from a high level object-oriented programming language. Specifically, the compiler of a high-level object-oriented programming language, HARPO/L (standing for HARdware Parallel Objects Language), outputs hardware configurations that are mappable to a coarse-grained reconfigurable architecture (CGRA) system. -- This thesis develops a data flow synthesis method, which is a critical component in the middle-module of the HARPO/L compiler. This method is extendable to most other high-level parallel object-oriented programming languages. -- In addition, this thesis proposes an automatic verification system for HARPO/L. An algorithm to compute weakest liberal precondition of parallel compositions, which fills the gap between verification of programming languages with parallel compositions and state-of-art automatic verification approaches, is introduced. This algorithm also helps verifying the absence of data race and the absence of deadlock, and has good interplay with grainless semantics.