Comparing Models of Nondeterministic Expression Evaluation
Ian J. Hayes, Alan Burns, Brijesh Dongol and Cliff B. Jones
Expression evaluation in programming languages is normally deterministic; however, if expressions involve variables that are being modified by the environment of the process during their evaluation, the result of the evaluation can be nondeterministic. Two common cases where this occurs are in concurrent programs where processes share variables and real-time programs that interact to monitor and/or control their environment. In these contexts, while any particular evaluation of an expression gives a single result, there is a range of possible results that could be returned depending on the relative timing of modification of variables by the environment and their access within expression evaluation. Hence to model the semantics of expression evaluation one can use the set of possible values the expression evaluation could return. This paper considers three views of interpreting expressions nondeterministically. The paper formalises the three approaches, highlights different properties satisfied by the approaches, relates the approaches and explores conditions under which they coincide. Furthermore, a link is made to a new notation used in reasoning about interference.
BibTex Entry
@techreport{Hayes2011,
author = {Ian J. Hayes and Alan Burns and Brijesh Dongol and Cliff B. Jones},
institution = {Newcastle University},
month = {September},
number = {CS-TR-1273},
title = {Comparing Models of Non\-deterministic Expression Evaluation},
year = {2011}
}