A Syntactic Model of Mutation and Aliasing

TL;DR

This paper introduces a syntactic memory model for imperative languages that simplifies reasoning about aliasing and memory isolation by embedding memory directly into program syntax, enabling easier analysis and implementation.

Contribution

It presents a novel syntactic approach to modeling memory and aliasing in imperative languages, replacing auxiliary structures with embedded syntax for improved reasoning.

Findings

Syntactic model encodes memory as part of program syntax.

Capsules represent isolated memory portions, facilitating safe movement.

Model can be encoded into conventional semantic models for implementation.

Abstract

Traditionally, semantic models of imperative languages use an auxiliary structure which mimics memory. In this way, ownership and other encapsulation properties need to be reconstructed from the graph structure of such global memory. We present an alternative "syntactic" model where memory is encoded as part of the program rather than as a separate resource. This means that execution can be modelled by just rewriting source code terms, as in semantic models for functional programs. Formally, this is achieved by the block construct, introducing local variable declarations, which play the role of memory when their initializing expressions have been evaluated. In this way, we obtain a language semantics which directly represents at the syntactic level constraints on aliasing, allowing simpler reasoning about related properties. To illustrate this advantage, we consider the issue, widely studied in the literature, of characterizing an isolated portion of memory, which cannot be reached through external references. In the syntactic model, closed block values, called "capsules", provide a simple representation of isolated portions of memory, and capsules can be safely moved to another location in the memory, without introducing sharing, by means of "affine' variables. We prove that the syntactic model can be encoded in the conventional one, hence efficiently implemented.