On the compositionality of round abstraction

Abstract

We revisit a technique called round abstraction as a solution to the problem of building low-latency synchronous systems from asynchronous specifications. We use a trace-semantic setting akin to Abramsky's Interaction Categories, which is also a generalisation of pointer-free game semantic models. We define partial and total correctness for round abstraction relative to composition and note that in its most general case, round abstraction can lead to incorrect behaviour. We then identify sufficient properties to guarantee partially correct composition. Finally, we propose a framework for round abstraction that is totally correct when applied to asynchronous behaviours. We apply this procedure to the Geometry of Synthesis, a technique for compiling higher-order imperative programming languages into digital circuits using game semantics. © 2010 Springer-Verlag.