![]() |
![]() |
University of Birmingham > Talks@bham > Lab Lunch > Resource management via type inference in a hardware compiler
Resource management via type inference in a hardware compilerAdd to your list(s) Download to your calendar using vCal
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:
Note that ex-directory lists are not shown. |
Other lists'Roles' Postgraduate Gender and Sexuality Network Discussion Cold Atoms Cold atomsOther talksNon-stationary quantum many-body dynamics Modelling nanoplasmonic hot carrier generation Medical Image Analysis with Data-efficient Learning Haptic human-robot communication Uniqueness of the phase transition in many-dipole cavity QED systems Rigidity of symmetry-forced frameworks |