Comparing degrees of non-determinism in expression evaluation

Ian J. Hayes*, Alan Burns, Brijesh Dongol, Cliff B. Jones

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

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 languageEnglish
Pages (from-to)741-755
Number of pages15
JournalComputer journal
Volume56
Issue number6
Early online date5 Feb 2013
DOIs
Publication statusPublished - 1 Jun 2013

Keywords

  • concurrency
  • Non-deterministic expression evaluation
  • real-time programming
  • rely-guarantee
  • sampling logic

Cite this