Resource management via type inference in a hardware compiler

Add to your list(s) Download to your calendar using vCal

• Alex Smith
• Tuesday 05 October 2010, 12:00-13:00
• CS 124.

If you have a question about this talk, please contact Dan Ghica.

Geometry of Synthesis is a technique for compiling higher-level programming languages into digital circuits via their game semantic model. Previous work presented the key idea and a provably correct compiler into asynchronous circuits in the context of the language 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.

Compiling ICA proceeds in three stages. First, an intermediate type system called Syntactic Control of Concurrency is used to statically determine ``concurrency bounds’’ on all identifiers in the program. Then, a program transformation 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.

[Paper to appear in POPL 2011 ]

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• CS 124
• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Lab Lunch
• Theoretical computer science seminar

Note that ex-directory lists are not shown.