Synchronized Shared Memory and Procedural Abstraction: Towards a Formal Semantics of Blech

Traditional imperative synchronous programming languages heavily rely on a strict separation between data memory and communication signals. Signals can be shared between computational units but cannot be overwritten within a synchronous reaction cycle. Memory can be destructively updated but cannot be shared between concurrent threads. This incoherence makes traditional imperative synchronous languages cumbersome for the programmer. The recent definition of sequentially constructive synchronous languages offers an improvement. It removes the separation between data memory and communication signals and unifies both through the notion of clock synchronised shared memory. However, it still depends on global causality analyses which precludes procedural abstraction. This complicates reuse and composition of software components. This paper shows how procedural abstraction can be accommodated inside the sequentially constructive model of computation. We present the Sequentially Constructive Procedural Language (SCPL) and its semantic theory of policy-constructive synchronous processes. SCPL supports procedural abstractions using policy interfaces to ensure that procedure calls are memory safe, wait-free and their scheduling is determinate and causal. At the same time, a policy interface constrains the level of freedom for the implementation and subsequent refactoring of a procedure. As a result, policies enable separate compilation and composition of procedures. We present our extensions abstractly as a formal semantics for SCPL and motivate it concretely in the context of the open-source, embedded, real-time language Blech.