  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.
