Geometry of Synthesis Ⅲ Resource Management Through Type Inference

摘要

Geometry of Synthesis is a technique for compiling higher-level programming languages into digital circuits via their game semantic model. Ghica (2007) first presented the key idea, then Ghica and Smith (2010) gave a provably correct compiler into asynchronous circuits for Syntactic Control of Interference (SCI), an affine-typed version of Reynolds's Idealized Algol. Affine typing has the dual benefits of ruling out race conditions through the type system and having a finite-state game-semantic model for any term, which leads to a natural circuit representation and simpler correctness proofs. In this paper we go beyond SCI to full Idealized Algol, enhanced with shared-memory concurrency and semaphores (Ghica and Murawski, 2008). Compiling ICA proceeds in three stages. First, an intermediate type system called Syntactic Control of Concurrency (SCC), (Ghica et al., 2006) is used to statically determine "concurrency bounds" on all identifiers in the program. Then, a program transformation called serialization is applied to the program to translate it into an equivalent SCC program in which all concurrency bounds are set to the unit. Finally, the resulting program can be then compiled into asynchronous circuits using a slightly enhanced version of the GoS II compiler, which can handle assignable variables used in non-sequential contexts.