Abstract
Expression evaluation in programming languages is normally assumed to be deterministic; however, if an expression involves variables that are being modified by the environment of the process during its evaluation, the result of the evaluation can be non-deterministic. Two common scenarios in which this occurs are concurrent programs within which processes share variables and real-time programs that interact to monitor and/or control their environment. In these contexts, although any particular evaluation of an expression gives a single result, there is a range of possible values that could be returned depending on the relative timing between modification of a variable by the environment and its access within the expression evaluation. To compare the semantics of non-deterministic expression evaluation, one can use the set of possible values the expression evaluation could return. This paper formalizes three approaches to non-deterministic expression evaluation, highlights their commonalities and differences, shows the relationships between the approaches and explores conditions under which they coincide. Modal operators representing that a predicate holds for all possible evaluations and for some possible evaluation are associated with each of the evaluation approaches, and the properties and relationships between these operators are investigated. Furthermore, a link is made to a new notation used in reasoning about interference.
Original language | English |
---|---|
Pages (from-to) | 741-755 |
Number of pages | 15 |
Journal | Computer journal |
Volume | 56 |
Issue number | 6 |
Early online date | 5 Feb 2013 |
DOIs | |
Publication status | Published - 1 Jun 2013 |
Keywords
- concurrency
- Non-deterministic expression evaluation
- real-time programming
- rely-guarantee
- sampling logic