Title
Synchronized Shared Memory and Procedural Abstraction: Towards a Formal Semantics of Blech
Abstract
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.
Year
DOI
Venue
2020
10.1109/FDL50818.2020.9232942
2020 Forum for Specification and Design Languages (FDL)
Keywords
DocType
ISSN
synchronous programming,clock-synchronised shared memory,procedural abstraction,operational semantics
Conference
1636-9874
ISBN
Citations 
PageRank 
978-1-7281-8929-1
1
0.42
References 
Authors
8
4
Name
Order
Citations
PageRank
Friedrich Gretz1664.49
Franz-Josef Grosch210.42
Michael Mendler331434.60
Stephan Scheele4174.36