Compilation of imperative synchronous programs with refined clocks

To overcome over-synchronization in synchronous programs, we recently introduced clock refinement to our synchronous programming language Quartz. This extension basically allows programmers to refine reaction steps into smaller internal computation steps while maintaining the external behavior. In this paper, we consider the compilation of the extended Quartz programs to synchronous guarded actions. To this end, we first define an intermediate language supporting multiple clocks based on synchronous guarded actions which is the target of the front-end of the compiler and the source of back-end tools that perform efficient analysis and synthesis procedures. We moreover present a compilation scheme to translate the extended Quartz programs to the new intermediate language. We discuss important design considerations and illustrate our approach with the help of some small examples.