Dataflow synthesis and verification for parallel object-oriented programming languages

Wu, Shuang (2011) Dataflow synthesis and verification for parallel object-oriented programming languages. Masters thesis, Memorial University of Newfoundland.

[English] PDF - Accepted Version Available under License - The author retains copyright ownership and moral rights in this thesis. Neither the thesis nor substantial extracts from it may be printed or otherwise reproduced without the author's permission. Download (9MB)

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.

Actions (login required)

View Item