Possible values: exploring a concept for concurrency
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.
Cite
@article{arxiv.1601.02132,
title = {Possible values: exploring a concept for concurrency},
author = {Cliff B. Jones and Ian J. Hayes},
journal= {arXiv preprint arXiv:1601.02132},
year = {2016}
}