Effect-Dependent Transformations for Concurrent Programs

TL;DR

This paper develops a denotational semantics for an abstract effect system in concurrent programming, enabling sound reasoning about program equivalences and transformations involving fine-grained concurrent data structures.

Contribution

It introduces a novel effect system based on abstract locations and game-based logical relations, validating transformations in concurrent programs that were previously unsound.

Findings

Proves soundness of effect-based program equivalences including parallelization.

Validates transformations involving concurrent data structures like Michael-Scott queues.

Enables reasoning about effects relative to abstract locations rather than physical memory.

Abstract

We describe a denotational semantics for an abstract effect system for a higher-order, shared-variable concurrent programming language. We prove the soundness of a number of general effect-based program equivalences, including a parallelization equation that specifies sufficient conditions for replacing sequential composition with parallel composition. Effect annotations are relative to abstract locations specified by contracts rather than physical footprints allowing us in particular to show the soundness of some transformations involving fine-grained concurrent data structures, such as Michael-Scott queues, that allow concurrent access to different parts of mutable data structures. Our semantics is based on refining a trace-based semantics for first-order programs due to Brookes. By moving from concrete to abstract locations, and adding type refinements that capture the possible side-effects of both expressions and their concurrent environments, we are able to validate many equivalences that do not hold in an unrefined model. The meanings of types are expressed using a game-based logical relation over sets of traces. Two programs $e_1$ and $e_2$ are logically related if one is able to solve a two-player game: for any trace with result value $v_1$ in the semantics of $e_1$ (challenge) that the player presents, the opponent can present an (response) equivalent trace in the semantics of $e_2$ with a logically related result value $v_2$.