Possible values: Exploring a concept for concurrency

- A new concept is introduced for use in specifying and reasoning about concurrent programs.
- Use of the notation for “possible values” fits well with Rely/Guarantee methods.
- The use of the notation and inference rules is illustrated on Simpson's “four-slot” algorithm.

An important issue in concurrency is interference. This issue manifests itself in both shared-variable and communication-based concurrency - this paper focuses 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.