Dataflow synthesis and verification for parallel object-oriented programming languages

Thesis (M.Eng.)--Memorial University of Newfoundland, 2011. Engineering and Applied Science Bibliography: leaves 93-97. 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...

Full description

Bibliographic Details
Main Author: Wu, Shuang, 1985-
Other Authors: Memorial University of Newfoundland. Faculty of Engineering and Applied Science
Format: Thesis
Language:English
Published: 2011
Subjects:
Online Access:http://collections.mun.ca/cdm/ref/collection/theses5/id/11829
Description
Summary:Thesis (M.Eng.)--Memorial University of Newfoundland, 2011. Engineering and Applied Science Bibliography: leaves 93-97. 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.