A Formal Semantics of Clock Refinement in Imperative Synchronous Languages

The synchronous model of computation divides the execution of a program into an infinite sequence of socalled macro steps, which are further divided into finitely many micro steps. Since all threads of a program are forced to run in lockstep, programmers have no means to express the independence of parallel threads, which leads to a phenomenon called over-synchronization. In this paper, we therefore propose a generalization of the synchronous model of computation by means of refined clocks, which divide a macro step into finer grained steps that themselves consist of micro steps. In particular, we present a structural operational semantics of subclocks and prove that the internal asynchrony given by subclocks still preserves input/output determinism.

• Type: Journal
• Year: 2010
• Where: ACSD
• Authors: Mike Gemunde, Jens Brandt, Klaus Schneider
• Keywords: ACSD 2010, Hardware, Macro Step, Micro Steps, Synchronous Model