Research output: Contribution to journal › Article
Journal | Computer journal |
---|---|
Date | E-pub ahead of print - 5 Feb 2013 |
Date | Published (current) - 1 Jun 2013 |
Issue number | 6 |
Volume | 56 |
Number of pages | 15 |
Pages (from-to) | 741-755 |
Early online date | 5/02/13 |
Original language | English |
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.
Find related publications, people, projects, datasets and more using interactive charts.