A Denotational Semantics for Communicating Unstructured Code

TL;DR

This paper develops a compositional denotational semantics for unstructured low-level code with communication, enabling formal reasoning and verification of such code by structuring it and capturing communication via finite traces.

Contribution

It introduces a novel compositional semantics for unstructured code that incorporates communication, based on fixed points and trace semantics, facilitating formal verification.

Findings

Semantics based on least fixed points for unstructured code

Communication modeled using finite trace semantics

Foundation for a proof calculus combining code and communication

Abstract

An important property of programming language semantics is that they should be compositional. However, unstructured low-level code contains goto-like commands making it hard to define a semantics that is compositional. In this paper, we follow the ideas of Saabas and Uustalu to structure low-level code. This gives us the possibility to define a compositional denotational semantics based on least fixed points to allow for the use of inductive verification methods. We capture the semantics of communication using finite traces similar to the denotations of CSP. In addition, we examine properties of this semantics and give an example that demonstrates reasoning about communication and jumps. With this semantics, we lay the foundations for a proof calculus that captures both, the semantics of unstructured low-level code and communication.