Possible values: exploring a concept for concurrency

TL;DR

This paper introduces a 'possible values' notation for reasoning about shared variables in concurrent programs, enhancing specification clarity and compositional reasoning without auxiliary variables.

Contribution

It proposes a novel 'possible values' approach to improve reasoning about interference in shared-variable concurrency, avoiding auxiliary variables.

Findings

Provides a clear specification method for interference

Enhances compositional reasoning in concurrent programs

Reduces reliance on auxiliary variables

Abstract

An important issue in concurrency is interference. This issue manifests itself in both shared-variable and communication-based concurrency --- this paper focusses on the former case where interference is caused by the environment of a process changing the values of shared variables. Rely/guarantee approaches have been shown to be useful in specifying and reasoning compositionally about concurrent programs. This paper explores the use of a "possible values" notation for reasoning about variables whose values can be changed multiple times by interference. Apart from the value of this concept in providing clear specifications, it offers a principled way of avoiding the need for some auxiliary (or ghost) variables whose unwise use can destroy compositionality.