11institutetext:  Department of Informatics, University of Bergen, Norway
11email<EMAIL_ADDRESS>22institutetext: Department of Computer Science,
Technische Universität Darmstadt, Germany
22email<EMAIL_ADDRESS>33institutetext: CNRS, Inria, LIP, Univ
Lyon, EnsL, UCBL, France
33email<EMAIL_ADDRESS>44institutetext: Department of Informatics,
University of Oslo, Norway
44email<EMAIL_ADDRESS>55institutetext: Department of
Computing, Western Norway University of Applied Sciences, Norway
55email<EMAIL_ADDRESS>
# LAGC Semantics of Concurrent Programming Languages

Crystal Chang Din 11 Reiner Hähnle 22 Ludovic Henrio 33 Einar Broch Johnsen 44
Ka I Pun 55 S. Lizeth Tapia Tarifa 44

###### Abstract

Formal, mathematically rigorous programming language semantics are the
essential prerequisite for the design of logics and calculi that permit
automated reasoning about concurrent programs. We propose a novel modular
semantics designed to align smoothly with program logics used in deductive
verification and formal specification of concurrent programs. Our semantics
separates local evaluation of expressions and statements performed in an
abstract, symbolic environment from their composition into global
computations, at which point they are concretised. This makes incremental
addition of new language concepts possible, without the need to revise the
framework. The basis is a generalisation of the notion of a program trace as a
sequence of evolving states that we enrich with event descriptors and trailing
continuation markers. This allows to postpone scheduling constraints from the
level of local evaluation to the global composition stage, where well-
formedness predicates over the event structure declaratively characterise a
wide range of concurrency models. We also illustrate how a sound program logic
and calculus can be defined for this semantics.

##  1 Introduction

We propose a trace semantics that scales flexibly to a range of concurrent,
imperative programming paradigms, as found, for example, in C, Java, ProMeLa
[44], Actors [41], or Active Objects [22]. Specifically, given a program $P$,
running on a collection of communicating processors or cores, we want to
obtain the set of all global system traces that $P$ can produce starting from
some initial state. Our overall goal is to provide a semantics that aligns
well with contract-based deductive verification [35]. To this end, it is
essential that the semantics cleanly separates local computations (one
statement on one core) from global ones; i.e., there must be a suitable notion
of _composition_ that can generate the global traces from the local ones. It
is known [16, 58] that compositionality in denotational semantics shifts the
flavour of the semantics in the direction of operational semantics [64], by
transitioning from state transformers [42, 9] to traces of execution states
[39, 17, 15] or communication events [21, 43, 48, 26]. We propose a hybrid
notion of trace that combines states and events, and show that the ensuing
semantic framework is well-suited to compositionally capture different forms
of concurrency for imperative languages.

The envisaged semantics should also be _modular_ in the following sense: it
must be possible to support a new language construct without the need to
revise the whole framework. Ideally, there is a single evaluation rule for
each construct of the target language that can be applied _independently_ from
all other rules: the recursive call to evaluate subsequent statements is not
inside the semantic evaluation of each statement. This is not only a good
match with deductive verification rules of program logics [35], but also with
formal specification languages for concurrent programs that have a trace
semantics [65, 12, 27, 67, 51].

A trace semantics for a given target language, satisfying the requirements
sketched above, can be defined in three phases:

  1. 1.

Declare _local_ evaluation rules for each syntax construct of the target
language.

  2. 2.

Declare _composition_ rules that combine local evaluation and process creation
into global traces. Scheduling is expressed declaratively as well-formedness
constraints over traces.

  3. 3.

Define the _generation_ of all global traces with the help of the composition
rules from a suitable initial configuration.

To achieve the desired degree of modularity, we generalise the standard notion
of a program trace [45], i.e. a sequence of evolving system configurations,
starting in some initial state. We make two generalisations. The first is that
local states $\sigma$ can be abstract. This means the value $\sigma(x)$ of a
memory location $x$ is permitted to be unspecified. One can think of an
abstract value $\sigma(x)$ as a Skolem constant $x_{0}$ whose interpretation
is determined by an external context. Alternatively, think of _symbolic
execution_ [19, 54], where the value of a memory location $x$ may be a
_symbolic_ term $x_{0}$ representing an unknown value. States containing
abstract values are called _symbolic_ , otherwise they are called _concrete_.

Symbolic states allow us to evaluate local code independently of its call
context. For example, when evaluating the semantics of a statement $s$ that
receives a message from another process, then the value of that message cannot
possibly be known independently of the call context. In this case, the local
evaluation of $s$ can be expressed in a trace with symbolic states. These
symbolic states are _concretised_ when the global context of the local
computations (here, the sender) is resolved, i.e. in the composition rules
during phase (2) above. Hence, the resulting global traces are concrete. Thus,
the name of our semantic framework: _locally abstract, globally concrete_
(LAGC).

The second generalisation of traces concerns _scheduling_ : concurrency models
differ in the exact locations at which a local computation can be interrupted
(aka preempted) and how exactly the computation is continued afterwards, i.e.
which scheduling decision is taken next. To achieve maximum modularity, we do
not build scheduling into a fixed set of rules. Instead, we use _continuation
markers_ to specify when scheduling and preemption is possible.

As a result, local traces are not merely abstract, but as well contain
_events_ used in the composition rules as interaction points. With the event
mechanism, various concurrency models can be defined easily in two parts:
first, ensure that local evaluation rules generate suitable synchronisation
events. Second, define a _well-formedness_ predicate on concrete traces
restricting the global traces that can be generated to those reflecting the
targeted concurrency model. Now it is sufficient to add the well-formedness
predicate as a premise to each composition rule. Events turn out to be a
flexible and intuitive mechanism, which can be used to express a range of
dependencies between processes beyond synchronous communication (for example,
object generation).

An LAGC-style trace semantics was pioneered for the active object language ABS
[27]. Here we show that, due to its modularity, LAGC semantics constitutes a
general _semantic framework_ for a wide range of concurrent programming
models: it is easy to add new syntactic constructs and to accommodate
different concurrency paradigms. We will demonstrate this as follows: starting
with a simple WHILE-language, we define LAGC semantics for an increasingly
complex series of languages by successively adding new features, sequential as
well as parallel ones. In the end we cover a representative set of language
features and concurrency models and instantiate our semantic framework to two
quite different concurrent programming languages.

The paper is organised as follows: In Section 2 we set up the formal framework
that the LAGC semantics is based upon. As explained above, we need symbolic
states and traces that may contain abstract values for memory locations. We
also need a concretisation operator that instantiates a symbolic trace to
match a concrete context. In addition, we equip traces with states and
continuation markers. Section 3 introduces the LAGC framework along phases
(1)–(3) for a WHILE-language. We substantiate the claim made above, that an
LAGC semantics is a good match for deductive verification calculi, by defining
in Section 4 a program logic for WHILE with a concise soundness proof. In
Section 5, we gradually extend the semantics to local parallelism (with
atomicity), local memory, and procedure calls. In Section 6, we take the step
to multiple processors that send and receive messages among each other. We
show that a wide range of communication patterns can be intuitively and
declaratively characterised via well-formedness, including synchronous and
asynchronous communication, bounded and unbounded FIFO, as well as causality.
Section 7 instantiates the LAGC framework to the rather different concurrency
models found in the languages ProMeLa and ABS, respectively. For the latter,
we need to add objects and futures, as well as to change the interleaving
semantics, which turns out to be easily possible. Related work is discussed in
Section 8, while Section 9 considers future directions for work and concludes.

##  2 Basics

###  2.1 States

We assume given standard basic types, including integers, Booleans and process
identifiers, with standard value domains and associated operators. In
addition, we allow starred expressions, representing unknown, _symbolic_
values.

$\begin{array}[t]{r@{\hspace{2pt}}r@{\hspace{2pt}}l}x\in\mathit{Var}\hskip
2.0&::=\hskip 2.0&\textit{identifier}\\\ v\in\mathit{Val}\hskip 2.0&::=\hskip
2.0&\mathrm{t\\!t}\mid\mathrm{f\\!f}\mid 0\mid 1\mid...\\\
op\in\mathit{Op}\hskip 2.0&::=\hskip 2.0&==\leavevmode\nobreak\
\mid\leavevmode\nobreak\ <\leavevmode\nobreak\ \mid\leavevmode\nobreak\
>\leavevmode\nobreak\ \mid\leavevmode\nobreak\ \leq\leavevmode\nobreak\
\mid\leavevmode\nobreak\ \geq\leavevmode\nobreak\
\mid\lit*{+}\mid\lit*{-}\mid\lit*{*}\mid\lit*{/}\mid\ldots\\\
e\in\mathit{Exp}\hskip 2.0&::=\hskip 2.0&x\mid v\mid e\,op\,e\\\ \
se\in\mathit{Sexp}\hskip 2.0&::=\hskip 2.0&e\mid\ast\end{array}$

Figure 1: Syntax of expressions.

######  Definition 1 (Variables, Values, (Starred) Expressions)

Let $\mathit{Var}$ be a set of program variables, $\mathit{Val}$ a set of
values, and $\mathit{Op}$ a set of operators, with typical elements $x$, $v$,
and $op$, respectively. The sets $\mathit{Val}$ and $\mathit{Op}$ include the
values and operators of the basic types (see Figure 1). The set $\mathit{Exp}$
contains expressions, with typical element $e$, obtained from variables,
values, and by applying operators to expressions. The set $Sexp$ contains
starred expressions, with typical element $se$, obtained by extending
expressions with an additional symbol $\ast$.

We assume that all expressions are well-typed; i.e., in expressions, operators
are only applied to subexpressions which can be reduced to values of
appropriate types. Let $\>\underline{op}\>$ denote an evaluation function for
the operators $\mathit{op}$ defined over the values of the basic types, such
that $v\>\>\underline{op}\>\>v^{\prime}$ is a value in the basic types. A
Boolean expression is an expression that evaluates to a Boolean value when its
arguments are values of the basic types, and similarly for expressions of
other basic types. Overline notation is used for lists of different syntactic
categories; e.g., $\overline{v}$ and $\overline{e}$ represent lists of values
and expressions, respectively. Let $\operatorname{vars}(e)$ denote the set of
variables in an expression $e$, which has a straightforward inductive
definition.

We now define computation states. Usually, states are mappings from variables
to concrete values. To permit _symbolic_ expressions (i.e., expressions
containing variables) occurring as _values_ in states, the starred expression
$\ast$ is used to represent a value for symbolic variables that cannot be
further evaluated. The $\ast$ symbol does not occur in programs, it is part of
the semantic domain.

######  Definition 2 (Symbolic State, State Update)

A _symbolic state_ $\sigma$ is a partial mapping

$\sigma:\mathit{Var}\to\mathit{Sexp}$

from variables to starred expressions. The notation $\sigma[x\mapsto se]$
expresses the _update_ of state $\sigma$ at $x$ with expression $se$:

$\sigma[x\mapsto se](y)=\left\\{\begin{array}[]{ll}se&x=y\\\ \sigma(y)&x\neq
y\ .\end{array}\right.$

In a symbolic state, a _symbolic variable_ is defined as a variable bound to
an unknown value, represented by the starred expression $\ast$. Symbolic
variables play a different role than ordinary variables: they act as
parameters, relative to which a local computation is evaluated. To distinguish
them syntactically, we adopt the convention of using capital letters for
symbolic variables as much as possible. Note that the set of symbolic and non-
symbolic variables are not two distinct categories and a variable that is
symbolic can become non-symbolic after substitution (see Example 2 below).

######  Definition 3 (Symbolic Variable)

_Symbolic variables_ in a state $\sigma$ are variables mapped to $\ast$:

$\operatorname{symb}(\sigma)=\\{X\in\mathit{Var}\mid\,\sigma(X)=\ast\\}\ .$

We will also need the concept of the extension of a state:

######  Definition 4 (State Extension)

We say that a state $\sigma^{\prime}$ _extends_ a state $\sigma$ if  (i)
$\operatorname{dom}(\sigma)\subseteq\operatorname{dom}(\sigma^{\prime})$and
(ii) $\sigma(x)=\sigma^{\prime}(x)$for all $x\in\operatorname{dom}(\sigma)$.
We overload the subset symbol and write $\sigma\subseteq\sigma^{\prime}$.

###### Example 1

Consider a state $\sigma_{0}=[x_{0}\mapsto
Y_{0}+w_{0},\,Y_{0}\mapsto\ast,\,w_{0}\mapsto 42,\,x_{1}\mapsto Y_{1}]$.
Observe that (1) the expressions in the range of $\sigma_{0}$ can be
simplified and (2) there are dangling references, such as $Y_{1}$, not in the
domain of $\sigma_{0}$.

The example shows that symbolic states are slightly too general for our
purpose, motivating the following definition, which constrains the variables
that may occur in value expressions of states to symbolic variables:

######  Definition 5 (Well-Formed State)

A state $\sigma$ is _well-formed_ if it fulfils the following condition:

$\\{x\in\operatorname{vars}(\sigma(y))\mid
y\in\operatorname{dom}(\sigma)\\}\subseteq\operatorname{symb}(\sigma)\enspace.$

A well-formed state $\sigma$ is _concrete_ if
$\operatorname{symb}(\sigma)=\\{\\}$. For a concrete, well-formed state
$\sigma$ and all $x\in\operatorname{dom}(\sigma)$, there is a value $v$ such
that $\sigma(x)=v$.

###### Example 2

The state $\sigma_{0}$ in Example 1 can be turned into a well-formed state
$\sigma_{1}$ by simplifying the expression $Y_{0}+w_{0},$ and binding $Y_{1}$
to a star, obtaining $\sigma_{1}=[x_{0}\mapsto
Y_{0}+42,\,Y_{0}\mapsto\ast,\,w_{0}\mapsto 42,\,x_{1}\mapsto
Y_{1},\,Y_{1}\,\mapsto\ast]$. We have that $\sigma_{1}=\sigma_{0}[x_{0}\mapsto
Y_{0}+42,\,Y_{1}\mapsto\ast]$ and
$\operatorname{symb}(\sigma_{1})=\\{Y_{0},\,Y_{1}\\}$. Let
$\sigma_{2}=\sigma_{1}[Y_{0}\mapsto 3,\,Y_{1}\mapsto 2]$. After
simplification, $\sigma_{2}$ is a concrete, well-formed state that can be
written as $\sigma_{2}=[x_{0}\mapsto 45,\,Y_{0}\mapsto 3,\,w_{0}\mapsto
42,\,x_{1}\mapsto 2,\,Y_{1}\mapsto 2]$.

Henceforth, all states are assumed to be well-formed. _We always assume states
to be simplified by propagation of concrete values_ , similar to $\sigma_{2}$
in Example 2, otherwise non-symbolic variables might occur as values. Symbolic
states, i.e. states with symbolic variables, are close to states in symbolic
execution as used in path exploration [33], but simplified and with an
additional restriction (Definition 11 below).

###  2.2 Evaluation

The evaluation of expressions in the context of a symbolic state reduces known
variables to their values and keeps the symbolic variables inside the
expression, reducing an expression as much as currently possible. The
evaluation function is defined as follows:

######  Definition 6 (Evaluation Function)

Let $\sigma$ be a symbolic state. The evaluation function
$\mathrm{val}_{\sigma}:Exp\rightarrow Exp$ for expressions in the context of
$\sigma$ is defined inductively:

$\begin{array}[]{r@{\,}c@{\,}ll}\mathrm{val}_{\sigma}(x)&=&\left\\{\begin{array}[]{ll}x&\text{
if }\sigma(x)=*\\\ \sigma(x)&\text{ otherwise}\end{array}\right.\\\
\mathrm{val}_{\sigma}(v)&=&v\\\
\mathrm{val}_{\sigma}(e_{1}\>op\>e_{2})&=&\left\\{\begin{array}[]{ll}\mathrm{val}_{\sigma}(e_{1})\>\underline{op}\>\mathrm{val}_{\sigma}(e_{2})&\text{
if }\mathrm{val}_{\sigma}(e_{1})\in\mathit{Val}\text{ and
}\mathrm{val}_{\sigma}(e_{2})\in\mathit{Val}\\\\[2.15277pt]
\mathrm{val}_{\sigma}(e_{1})\>op\>\mathrm{val}_{\sigma}(e_{2})&\text{
otherwise}\end{array}\right.\end{array}$

In the following we will ensure that
$\operatorname{vars}(e)\subseteq\operatorname{dom}(\sigma)$ holds, such that
$\mathrm{val}_{\sigma}$ is a total function.

###### Example 3

Using state $\sigma_{1}$ of Example 2, we evaluate
$\mathrm{val}_{\sigma_{1}}(x_{0}+Y_{0}+Y_{1})=(Y_{0}+42)+Y_{0}+Y_{1}$.

Let $\mathrm{val}_{\sigma}(\overline{e})$ denote the element-wise application
of the evaluation function to all expressions in the list $\overline{e}$, and
likewise for sets.

###  2.3 Traces and Events

Traces are sequences over states and structured events. The presence of events
makes it easy to ensure global properties of traces via well-formedness
conditions over events. Since states may be symbolic, traces will be symbolic
as well and it is necessary to constrain traces by symbolic path conditions.
We start with a general definition of events. Their specific structure will be
added later.

######  Definition 7 (Event Marker)

Let $\textit{ev}(\overline{e})$ be an _event marker_ over expressions
$\overline{e}$.

######  Definition 8 (Path Condition)

A _path condition_ $pc$ is a finite set of Boolean expressions. If $pc$
contains no variables, then we can assume it to be fully evaluated; i.e. it is
either $\emptyset$, $\\{\mathrm{f\\!f},\,\mathrm{t\\!t}\\}$,
$\\{\mathrm{f\\!f}\\}$, or $\\{\mathrm{t\\!t}\\}$. A fully evaluated path
condition is _consistent_ if and only if it does not contain $\mathrm{f\\!f}$.

For any concrete state $\sigma$, $\mathrm{val}_{\sigma}(pc)$ is a path
condition with no variables that can be fully evaluated.

######  Definition 9 (Conditioned Symbolic Trace)

A _symbolic trace_ $\tau$ is defined co-inductively by the following rules
($\varepsilon$ denotes the empty trace):

$\begin{array}[]{l@{\;::=\;}l}\tau&\varepsilon\leavevmode\nobreak\
|\leavevmode\nobreak\ \tau\curvearrowright t\\\ t&\sigma\leavevmode\nobreak\
|\leavevmode\nobreak\ \textit{ev}(\overline{e})\end{array}$

A _conditioned symbolic trace_ has the form $pc\triangleright\tau$, where $pc$
is a path condition and $\tau$ is a symbolic trace. If $pc$ is consistent, we
simply write $\tau$ for $pc\triangleright\tau$.

Traces can be finite or infinite. For simplicity, let $\langle\sigma\rangle$
denote the _singleton trace_ $\varepsilon\curvearrowright\sigma$.
_Concatenation_ of two traces $\tau_{1}$, $\tau_{2}$ is written as
$\tau_{1}\cdot\tau_{2}$ and only defined when $\tau_{1}$ is finite. The final
state of a non-empty, finite trace $\tau$ is selected with
$\mathrm{last}(\tau)$, the first state of a non-empty trace $\tau$ with
$\mathrm{first}(\tau)$.

###### Example 4

Continuing Example 2, we define a conditioned symbolic trace
$pc_{0}\triangleright\tau_{0}=\\{Y_{0}>Y_{1}\\}\triangleright\langle\sigma_{1}\rangle\curvearrowright\sigma_{1}[x_{0}\mapsto
17]$.

##### Sequential Composition

It is important that traces can semantically model the sequential composition
of program statements. Assume that $\tau_{1}$ is a trace of a statement $r$
and $\tau_{2}$ a trace of another statement $s$. To obtain the trace
corresponding to the sequential composition of $r$ and $s$, the traces
corresponding to $r$ and $s$ should be concatenated, but the last state of the
first trace and the first state of the second trace are generally identical.
We generalize such a concatenation in case the states are not exactly the
same: to concatenate two traces $\tau_{1}$ and $\tau_{2}$ the first state of
$\tau_{2}$ should be an extension of the last state of $\tau_{1}$, but the
resulting trace should only contain the largest of the two states. This
motivates the _semantic chop_ $\mathbin{\ast\ast}$ on traces (following [60],
who in turn were inspired by interval temporal logic [36]):

######  Definition 10 (Chop on Traces)

Let $pc_{1},pc_{2}$ be path conditions and $\tau_{1},\,\tau_{2}$ be symbolic
traces, and assume that $\tau_{1}$ is a non-empty, finite trace. The semantic
chop
$(pc_{1}\triangleright\tau_{1})\mathbin{\ast\ast}(pc_{2}\triangleright\tau_{2})$
is defined as follows:

$(pc_{1}\triangleright\tau_{1})\mathbin{\ast\ast}(pc_{2}\triangleright\tau_{2})=(pc_{1}\cup
pc_{2})\triangleright\tau\cdot\tau_{2}\leavevmode\nobreak\
\mbox{where}\leavevmode\nobreak\ \tau_{1}=\tau\curvearrowright\sigma,\
\tau_{2}=\langle\sigma^{\prime}\rangle\cdot\tau^{\prime}\leavevmode\nobreak\
\mbox{and}\leavevmode\nobreak\ \sigma\subseteq\sigma^{\prime}\ .$

For infinite and empty traces $\tau_{1}$, the chop operator is undefined.
Whenever the final state of the first trace cannot be extended to the first
state of the second trace, the operator is undefined.

The definition can be specialised to traces without path conditions in the
obvious way: $\tau_{1}\mathbin{\ast\ast}\tau_{2}$ is
$(\emptyset\triangleright\tau_{1})\mathbin{\ast\ast}(\emptyset\triangleright\tau_{2})$.

##### Traces with Events.

Events will be uniquely associated with the state in a trace at which they
occurred. The events do not update the values in a state, but they may extend
a state with fresh symbolic variables. To this aim, an event
$\textit{ev}(\overline{e})$ is inserted into a trace after a state $\sigma$
and the state is then augmented by a set $\overline{V}$ of symbolic variables.
The notation we use for this operation is an _event trace_
$\textit{ev}_{\sigma}^{\overline{V}}({\overline{e}})$ of length three:

$\textit{ev}_{\sigma}^{\overline{V}}({\overline{e}})=\langle\sigma\rangle\curvearrowright\textit{ev}(\mathrm{val}_{\sigma^{\prime}}(\overline{e}))\curvearrowright\sigma^{\prime}\
\text{ where }\sigma^{\prime}=\sigma[\overline{V}\,\mapsto\,\ast].$

Given a trace of the form $\tau_{1}\curvearrowright\sigma$ and event
$\textit{ev}(\overline{e})$, appending the event is achieved by the trace
$\tau_{1}\cdot\textit{ev}_{\sigma}^{\overline{V}}({\overline{e}})$. The
preceding definition ensures that events in traces are “choppable”;
$\tau\mathbin{\ast\ast}\textit{ev}_{\sigma}^{\overline{V}}({e})$ is well-
defined whenever $\mathrm{last}(\tau)=\sigma$. If $\overline{V}$ is empty then
the state is unchanged, in this case we omit the set of symbolic variables:

$\textit{ev}_{\sigma}({\overline{e}})=\textit{ev}_{\sigma}^{\emptyset}({\overline{e}})$

###### Example 5

Event traces can be inserted at the middle of a trace. To insert an event
$\textit{ev}(Y_{0})$ that does not introduce symbolic variables at
$\sigma_{1}$ to trace $\tau_{0}$ in Example 4, we use the event trace
$\textit{ev}_{\sigma_{1}}({Y_{0}})=\langle\sigma_{1}\rangle\curvearrowright\textit{ev}(\mathrm{val}_{\sigma_{1}}(Y_{0}))\curvearrowright\sigma_{1}=\langle\sigma_{1}\rangle\curvearrowright\textit{ev}(Y_{0})\curvearrowright\sigma_{1}$.
This results in the trace:
$\tau_{2}=\\{Y_{0}>Y_{1}\\}\triangleright\langle\sigma_{1}\rangle\curvearrowright\textit{ev}(Y_{0})\curvearrowright\sigma_{1}\curvearrowright\sigma_{1}[x_{0}\mapsto
17]$. To insert an event $\textit{ev}(Y_{2})$ that introduces the symbolic
variable $Y_{2}$, we use the event trace
$\textit{ev}_{\sigma_{1}}^{\\{Y_{2}\\}}({Y_{2}})=\langle\sigma_{1}\rangle\curvearrowright\textit{ev}(Y_{2})\curvearrowright\sigma_{1}[Y_{2}\,\mapsto\,\ast]$.
The trace in Example 4 results in the trace:

$\tau_{2}^{\prime}=\\{Y_{0}>Y_{1}\\}\triangleright\langle\sigma_{1}\rangle\curvearrowright\textit{ev}(Y_{2})\curvearrowright\sigma_{1}[Y_{2}\,\mapsto\,\ast]\curvearrowright\sigma_{1}[Y_{2}\,\mapsto\,\ast,x_{0}\mapsto
17].$

##### Well-Formed Traces.

Similar to the values of well-formed states, the expressions in events and
path conditions of a well-formed trace should only contain symbolic variables.
This requires all states in a trace to agree upon which variables are
symbolic. We also impose an additional well-formedness condition on events:
any event occurring in a trace must be immediately preceded and followed by
the same state $\sigma$; i.e., it can be obtained by inserting an event trace
at $\sigma$. This implies that a trace always starts and ends with a state,
never with an event. Well-Formed traces are formalised as follows:

######  Definition 11 (Well-Formed Trace)

Let $pc\triangleright\tau$ be a conditioned symbolic trace and let
$V=\bigcup_{\sigma\in\tau}\operatorname{symb}(\sigma)$. The trace
$pc\triangleright\tau$ is well-formed if the following conditions hold:

$\displaystyle\forall\sigma\in\tau.\,\sigma\text{ is well-formed}$ (1)
$\displaystyle\forall\sigma\in\tau.\,(\operatorname{dom}(\sigma)\setminus\operatorname{symb}(\sigma))\cap
V=\emptyset$ (2) $\displaystyle\operatorname{vars}(pc)\subseteq V$ (3)
$\displaystyle\forall\textit{ev}(\overline{e})\in\tau.\,\operatorname{vars}(\overline{e})\subseteq
V$ (4)
$\displaystyle\forall\textit{ev}(\overline{e}),\tau_{1},\tau_{2}.\,\left(\tau=\tau_{1}\curvearrowright\textit{ev}(\overline{e})\cdot\tau_{2}\implies\exists\sigma.\,\mathrm{last}(\tau_{1})=\sigma\land\mathrm{first}(\tau_{2})=\sigma\right)$
(5)

Equation (2) states that a variable that is symbolic in a state cannot be non-
symbolic in another state of the trace. Equations (3)–(4) ensure that any
variable to occur in a path condition or event is a symbolic variable from
some state. Equation (5) guarantees that any event in a trace is surrounded by
identical states.

###### Example 6

The traces $\tau_{2}$ and $\tau_{2}^{\prime}$ in Example 5 have well-formed
states. Only symbolic variables occur in path conditions and events, and the
events were added by inserting event traces. Hence, they are well-formed.

######  Definition 12 (Concrete Traces)

A _concrete trace_ is a well-formed trace containing only concrete states and
events, as well as a fully evaluated, consistent path condition. We use $sh$
for concrete traces, where the letters stand for “shining” trace.

###### Example 7

Let $\sigma_{3}=[x_{0}\mapsto 45,\,Y_{0}\mapsto 3,\,w_{0}\mapsto
42,\,x_{1}\mapsto 2,\,Y_{1}\mapsto 2]$, then a concrete trace of length two is
$\tau_{3}=\langle\sigma_{3}\rangle\curvearrowright\sigma_{3}[x_{0}\mapsto
17]$. The path condition $Y_{0}>Y_{1}$ is evaluated to $3>2=\mathrm{t\\!t}$ in
$\sigma_{3}$ and thus consistent.

Observe that $\tau_{3}$ can be obtained from $\tau_{0}$ in Example 4 by a
suitable instantiation of its symbolic variables. The precise definition of
this operation is the purpose of the following subsection.

###  2.4 Concretisation

A concretisation mapping is defined relative to a state. It associates a
concrete value to each symbolic variable of the state.

######  Definition 13 (State Concretisation Mapping)

A mapping $\rho:\mathit{Var}\to\mathit{Val}$ is a _concretisation mapping_ for
a state $\sigma$ if
$\operatorname{dom}(\rho)\cap\operatorname{dom}(\sigma)=\operatorname{symb}(\sigma)$.

A concretisation mapping $\rho$ may additionally define the value of variables
that are not in the domain of $\sigma$.

###### Example 8

Consider $\sigma_{1}$ of Example 2 where
$\operatorname{symb}(\sigma_{1})=\\{Y_{0},\,Y_{1}\\}$. We define the
concretisation mapping $\rho_{1}=[Y_{0}\mapsto 3,\,Y_{1}\mapsto 2]$ for
$\sigma_{1}$.

Let $\sigma_{4}=[X\mapsto\ast,\,z\mapsto 3]$. Then a concretisation mapping
must give a value to $X$, but _not_ to $z$, for example, $\rho_{2}=[X\mapsto
2,\,Y\mapsto 0]$ is a concretisation mapping for $\sigma_{4}$.

A symbolic state can be concretised using the values assigned to its symbolic
variables in a concretisation mapping to evaluate the symbolic expressions.

######  Definition 14 (State Concretisation)

Let $\sigma$ be a state and $\rho$ a concretisation mapping for $\sigma$. The
concretisation of $\sigma$ with $\rho$ is defined as follows:

$\rho\bullet\sigma=\rho\cup\\{x\mapsto\mathrm{val}_{\rho}(\sigma(x))\mid\,x\in\operatorname{dom}(\sigma)\setminus\operatorname{dom}(\rho)\\}\
.$

###### Example 9

Continuing Examples 7 and 8, we obtain $\rho_{1}\bullet\sigma_{1}=\sigma_{3}$.

To concretise a symbolic trace $pc\triangleright\tau$, we must apply a
concretisation mapping $\rho$ to all states and events of the trace. This
means the domain of $\rho$ must comprise all symbolic variables that occur in
the trace. This is the case for well-formed traces, whose states must agree on
which variables are symbolic (equation (2) in Definition 11).

######  Definition 15 (Trace Concretisation Mapping)

A mapping $\rho$ is a _trace concretisation mapping_ for $\tau$ if it is a
concretisation mapping for all the states in $\tau$. We say that _$\rho$
concretises $\tau$_.

######  Definition 16 (Symbolic Trace Concretisation)

Let $pc\triangleright\tau$ be a well-formed trace and $\rho$ a concretisation
mapping for $\tau$. The _concretisation_ $\rho(pc\triangleright\tau)$ of
$pc\triangleright\tau$ is obtained as $\rho(pc)\triangleright\rho(\tau)$,
where $\rho(pc)=\mathrm{val}_{\rho}(pc)$ and $\rho(\tau)$ is defined as
follows:

$\rho(t_{1}\cdots t_{n}\cdots)=\rho(t_{1})\cdots\rho(t_{n})\cdots$
$\rho(\sigma)=\rho\bullet\sigma$
$\rho(\textit{ev}(\overline{e}))=\textit{ev}(\mathrm{val}_{\rho}(\overline{e}))$

###### Proposition 1

The concretisation of a state is a concrete state. The concretisation of a
well-formed trace is a concrete, well-formed trace. Any concrete state or
trace is a concretisation of itself.

###### Example 10

We continue to use the symbolic trace $pc_{0}\triangleright\tau_{0}$ of
Example 4 and concretise it with the mapping $\rho_{1}$ of Example 8. The
resulting concrete trace is $\tau_{3}$ from Example 7 with path condition
$\\{\mathrm{t\\!t}\\}$.

###  2.5 Continuations

To capture the local semantics of a language, below we define an evaluation
function $\mathrm{val}_{\sigma}(s)$ that evaluates a single statement $s$ in
a—possibly symbolic—state $\sigma$ to a set of conditioned, symbolic traces.
_Compositional_ local evaluation rules can then be defined for each statement
by adding a _continuation marker_ at the end. Continuation markers are needed,
if $s$ is a composite statement that requires separate evaluation of its
constituent parts. In particular, $s$ might not terminate, but this should not
jeopardise parallel computations when computing a sequential trace for a
global system. We avoid this issue by stopping the evaluation after a finite
number of steps by means of a continuation marker, defined as follows:

######  Definition 17 (Continuation Marker)

Let $s$ be a program statement. The _continuation marker_ $\mathrm{K}(s)$
expresses that a given trace is extended by the traces resulting from
computing $s$. The empty continuation, denoted $\mathrm{K}(\mbox{\bottle})$,
expresses that nothing remains to be computed.111The mnemonics of the symbol
is that from an empty bottle nothing can be consumed.

The argument to the continuation marker is the code on which evaluation is
continued. When atomic statements are evaluated, there is no continuation code
but only a return of control. In this case, we end the trace with an empty
continuation (see Section 3.1). Local evaluation (corresponding to phase (1)
in Section 1) is defined below such that for each statement $s$ and symbolic
state $\sigma$ the result of $\mathrm{val}_{\sigma}(s)$ is a set of
conditioned, symbolic traces of the form
$pc\triangleright\tau\cdot\mathrm{K}(s^{\prime})$ where $\tau$ is a _finite_
trace. These traces are called _continuation traces_ ; we denote by
$\mathbf{CTr}$ the type of continuation traces.

##  3 LAGC Semantics of WHILE

${{{\begin{array}[t]{r@{\hspace{2pt}}r@{\hspace{2pt}}l}s\in\mathit{Stmt}\hskip
2.0&::=\hskip
2.0&\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
skip}}}}}}\mid
x:=e\mid\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
if}}}}}}\leavevmode\nobreak\ e\leavevmode\nobreak\ \\{\leavevmode\nobreak\
s\leavevmode\nobreak\ \\}\mid
s;s\mid\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
while}}}}}}\ e\,\\{\,s\,\\}\end{array}$

Figure 2: The syntax for statements in WHILE.

We define a LAGC semantics for WHILE, a language with basic sequential
constructs that can be seen as a kernel of imperative programming languages
[9]. The statements of WHILE consist of skip, assignment, conditional,
sequential composition, and while-loops. The syntax for statements is given in
Figure 2, where we assume given standard expressions $e$. Assignment binds the
value of an expression to a variable. Conditionals and while-loops depend on
the value of a Boolean expression $e$. We assume the standard semantics of
this language to be known, and use it to illustrate our trace semantics.
_Local rules_ (phase (1)) unfold the traces until the next possible scheduling
point, marked by a continuation. _Composition rules_ (phase (2)) select the
next trace to be unfolded at the scheduling point; for the sequential
language, there is only one trace so the latter selection is deterministic.
Due to its simplicity, WHILE merely needs state-based traces, the use of
events is covered in Section 5.4.

###  3.1 Local Evaluation

Local evaluation rules a single statement in the context of a symbolic state,
and return a set of finite continuation traces. Each evaluation rule
represents the execution of a single statement, producing a set of
continuations traces. The evaluation rules are reminiscent of small-step
reduction rules, but work in a denotational setting and with a symbolic
context. We overload the symbol $\mathrm{val}_{\sigma}$ and declare it with
the type $\mathrm{val}_{\sigma}:\mathit{Stmt}\rightarrow 2^{\mathbf{CTr}}$.

The rule for skip generates an empty path condition, returns the state it was
called in, and continues with the empty continuation. The result is a set
containing one singleton trace:

${\begin{array}[]{@{}r@{\,}c@{\,}l@{}}\mathrm{val}_{\sigma}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
skip}}}}}})&=&\\{\emptyset\triangleright\langle\sigma\rangle\cdot\mathrm{K}(\mbox{\bottle})\\}\
.\end{array}$ (6)

The assignment rule generates an empty path condition and a trace from the
current state $\sigma$ to a state which updates $\sigma$ at $x$, and continues
with an empty continuation. The result is one trace of length two:

$\begin{array}[]{@{}r@{\,}c@{\,}l@{}}\mathrm{val}_{\sigma}(x:=e)&=&\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[x\mapsto\mathrm{val}_{\sigma}(e)]\cdot\mathrm{K}(\mbox{\bottle})\\}\
.\end{array}$ (7)

The rule for the conditional statement branches on the value of the condition,
resulting in two traces with different path conditions. The first trace is
obtained from the current state and the continuation with the statements in
the if-branch, and the second trace has the empty continuation (corresponding
to the empty else-branch):

${\begin{array}[]{@{}r@{\,}c@{\,}l@{}}\mathrm{val}_{\sigma}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
if}}}}}}\leavevmode\nobreak\ e\leavevmode\nobreak\ \\{\leavevmode\nobreak\
s\leavevmode\nobreak\
\\})&=&\\{\\{\,\mathrm{val}_{\sigma}(e)=\mathrm{t\\!t}\\}\triangleright\langle\sigma\rangle\cdot\mathrm{K}(s),\leavevmode\nobreak\
\leavevmode\nobreak\
\\{\mathrm{val}_{\sigma}(e)=\mathrm{f\\!f}\\}\triangleright\langle\sigma\rangle\cdot\mathrm{K}(\mbox{\bottle})\,\\}\
.\end{array}$ (8)

The semantics of while is similar to the semantics for the conditional
statement. This gives us the opportunity to illustrate that the semantics of a
statement can easily be expressed in terms of the semantics of another
statement, without having to expose intermediate states:

${{{\begin{array}[]{@{}r@{\,}c@{\,}l@{}}\mathrm{val}_{\sigma}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
while}}}}}}\leavevmode\nobreak\ e\leavevmode\nobreak\ \\{\leavevmode\nobreak\
s\leavevmode\nobreak\
\\})&=&\mathrm{val}_{\sigma}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
if}}}}}}\leavevmode\nobreak\ e\leavevmode\nobreak\ \\{\leavevmode\nobreak\
s;\leavevmode\nobreak\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
while}}}}}}\leavevmode\nobreak\ e\leavevmode\nobreak\ \\{\leavevmode\nobreak\
s\leavevmode\nobreak\ \\}\\})\ .\end{array}$ (9)

The rule for sequential composition $r;s$ is obtained by first evaluating $r$
to traces of the form $pc\triangleright\tau\cdot\mathrm{K}(r^{\prime})$ with
continuation $r^{\prime}$. The statement $s$ can simply be added to this
continuation:

$\begin{array}[]{@{}r@{\,}c@{\,}l@{}}\mathrm{val}_{\sigma}(r;s)=\\{pc\triangleright\tau\cdot\mathrm{K}(r^{\prime};s)\mid
pc\triangleright\tau\cdot\mathrm{K}(r^{\prime})\in\mathrm{val}_{\sigma}(r)\\}\
.\end{array}$ (10)

A subtle point concerns the propagation of empty continuations: $r^{\prime}$
might be the empty continuation , which should be ignored. This behavior is
captured in the following rewrite rule, which is exhaustively applied to
statements occurring inside continuations:

$s;s^{\prime}\rightsquigarrow s^{\prime}\text{ if }s=\mbox{\bottle}\ .$

This rewrite rule reflects that the empty continuation is an identity element
for sequential composition. Similar rewrite rules will be added to handle
identity elements for other composition operators in the sequel.

###### Example 11

Consider the sequential statement $s_{seq}=(x:=1;\ y:=x+1)$. To explain how
its evaluation is performed, we start from an arbitrary symbolic state
$\sigma$ (to be instantiated later by a composition rule). The equation for
sequential composition yields

$\mathrm{val}_{\sigma}(s_{seq})=\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[x\mapsto
1]\cdot\mathrm{K}(y:=x+1)\\}\ .$ (11)

To perform this evaluation, we need the result of evaluating the first
assignment in the context of $\sigma$:

$\mathrm{val}_{\sigma}(x:=1)=\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[x\mapsto
1]\cdot\mathrm{K}(\mbox{\bottle})\\}\ .$

In the composition rules it might be necessary to evaluate the empty
continuation, so we must define it. It is simply the empty set of traces:

$\begin{array}[]{@{}r@{\,}c@{\,}l@{}}\mathrm{val}_{\sigma}(\mbox{\bottle})=\\{\\}\
.\end{array}$ (12)

###### Proposition 2

Given a concrete state $\sigma$ and a program $s$ such that
$vars(s)\subseteq\operatorname{dom}(\sigma)$, then $\mathrm{val}_{\sigma}(s)$
is a set of concrete continuation traces of the form
$pc\triangleright\tau\cdot\mathrm{K}(s^{\prime})$. There is exactly one
continuation trace with a consistent path condition.

###  3.2 Trace Composition

Local traces are composed into concrete global ones. As WHILE is sequential
and deterministic, we expect to obtain exactly one trace, provided that the
execution starts in a concrete state that assigns values to all the variables
of a program. Proposition 2 ensures that all local evaluation rules produce
concrete traces in this case.

The task of the composition rule for WHILE-programs is to repeatedly evaluate
one statement at a time in a concrete state until the next continuation, then
stitch the resulting concrete traces together. Given a concrete trace $sh$
with final state $\sigma$ and a continuation $\mathrm{K}(s)$, we evaluate $s$
starting in $\sigma$. The result is a set of conditioned traces from which one
trace with a consistent path condition and a trailing continuation
$\mathrm{K}(s^{\prime})$ is chosen.222For a deterministic language like WHILE,
there is exactly one trace, but the rule is designed to work for the non-
deterministic extension below as well. The chosen trace $\tau$ is chopped with
the given trace $sh$. Afterwards, the composition rule can be applied again to
the extended concrete trace and $\mathrm{K}(s^{\prime})$.

$\begin{array}[]{c}\sigma=\mathrm{last}(sh)\quad
pc\triangleright\tau\cdot\mathrm{K}(s^{\prime})\in\mathrm{val}_{\sigma}(s)\quad
pc\text{ consistent}\\\\[1.0pt] \hline\cr\\\\[-7.0pt] sh,\mathrm{K}(s)\to
sh\mathbin{\ast\ast}\tau,\mathrm{K}(s^{\prime})\end{array}$ (13)

The rule assumes that $s$ is evaluated to a concrete trace so that
$sh\mathbin{\ast\ast}\tau$ stays concrete. At this stage, symbolic traces do
not yet figure. This works as long as Proposition 2 ensures that
$pc\triangleright\tau$ is a concrete trace, however, in general the proviso
$vars(s)\subseteq\operatorname{dom}(\sigma)$ does not hold. There are several
approaches to address this. For example, it is sufficient to consider the
_non-initialised_ variables of $s$, instead of all of them. We avoid a lengthy
definition to address this technicality by simply assuming that
$\mathrm{last}(sh)$ defines all variables of $s$. This can be easily achieved
by initialising all variables to default values at program start, as done
below.

###  3.3 Global Trace Semantics

Let
$sh,\mathrm{K}(s)\stackrel{{\scriptstyle*}}{{\to}}sh^{\prime},\mathrm{K}(s^{\prime})$
denote the transitive closure of applying rule (13), expressing that
$sh^{\prime},\mathrm{K}(s^{\prime})$ can be reached from $sh,\mathrm{K}(s)$ in
zero or more steps.

######  Definition 18 (Program Semantics)

Given a program s and a state $\sigma$, let

$sh_{0},\,\mathrm{K}(s_{0})\rightarrow
sh_{1},\,\mathrm{K}(s_{1})\rightarrow\cdots$

be a maximal sequence obtained by the repeated application of rule (13),
starting from $\langle\sigma\rangle,\mathrm{K}(s)$. If the sequence is finite,
then it must have the form333Observe that $sh,\mathrm{K}(\mbox{\bottle})$ is
the end of the execution because the evaluation of
$\mathrm{K}(\mbox{\bottle})$ returns $\\{\\}$ such that the composition rule
(13) is no longer applicable. The empty continuation is obtained once the
whole program has been evaluated.

$\langle\sigma\rangle,\mathrm{K}(s)\stackrel{{\scriptstyle*}}{{\to}}sh,\mathrm{K}(\mbox{\bottle})\
.$

If the sequence is infinite, let $sh=\lim_{i\rightarrow\infty}sh_{i}$. The set
of all such traces $sh$ for a program $s$ starting from a state $\sigma$ is
denoted $\mathbf{Tr}(s,\sigma)$.

For any statement $s$, let $I_{s}$ be the state, where $[x\mapsto 0]$ for all
$x\in vars(s)$ (for simplicity, assume all variables are of integer type—the
generalisation is obvious). To help readability, we sometimes omit such
default values from the states in the following examples.

###### Example 12

We apply rule (13) to $\langle I_{seq}\rangle,\mathrm{K}(s_{seq})$, the
program from Example 11. To obtain the premise, we instantiate equation (11)
with $\sigma=I_{seq}$.

$\begin{array}[]{c}I_{seq}=\mathrm{last}(\langle
I_{seq}\rangle)\qquad\emptyset\text{ consistent}\\\
\emptyset\triangleright\langle I_{seq}\rangle\curvearrowright I_{seq}[x\mapsto
1]\cdot\mathrm{K}(y:=x+1)\in\mathrm{val}_{I_{seq}}(x:=1;y:=x+1)\\\\[1.0pt]
\hline\cr\\\\[-7.0pt] \langle I_{seq}\rangle,\mathrm{K}(x:=1;y:=x+1)\to\langle
I_{seq}\rangle\curvearrowright I_{seq}[x\mapsto
1],\,\mathrm{K}(y:=x+1)\end{array}$ (14)

For the subsequent rule application, it is necessary to evaluate the program
$y:=x+1$ in the continuation. Again, we do this for a general state, while in
the rule we use $\sigma=I_{seq}[x\mapsto 1]$ (from now on we omit $I_{seq}$):

$\begin{array}[h]{c}\mathrm{val}_{\sigma}(y:=x+1)=\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[y\mapsto\mathrm{val}_{\sigma}(x+1)]\cdot\mathrm{K}(\mbox{\bottle})\\}\end{array}$

$\begin{array}[]{c}[x\mapsto 1]=\mathrm{last}(\langle
I_{seq}\rangle\curvearrowright[x\mapsto 1])\qquad\emptyset\text{
consistent}\\\ \emptyset\triangleright\langle[x\mapsto
1]\rangle\curvearrowright[x\mapsto 1][y\mapsto\mathrm{val}_{[x\mapsto
1]}(x+1)]\cdot\mathrm{K}(\mbox{\bottle})\in\mathrm{val}_{[x\mapsto
1]}(y:=x+1)\\\\[1.0pt] \hline\cr\\\\[-7.0pt] \langle
I_{seq}\rangle\curvearrowright[x\mapsto 1],\mathrm{K}(y:=x+1)\to\langle
I_{seq}\rangle\curvearrowright[x\mapsto 1]\curvearrowright[x\mapsto 1,y\mapsto
2],\mathrm{K}(\mbox{\bottle})\end{array}$ (15)

Hence,
${\mathbf{Tr}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{x}}:=1;{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{y}}:={\@listingGroup{ltx_lst_identifier}{x}}+1}}}},I_{seq})=\\{\langle
I_{seq}\rangle\curvearrowright[x\mapsto 1]\curvearrowright[x\mapsto 1,y\mapsto
2]\\}$.

###  3.4 Discussion

As mentioned, as long as we start semantic evaluation in a sufficiently
initialised concrete state, Proposition 2 ensures that only concrete traces
will be generated by local rules. Consequently, we have a semantics that can
be aptly called modular and compositional (exactly one independent rule per
language construct and a uniform composition rule), but the overhead
introduced with _symbolic_ traces is not yet justified.

The advantages offered by symbolic traces and states are realised in the
following two sections. In Section 4 we define a program logic for WHILE that
employs symbolic traces at the level of the _calculus_. This close
correspondence between semantics and deduction system is the basis for an
intuitive soundness proof for the deductive system.

In Sections 5–7 we extend WHILE with a number of complex instructions, in
particular, for parallel programming. It will be seen that a wide range of
concurrency paradigms fit naturally into the LAGC semantic framework.

##  4 A Program Logic and Sound Calculus for WHILE

We provide a dynamic logic (DL) [37] as well as a calculus for reasoning about
the correctness of WHILE-programs that is sound relative to our semantics. In
deductive verification dynamic logic [11, 4] offers technical advantages over
Hoare logic [42]: it is syntactically closed with respect to first-order
logic, more expressive, and cleanly separates first-order (“logical”) from
program variables [4, p. 50]. Below we define program formulas of the form
$\psi\rightarrow\tau\left[s\right]\phi$, where $\tau$ is a finite symbolic
trace, $s$ any WHILE-statement, $\psi$ a first-order formula, and $\phi$ a
formula that in turn may contain programs. The intuitive meaning is that any
terminating execution of $s$ continuing a trace that concretises $\tau$ and
started in a state that satisfies $\psi$, must end in a state that satisfies
$\phi$. The modality $\left[s\right]$ corresponds to a _continuation_ in the
semantics of WHILE, represented symbolically.

The unusual aspect of this setup is the presence of a symbolic trace $\tau$
inside a formula. It aligns with our locally abstract semantics, but it is
also justified, because—unlike a semantics—rule schemata in calculus rules
_necessarily_ deal with symbolic values: a verification calculus aims at
proving a property that holds for _all_ inputs of a program, not merely for a
single run. Nevertheless, the presence of symbolic traces inside formulas may
appear as insufficiently syntactic or as an inappropriate intrusion of the
semantics into the calculus. However, efficient syntactic representations of
symbolic assignments are fairly common and well understood: for example, the
deductive verification system KeY uses symbolic _updates_ 444Updates can be
viewed as a syntactic, efficient, lazy representation of symbolic traces:
concrete values are not eagerly substituted and assignments are kept in single
static (SSA) shape. [4] and in the B-method explicit generalised substitutions
play a comparable role [1]. To keep the calculus as general as possible, we do
not commit to a particular implementation of symbolic traces.

The calculus rules given below will symbolically execute a program $s$ in a
sequent of the form $\psi\rightarrow\tau\left[s\right]\phi$ and produce
verification conditions of the form $\Gamma\Rightarrow\tau\,\phi$, where
$\phi$ is a first-order formula and $\tau$ a symbolic trace.

###  4.1 Dynamic Logic

Given a signature $\Sigma$ with typed function and predicate symbols and a set
$V$ of logical variables which is disjoint from the symbols in $\Sigma$, let
$\textbf{Terms}(\Sigma,V)$ denote the well-formed terms over $\Sigma$ and $V$
(respecting type compatibility). Note that the logical variables in $V$ are
disjoint from program variables $\mathit{Var}$. Unlike the latter, the logical
variables can be bound by quantifiers and do not change their value during
program execution.

######  Definition 19 (DL Formula)

Let $\Sigma$ be a signature and $V$ a set of logical variables disjoint from
$\Sigma$. The language $\textbf{DL}(\Sigma,V)$ of formulas in dynamic logic is
defined inductively as follows:

  1. 1.

$B\in\textbf{DL}(\Sigma,V)$ if $B\in\textbf{Terms}(\Sigma,V)$ and the type of
$B$ is Boolean

  2. 2.

$\neg\phi_{1},\,\phi_{1}\land\phi_{2},\,\phi_{1}\lor\phi_{2},\,\phi_{1}\rightarrow\phi_{2},\,\phi_{1}\leftrightarrow\phi_{2}\in\textbf{DL}(\Sigma,V)$
if $\phi_{1},\,\phi_{2}\in\textbf{DL}(\Sigma,V)$

  3. 3.

$\exists x\cdot\phi,\,\forall x\cdot\phi\in\textbf{DL}(\Sigma,V)$ if $x\in V$
and $\phi\in\textbf{DL}(\Sigma,V)$

  4. 4.

${\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi\in\textbf{DL}(\Sigma,V)$
if $s$ is a, possibly empty, WHILE-program and $\phi\in\textbf{DL}(\Sigma,V)$

We often omit the signature and variable set of $\phi\in\textbf{DL}(\Sigma,V)$
and simply write $\phi\in\textbf{DL}$.

There is a subtle point about empty programs. As explained above, the program
$s$ in the modality can be viewed as the continuation of the current trace.
The rules of the calculus defined below will symbolically execute $s$ from
left to right, until the program remaining to be executed is empty. For this
reason, we allow empty programs, denoted $\circ$, in clause (4). The empty
program is the identity element for the composition operators (i.e.,
$\circ;s=s;\circ=s$). However, the continuation with the empty program is not
the same as the empty continuation; it requires a semantics that amounts to an
empty trace, which is reflected in Definition 21 below.

######  Definition 20 (Substitution)

Given a language $\textbf{DL}(\Sigma,V)$ and a set of logical variables
$V^{\prime}=\\{x_{1},\ldots,x_{n}\\}$ such that $V^{\prime}\subseteq V$, a
_substitution_ $[x_{1}/t_{1},\ldots,x_{n}/t_{n}]$ is a function
$V^{\prime}\rightarrow\textbf{Terms}(\Sigma,V)$ which associates with every
$x_{i}\in V^{\prime}$ a type-compatible term
$t_{i}\in\textbf{Terms}(\Sigma,V)$.

Denote by $\phi[x_{1}/t_{1},\ldots,x_{n}/t_{n}]$ the application of a
substitution $[x_{1}/t_{1},\ldots,x_{n}/t_{n}]$ to a logical formula
$\phi\in\textbf{DL}(\Sigma,V)$. Observe that applying a substitution removes
occurrences of _logical variables_ in a formula and does not affect programs.
The application of the substitution has a straightforward inductive definition
over $\phi$ (omitted here).

We write $\tau\models\phi$ and $\sigma\models\phi$ to denote555To simplify
presentation, we assume a fixed standard interpretation of the symbols in
$\Sigma$. It is straightforward to accommodate undefined symbols and
relativise satisfiability to first-order models. that a formula $\phi$ is
valid for a _concrete_ trace $\tau$ and in a _concrete_ state $\sigma$,
respectively (equivalently, $\tau$ and $\sigma$ satisfy $\phi$). Formally,
satisfiability can be defined as follows:

######  Definition 21 (Satisfiability of DL Formulas)

Let $\phi\in\textbf{DL}(\Sigma,V)$ be a DL formula,
$B\in\textbf{Terms}(\Sigma,V)$ a Boolean term, $\sigma$ a concrete state and
$\tau$ a concrete trace.

${{\begin{array}[]{l}\sigma\models
B\iff\mathrm{val}_{\sigma}(B)=\mathrm{t\\!t}\\\
\sigma\models\neg\phi\iff\sigma\not\models\phi\\\
\sigma\models\phi_{1}\land\phi_{2}\iff\sigma\models\phi_{1}\ \text{and}\
\sigma\models\phi_{2}\quad\text{(analogous for the remaining propositional
connectives)}\\\ \sigma\models\exists x\cdot\phi\iff\sigma\models\phi[x/t]\
\text{for some substitution}\ [x/t]\ \text{where}\
t\in\textbf{Terms}(\Sigma,V)\text{, variable-free}\\\ \sigma\models\forall
x\cdot\phi\iff\sigma\models\phi[x/t]\ \text{for all substitutions}\ [x/t]\
\text{where}\ t\in\textbf{Terms}(\Sigma,V)\text{, variable-free}\\\
\sigma\models\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi\iff\tau\models\phi\
\text{for all finite}\
\tau\in\mathbf{Tr}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}},\sigma)\\\
\sigma\models\left[\circ\right]\phi\iff\sigma\models\phi\\\
\tau\models\phi\iff\tau\text{ finite, non-empty},\
\mathrm{last}(\tau)=\sigma,\text{ and }\sigma\models\phi\end{array}$

Observe that the third but last clause implies a partial correctness
semantics.

###  4.2 Calculus

As usual in deductive verification [35], we define a calculus operating on
_sequents_. These have the form $\Gamma\Rightarrow\tau\;\phi$, where $\Gamma$
is a set of formulas thought to be implicitly conjoined (called the
_antecedent_), the symbol $\Rightarrow$ can be read as implication, $\tau$ is
a non-empty, finite symbolic trace, and $\phi$ is a DL formula. Without loss
of generality, we can assume that $\Gamma$ consists of a single formula
$\psi$.

######  Definition 22 (Valid Sequent)

A sequent is _valid_ , denoted $\models\psi\Rightarrow\tau\;\phi$, iff for
_all_ concretisation mappings $\rho$ such that
$\mathrm{first}(\rho(\tau))\models\psi$, we have that

$\mathrm{last}(\rho(\tau))\models\phi\enspace.$

To make the correspondence with the semantics of WHILE more immediate, we
represent path conditions as a separate set in the antecedent of the sequents.
The rules for programs are shown in Figure 3. Observe that this rule set is
incomplete as it leaves open how a sequent of the form
$\Gamma,pc\Rightarrow\tau\,\phi$ should be derived, where $\phi$ is a first-
order formula. For generality, we do not commit to a specific representation
of symbolic traces and how they are applied to first-order formulas. For
example, if symbolic traces are represented with updates as in KeY, then the
rules in [4, Ch. 2] can be used. In the soundness proof below we assume that
there is a sound calculus able to derive $\Gamma,pc\Rightarrow\tau\,\phi$.

${{{{{{{{{\begin{array}[]{c}\begin{array}[]{c}\textsc{\footnotesize(Assign)}\\\
\sigma^{\prime}=\sigma[x\mapsto\mathrm{val}_{\sigma}(e)]\\\
\mathrm{last}(\tau)=\sigma\qquad\Gamma,pc\Rightarrow\tau\curvearrowright\sigma^{\prime}\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi\\\
\hline\cr\Gamma,pc\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{x}}:={\@listingGroup{ltx_lst_identifier}{e}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi\end{array}\qquad\begin{array}[]{c}\textsc{\footnotesize(Cond)}\\\
\mathrm{last}(\tau)=\sigma\\\
\Gamma,pc\cup\\{\mathrm{val}_{\sigma}(e)=\mathrm{f\\!f}\\}\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}\textquoteright}}}}\right]\phi\\\
\Gamma,pc\cup\\{\mathrm{val}_{\sigma}(e)=\mathrm{t\\!t}\\}\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{s}}\textquoteright}}}}\right]\phi\\\
\hline\cr\Gamma,pc\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
if}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{e}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{s}}{\@listingGroup{ltx_lst_space}{
}}\textbraceright;{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{s}}\textquoteright}}}}\right]\phi\end{array}\\\
\\\ \begin{array}[]{c}\textsc{\footnotesize(skip)}\\\
\Gamma,pc\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi\\\
\hline\cr\Gamma,pc\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
skip}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi\end{array}\qquad\begin{array}[]{c}\textsc{\footnotesize(While)}\\\
\Gamma,pc\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
if}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{e}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{s}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_keyword}{\bf while}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{e}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{s}}{\@listingGroup{ltx_lst_space}{
}}\textbraceright{\@listingGroup{ltx_lst_space}{
}}\textbraceright;{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{s}}\textquoteright}}}}\right]\phi\\\
\hline\cr\Gamma,pc\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
while}}{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{e}}{\@listingGroup{ltx_lst_space}{
}}\textbraceleft{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{s}}{\@listingGroup{ltx_lst_space}{
}}\textbraceright;{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{s}}\textquoteright}}}}\right]\phi\end{array}\qquad\begin{array}[]{c}\textsc{\footnotesize(Empty)}\\\
\Gamma,pc\Rightarrow\tau\,\phi\\\
\hline\cr\Gamma,pc\Rightarrow\tau\left[\circ\right]\phi\end{array}\end{array}$

Figure 3: Dynamic logic sequent rules for WHILE.

We denote by
${\vdash\psi\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi$
that the DL sequent
${\psi\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi$
can be derived in the proof system. To prove that a postcondition Post holds
after termination of program $s$ under a precondition Pre, it is sufficient to
derive the sequent

${\text{Pre}\Rightarrow\langle\sigma_{\ast}\rangle\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\text{Post}\enspace,$

where $\sigma_{\ast}(x)\mapsto\ast$ for all $x\in\mathit{Var}$. By
construction, the only symbolic variables that occur in a well-formed symbolic
trace $\tau$ are introduced in the initial state of $\tau$. Thus, all path
conditions are expressed in terms of the initial symbolic state
$\sigma_{\ast}$.

######  Theorem 4.1 (Soundness)

Let $\tau$ be a well-formed symbolic trace and let $\phi,\,\psi$ be DL
formulas. If $\vdash\psi\Rightarrow\tau\;\phi$, then
$\models\psi\Rightarrow\tau\;\phi$.

###### Proof

The proof is by induction over the structure of $\phi$. We assume the
soundness of first-order (or “program-free”) formulas; i.e., if $\vdash B$
then $\models B$ for $B\in\textbf{Terms}(\Sigma,V)$.

Case Empty. Assume $\vdash\psi\Rightarrow\tau\left[\circ\right]\phi$. By rule
(Empty), we get $\vdash\psi\Rightarrow\tau\,\phi$.

For the base case, we may assume that $\phi$ is a first-order formula. Then,
by assumption, $\models\psi\Rightarrow\tau\,\phi$, which means that for any
concretisation mapping $\rho$, if $\mathrm{first}(\rho(\tau))\models\psi$,
then $\mathrm{last}(\rho(\tau))\models\phi$. The latter is, by Definition 21,
equivalent to $\mathrm{last}(\rho(\tau))\models\left[\circ\right]\phi$. Since
$\rho$ was arbitrary, this yields
$\models\psi\Rightarrow\tau\left[\circ\right]\phi$.

For the inductive case, we may assume that $\phi$ is any DL formula. Then,
$\models\psi\Rightarrow\tau\,\phi$ follows from the induction hypothesis
(hereafter, IH), and the rest of the proof is analogous to the base case.

Case Skip. Assume
${\vdash\psi\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
skip}};{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi$. By rule
(Skip), we get
${\vdash\psi\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi$,
and by IH we have
${\models\psi\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi$.
Hence, for any concretisation mapping $\rho$, if
$\mathrm{first}(\rho(\tau))\models\psi$, then
$\mathrm{last}(\rho(\tau))\models\left[s\right]\phi$. Then
$\tau^{\prime}\models\left[\circ\right]\phi$ for all
$\tau^{\prime}\in\mathbf{Tr}(s,\mathrm{last}(\rho(\tau)))$. By equations (13),
(10) and (6), we have
${\mathbf{Tr}(s,\sigma)=\mathbf{Tr}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
skip}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{s}}}}}},\sigma)$ for any $\sigma$.
Therefore, for all
${\tau^{\prime\prime}\in\mathbf{Tr}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
skip}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{s}}}}}},\mathrm{last}(\rho(\tau)))$ we
have $\tau^{\prime\prime}\models\left[\circ\right]\phi$, and it follows that
${\models\psi\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
skip}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi$.

Case Assign. Assume
${\vdash\psi\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{x}}:={\@listingGroup{ltx_lst_identifier}{e}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi$. By rule (Assign),
we get
${\vdash\psi\Rightarrow\tau\curvearrowright\sigma^{\prime}\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi$
where $\mathrm{last}(\tau)=\sigma$ and
$\sigma^{\prime}=\sigma[x\mapsto\mathrm{val}_{\sigma}(e)]$. By IH we have
${\models\psi\Rightarrow\tau\curvearrowright\sigma^{\prime}\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi$.
Hence, for any concretisation mapping $\rho$, if
$\mathrm{first}(\rho(\tau\curvearrowright\sigma^{\prime}))\models\psi$, then
$\mathrm{last}(\rho(\tau\curvearrowright\sigma^{\prime}))\models\left[s\right]\phi$,
i.e. $\rho(\sigma^{\prime})\models\left[s\right]\phi$. By equations (13), (10)
and (7), we have
${\mathbf{Tr}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{x}}:={\@listingGroup{ltx_lst_identifier}{e}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{s}}}}}},\sigma)=\\{\langle\sigma\rangle\curvearrowright\sigma^{\prime}\mathbin{\ast\ast}\tau^{\prime}\mid\tau^{\prime}\in\mathbf{Tr}(s,\sigma^{\prime})\\}$.
Therefore,
${\mathrm{last}(\rho(\tau))\models\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{x}}:={\@listingGroup{ltx_lst_identifier}{e}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi$ and, since $\rho$
was arbitrary and
$\mathrm{first}(\rho(\tau\curvearrowright\sigma^{\prime}))=\mathrm{first}(\rho(\tau))$,
we have
${\models\psi\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{x}}:={\@listingGroup{ltx_lst_identifier}{e}};{\@listingGroup{ltx_lst_space}{
}}{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi$.

Case Cond. Assume
${{{{\vdash\psi\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
if}}}}}}\leavevmode\nobreak\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{e}}}}}}\leavevmode\nobreak\
\\{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}\textquoteright}}}}\\};\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi$.
By rule (Cond), we get
${\vdash\psi,\,\mathrm{val}_{\sigma}(e)=\mathrm{f\\!f}\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi$
and
${\vdash\psi,\,\mathrm{val}_{\sigma}(e)=\mathrm{t\\!t}\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}\textquoteright;{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi$,
where $\mathrm{last}(\tau)=\sigma$. Correspondingly, we have two induction
hypotheses:
${\models\psi,\,\mathrm{val}_{\sigma}(e)=\mathrm{f\\!f}\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi$
(hereafter, IH1) and
${\models\psi,\,\mathrm{val}_{\sigma}(e)=\mathrm{t\\!t}\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}\textquoteright;{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi$
(hereafter, IH2). Let $\rho$ be any concretisation mapping and assume
$\mathrm{first}(\rho(\tau))\models\psi$. Depending on the value of
$\mathrm{val}_{\rho(\sigma)}(e)$, exactly one of the subcases applies.

Subcase IH1. We can assume $\mathrm{val}_{\rho(\sigma)}(e)=\mathrm{f\\!f}$
and, by IH1,
${\models\psi,\,\mathrm{val}_{\sigma}(e)=\mathrm{f\\!f}\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi$,
which together gives $\mathrm{last}(\rho(\tau))\models\left[s\right]\phi$. By
definition,
${\tau^{\prime}\models\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi$
for all
${\tau^{\prime}\in\mathbf{Tr}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}},\mathrm{last}(\rho(\tau)))$.
By Equations (13), (10) and (8), we have
${{{{{\mathbf{Tr}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}},\sigma)=\mathbf{Tr}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
if}}}}}}\leavevmode\nobreak\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{e}}}}}}\leavevmode\nobreak\
\\{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}\textquoteright}}}}\\};\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}},\,\sigma)$,
observing that the path condition is consistent. Therefore,
${{{{\tau^{\prime}\models\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
if}}}}}}\leavevmode\nobreak\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{e}}}}}}\leavevmode\nobreak\
\\{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}\textquoteright}}}}\\};\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi$
for all
${{{{\tau^{\prime}\in\mathbf{Tr}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
if}}}}}}\leavevmode\nobreak\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{e}}}}}}\leavevmode\nobreak\
\\{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}\textquoteright}}}}\\};\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}},\,\mathrm{last}(\rho(\tau)))$
and so
${{{{\models\psi\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
if}}}}}}\leavevmode\nobreak\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{e}}}}}}\leavevmode\nobreak\
\\{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}\textquoteright}}}}\\};\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_identifier}{s}}}}}}\right]\phi$.

Subcase IH2. We can assume $\mathrm{val}_{\rho(\sigma)}(e)=\mathrm{t\\!t}$ and
proceed by a completely analogous argument as in the other subcase.

Case While. Follows directly from the case for Cond.

##  5 Semantics for a Shared-Variable Parallel Programming Language

In this and the following section we show that the LAGC semantics naturally
extends to cover advanced language constructs. We gradually extend WHILE with
parallel programming constructs: parallel execution, procedure calls,
distributed memory, dynamic process creation, and communication between
procedures. To cater for interleaved execution of parallel instructions, and
to allow for the compositional definition of semantics, the traces of the
sequential language are gradually unfolded by means of continuations.

###  5.1 Local Parallelism

We extend WHILE with a statement for parallel execution, such that the syntax
for statements from Figure 2 becomes:

${{\begin{array}[]{r@{\,}l@{\,}l}s\in\mathit{Stmt}&::=&\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\ s\leavevmode\nobreak\ ||\leavevmode\nobreak\ s\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}}\ \ |\ \ldots\ .\\\ \end{array}$

The semantics of this statement consists in interleaving the evaluation of the
two parallel branches at the granularity of atomic statements, as exemplified
below.

###### Example 13

The execution of the program
${{s_{co}=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\ x:=1;\ y:=x+1\leavevmode\nobreak\ ||\leavevmode\nobreak\ x:=2\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}}$ produces one of three possible traces that correspond to the traces
of the following sequential programs: $x:=1;\ y:=x+1;\ x:=2$, or $x:=1;\
x:=2;\ y:=x+1$, or $x:=2;\ x:=1;\ y:=x+1$.

####  5.1.1 Local Evaluation

The evaluation rule for the parallel execution statement co
$r\leavevmode\nobreak\ ||\leavevmode\nobreak\ s$ oc branches on the statement
which first gets to execute, resulting in two sets of traces where the first
set contains traces with the path condition of $r$ and the continuation of $r$
in parallel with $s$ and the second set contains traces with the path
condition of $s$ and the continuation of $s$ in parallel with r. The valuation
rule is formalised as follows:

${{{{{{\begin{array}[]{@{}r@{\,}c@{\,}l@{}}\mathrm{val}_{\sigma}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\ r\leavevmode\nobreak\ ||\leavevmode\nobreak\ s\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}})&=&\\{pc_{r}\\!\triangleright\\!\tau_{r}\cdot\mathrm{K}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\ r^{\prime}\leavevmode\nobreak\ ||\leavevmode\nobreak\ s\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}})\\!\mid\\!pc_{r}\\!\triangleright\\!\tau_{r}\cdot\mathrm{K}(r^{\prime})\\!\in\\!\mathrm{val}_{\sigma}(r)\\}\\\
&&\cup\\{pc_{s}\\!\triangleright\\!\tau_{s}\cdot\mathrm{K}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\ r\leavevmode\nobreak\ ||\leavevmode\nobreak\ s^{\prime}\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}})\\!\mid\\!pc_{s}\\!\triangleright\\!\tau_{s}\cdot\mathrm{K}(s^{\prime})\\!\in\\!\mathrm{val}_{\sigma}(s)\\}\
.\end{array}$ (16)

As with sequential composition in rule (10), we need to ensure that empty
continuations are not propagated. To this end we define the following rewrite
rule for parallel composition inside continuations (observe that the case
$s=s^{\prime}=\mbox{\bottle}$ cannot occur):

${{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\ s\,\leavevmode\nobreak\ ||\leavevmode\nobreak\ s^{\prime}\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}}\rightsquigarrow\left\\{\begin{array}[]{rl}s^{\prime}&\text{ if
}s=\mbox{\bottle},\,s^{\prime}\neq\mbox{\bottle}\\\ s&\text{ if
}s\neq\mbox{\bottle},\,s^{\prime}=\mbox{\bottle}\ .\end{array}\right.$ (17)

####  5.1.2 Trace Composition

The composition rule (13) can be kept unchanged (although the abstract variant
in rule (23) below can be used as well). Its effect is that all combinations
of execution sequences of atomic statements in the parallel branches can be
generated. This behaviour corresponds to the classical interleaving semantics
(e.g., [8]), as demonstrated below.

###### Example 14

Consider program $s_{co}$ from Example 13, its evaluation is

${{{{{{\mathrm{val}_{\sigma}(s_{co})\begin{array}[t]{l}=\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[x\mapsto
1]\cdot\mathrm{K}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\ y:=x+1\leavevmode\nobreak\ \leavevmode\nobreak\
||\leavevmode\nobreak\ \leavevmode\nobreak\ x:=2\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}})\\}\cup\\\
\quad\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[x\mapsto
2]\cdot\mathrm{K}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\ x:=1;y:=x+1\leavevmode\nobreak\ \leavevmode\nobreak\
||\leavevmode\nobreak\ \leavevmode\nobreak\ \mbox{\bottle}\leavevmode\nobreak\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}})\\}\\\
=\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[x\mapsto
1]\cdot\mathrm{K}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\ y:=x+1\leavevmode\nobreak\ ||\leavevmode\nobreak\ x:=2\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}})\\}\cup\\\
\quad\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[x\mapsto
2]\cdot\mathrm{K}(x:=1;y:=x+1)\\}\ ,\end{array}$

using the following sub-evaluations:
$\mathrm{val}_{\sigma}(x:=1;y:=x+1)=\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[x\mapsto
1]\cdot\mathrm{K}(y:=x+1)\\}$ and
$\mathrm{val}_{\sigma}(x:=2)=\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[x\mapsto
2]\cdot\mathrm{K}(\mbox{\bottle})\\}$. For trace composition, we first need to
evaluate the continuation
${{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\ y:=x+1\leavevmode\nobreak\ ||\leavevmode\nobreak\ x:=2\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}}$:

${{{{{{\mathrm{val}_{\sigma}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\ y:=x+1\leavevmode\nobreak\ ||\leavevmode\nobreak\ x:=2\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}})\begin{array}[t]{l}=\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[y\mapsto\mathrm{val}_{\sigma}(x+1)]\cdot\mathrm{K}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\ \mbox{\bottle}\leavevmode\nobreak\ \leavevmode\nobreak\
||\leavevmode\nobreak\ \leavevmode\nobreak\ x:=2\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}})\\}\cup\\\
\quad\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[x\mapsto
2]\cdot\mathrm{K}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\ y:=x+1\leavevmode\nobreak\ \leavevmode\nobreak\
||\leavevmode\nobreak\ \leavevmode\nobreak\ \mbox{\bottle}\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}})\\}\\\
=\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[y\mapsto\mathrm{val}_{\sigma}(x+1)]\cdot\mathrm{K}(x:=2)\\}\cup\\\
\quad\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[x\mapsto
2]\cdot\mathrm{K}(y:=x+1)\\}\ ,\end{array}$

using the following sub-evaluations:
$\mathrm{val}_{\sigma}(y:=x+1)=\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[y\mapsto\mathrm{val}_{\sigma}(x+1)]\cdot\mathrm{K}(\mbox{\bottle})\\}$
and
$\mathrm{val}_{\sigma}(x:=2)=\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[x\mapsto
2]\cdot\mathrm{K}(\mbox{\bottle})\\}$.

To illustrate trace composition, let us consider the trace where statement
$x:=1$ is executed first and explore the remaining possible traces. We start
from the state $I_{co}$. The first application of rule (13) results in the
following concrete trace and continuation:

${{\langle I_{co}\rangle\curvearrowright[x\mapsto
1],\mathrm{K}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\ y:=x+1\leavevmode\nobreak\ ||\leavevmode\nobreak\ x:=2\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}})\ .$

At this point, two different instances of the composition rule are applicable,
corresponding to the two possible interleavings; i.e., there is a choice
between the two continuations in ${{\mathrm{val}_{[x\mapsto
1]}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\ y:=x+1\leavevmode\nobreak\ ||\leavevmode\nobreak\ x:=2\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}})$ as shown above. The first possible instance of the composition rule
is:

${{{{\begin{array}[]{c}[x\mapsto 1]=\mathrm{last}(\langle
I_{co}\rangle\curvearrowright[x\mapsto 1])\qquad\emptyset\text{ consistent}\\\
\hskip 8.53581pt\emptyset\triangleright\langle[x\mapsto
1]\rangle\curvearrowright[x\mapsto 1][y\mapsto\mathrm{val}_{[x\mapsto
1]}(x+1)]\cdot\mathrm{K}(x:=2)\\\ \in\mathrm{val}_{[x\mapsto
1]}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\ y:=x+1\leavevmode\nobreak\ ||\leavevmode\nobreak\ x:=2\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}})\\\\[1.0pt] \hline\cr\\\\[-7.0pt] \langle
I_{co}\rangle\curvearrowright[x\mapsto
1],\mathrm{K}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\ y:=x+1\leavevmode\nobreak\ ||\leavevmode\nobreak\ x:=2\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}})\to\\\ \langle I_{co}\rangle\curvearrowright[x\mapsto
1]\curvearrowright[x\mapsto 1,y\mapsto 2],\mathrm{K}(x:=2)\end{array}$ (18)

One further rule application is possible, which results in the final step:

$\begin{array}[]{l}\langle I_{co}\rangle\curvearrowright[x\mapsto
1]\curvearrowright[x\mapsto 1,y\mapsto 2],\mathrm{K}(x:=2)\to\\\ \langle
I_{co}\rangle\curvearrowright[x\mapsto 1]\curvearrowright[x\mapsto 1,y\mapsto
2]\curvearrowright[x\mapsto 2,y\mapsto
2],\mathrm{K}(\mbox{\bottle})\enspace.\end{array}$

The second possible instance of the composition rule is similar and yields:

$\begin{array}[]{l}\langle I_{co}\rangle\curvearrowright[x\mapsto
1]\curvearrowright[x\mapsto 2],\mathrm{K}(y:=x+1)\to\\\ \langle
I_{co}\rangle\curvearrowright[x\mapsto 1]\curvearrowright[x\mapsto
2]\curvearrowright[x\mapsto 2,y\mapsto
3],\mathrm{K}(\mbox{\bottle})\enspace.\end{array}$

The third possible trace is obtained analogously by starting with the second
branch. After this, only one continuation is possible. Altogether, the
following traces are obtained:

$\begin{array}[]{lcl}\mathbf{Tr}(s_{co},I_{co})&=\;\\{&\langle
I_{co}\rangle\curvearrowright[x\mapsto 1]\curvearrowright[x\mapsto 1,y\mapsto
2]\curvearrowright[x\mapsto 2,y\mapsto 2],\\\ &&\langle
I_{co}\rangle\curvearrowright[x\mapsto 1]\curvearrowright[x\mapsto
2]\curvearrowright[x\mapsto 2,y\mapsto 3],\\\ &&\langle
I_{co}\rangle\curvearrowright[x\mapsto 2]\curvearrowright[x\mapsto
1]\curvearrowright[x\mapsto 1,y\mapsto 2]\;\\}\ .\end{array}$

####  5.1.3 Calculus

Let $ar$ and $as$ range over the atomic statements of WHILE (i.e., assignment
and skip). It is straightforward to realise a set of DL rules directly
inspired by rule (16). Local parallelism introduces a new composition
operator, and the rules need to cover the different cases of nested
statements.

${{{{{{{{{{{{{{{{{{{{{{{{\begin{array}[]{c}\begin{array}[]{c}\textsc{\footnotesize(Par)}\\\
\Gamma,\,pc\Rightarrow\tau\left[ar;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\;r^{\prime}\leavevmode\nobreak\ ||\leavevmode\nobreak\
as;\,s^{\prime}\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}}\right]\phi\\\
\Gamma,\,pc\Rightarrow\tau\left[as;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\;ar;\,r^{\prime}\leavevmode\nobreak\ ||\leavevmode\nobreak\
s^{\prime}\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}}\right]\phi\\\
\hline\cr\Gamma,\,pc\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\;ar;\,r^{\prime}\leavevmode\nobreak\ ||\leavevmode\nobreak\
as;\,s^{\prime}\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}}\right]\phi\end{array}\quad\begin{array}[]{c}\\\
\textsc{\footnotesize(Par-Empty${}_{1})$}\\\
\Gamma,\,pc\Rightarrow\tau\left[s\right]\phi\\\
\hline\cr\Gamma,\,pc\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\circ\\!\\!\leavevmode\nobreak\ ||\leavevmode\nobreak\
s\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}}\right]\phi\end{array}\quad\begin{array}[]{c}\\\
\textsc{\footnotesize(Par-Empty${}_{2}$)}\\\
\Gamma,\,pc\Rightarrow\tau\left[r\right]\phi\\\
\hline\cr\Gamma,\,pc\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\;r\leavevmode\nobreak\ ||\leavevmode\nobreak\
\\!\\!\circ\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}}\right]\phi\end{array}\\\ \\\
\begin{array}[]{@{}c@{}}\textsc{\footnotesize(Par-If${}_{1}$)}\\\
\mathrm{last}(\tau)=\sigma\\\
\Gamma,pc\cup\\{\mathrm{val}_{\sigma}(e)=\mathrm{f\\!f}\\}\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\;\,r^{\prime}\leavevmode\nobreak\ ||\leavevmode\nobreak\
s\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}}\right]\phi\\\
\Gamma,pc\cup\\{\mathrm{val}_{\sigma}(e)=\mathrm{t\\!t}\\}\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\;r;\,r^{\prime}\leavevmode\nobreak\ ||\leavevmode\nobreak\
s\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}}\right]\phi\\\
\hline\cr\Gamma,\,pc\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
if}}}}}}\ e\ \\{r\\};\,r^{\prime}\leavevmode\nobreak\ ||\leavevmode\nobreak\
s\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}}\right]\phi\end{array}\qquad\begin{array}[]{@{}c@{}}\textsc{\footnotesize(Par-
If${}_{2}$)}\\\ \mathrm{last}(\tau)=\sigma\\\
\Gamma,pc\cup\\{\mathrm{val}_{\sigma}(e)=\mathrm{f\\!f}\\}\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\;\,r\leavevmode\nobreak\ ||\leavevmode\nobreak\
s^{\prime}\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}}\right]\phi\\\
\Gamma,pc\cup\\{\mathrm{val}_{\sigma}(e)=\mathrm{t\\!t}\\}\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\;r\leavevmode\nobreak\ ||\leavevmode\nobreak\
s;s^{\prime}\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}}\right]\phi\\\
\hline\cr\Gamma,\,pc\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\;r\leavevmode\nobreak\ ||\leavevmode\nobreak\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
if}}}}}}\ e\
\\{s\\};\,s^{\prime}\;\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}}\right]\phi\end{array}\end{array}$

The base cases are covered by rules (Par), (Par-Empty1) and (Par-Empty2). Rule
(Par), where $ar$ and $as$ match atomic statements, splits the proof into two
cases, depending on the first executed atomic statement in the interleaved
execution. The two rules (Par-Empty1) and (Par-Empty2) correspond to rewriting
with empty continuations in rule (17). The remaining rules deal with the case
when the statement inside the parallel statement is not atomic. We illustrate
these rules with (Par-If1) and (Par-If2), which resolve a conditional inside
the parallel statement. Similar rules are required for inner loops, which
unfold a while-statement in either branch into a conditional, and for nested
parallel statements, which split the proof by recursively unfolding different
branches. While the soundness of these rules, relative to the LAGC semantics,
is evident, they are impractical because they quickly lead to path explosion.
Numerous approaches to mitigate this effect have been proposed in the
literature (e.g., [63, 10, 62, 32]), but here is not the place to dwell on
them.

###  5.2 Atomic

We extend WHILE with atomic blocks to control interleaving in the execution of
parallel statements, such that the syntax for statements from Figure 2 becomes

${{{\begin{array}[]{r@{\,}l@{\,}l}s\in\mathit{Stmt}&::=&\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\ s\leavevmode\nobreak\ ||\leavevmode\nobreak\ s\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}}\
\mid\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
atomic}}}}}}({st})\ \mid\ \ldots\enspace,\\\ \end{array}$

where $st$ is a statement without while loops.

####  5.2.1 Local Evaluation

The atomic statement protects its argument against interleaving computations
from other branches of a parallel execution operator. A (loop-free) statement
$st$ can be made to execute atomically, i.e. without preemption, written
${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
atomic}}}}}}(st)$. Atomic execution requires interleaving points to be
_removed_ during trace composition.

${{\begin{array}[]{@{}r@{\,}c@{\,}l@{}}\mathrm{val}_{\sigma}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
atomic}}}}}}(st))=&&\\{pc_{1}\cup
pc_{2}\triangleright\tau_{1}\mathbin{\ast\ast}\tau_{2}\cdot\mathrm{K}(\mbox{\bottle})\mid
pc_{1}\triangleright\tau_{1}\cdot\mathrm{K}(st^{\prime})\in\mathrm{val}_{\sigma}(st)\land
st^{\prime}\not=\mbox{\bottle}\ \land\\\ &&\qquad\qquad
pc_{2}\triangleright\tau_{2}\cdot\mathrm{K}(\mbox{\bottle})\in\mathrm{val}_{\sigma^{\prime}}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
atomic}}}}}}(st^{\prime}))\land\sigma^{\prime}=\mathrm{last}(\tau_{1})\\}\
\cup\\\ &&\\{pc\triangleright\tau\cdot\mathrm{K}(\mbox{\bottle})\mid
pc\triangleright\tau\cdot\mathrm{K}(\mbox{\bottle})\in\mathrm{val}_{\sigma}(st)\\}\end{array}$
(19)

The main idea behind rule (19) is to recursively unfold the execution of its
atomic argument $st$, while removing continuation markers. During trace
composition, this will prevent the atomic code from being interleaved. The
rule has two cases, depending on whether the evaluation of $st$ contains a
non-empty continuation or not: if the continuation is not empty, we need to
evaluate it immediately, as the execution cannot be interrupted before the end
of the atomic statement. Note the structural similarity in the definition of
the first trace set above and the composition rule (13). The difference is
that the consistency check and concretisation are deferred until the actual
trace composition.

##### Discussion.

In this execution model, the semantics $\mathrm{val}_{\sigma}$ of non-
terminating atomic statements is _undefined_ , which is the reason for
excluding loops. This is a design choice and not a principal limitation: It is
possible to define the semantics of non-terminating atomic programs with
suitable scheduling events that allow to process non-terminating code piece-
wise [27]. However, that approach is more complex than the adopted solution
and breaks with the modularity we aim at with only one rule per syntactic
construct. A different solution is to equip atomic with a path condition
argument (using $pc_{1}$ in the recursive call) and only keep consistent
traces. When $\sigma$ is concrete, this would suffice for terminating loops.

Another solution, presented in Section 7.3 below, is to define a trace
composition rule with run-to-completion semantics: atomic execution of _any_
statement is the default, which can be interrupted only at explicit suspension
points.

Observe that the semantics of non-terminating _non-atomic_ programs is well-
defined: infinite traces are produced by an infinite number of applications of
the composition rule.

####  5.2.2 Trace Composition

The trace composition rule (13) is unchanged, but it is worthwhile to observe
how it works in the presence of atomic. When rule (13) processes a
continuation of the form
${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
atomic}}}}}}(st)$, it needs to evaluate
${\mathrm{val}_{\sigma}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
atomic}}}}}}(st))$ for the concrete state $\sigma=\mathrm{last}(sh)$. Rule
(19) evaluates $s$ until it reaches a continuation $s^{\prime}$, then
recursively evaluates $s^{\prime}$, until $s$ is completely executed. No
interleaving can occur during the evaluation, which reflects the intended
semantics of atomic statements.

###### Example 15

To illustrate the evaluation of interleaved execution with atomic, we modify
Example 14 as follows: let
${{{s_{at}=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
atomic}}}}}}(x:=1;y:=x+1)\leavevmode\nobreak\ ||\leavevmode\nobreak\ x:=2\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}}$. The evaluation branches into either
${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
atomic}}}}}}(x:=1;y:=x+1)$ and then $x:=2$, or $x:=2$ and then
${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
atomic}}}}}}(x:=1;y:=x+1)$. In either case, the final value of $y$ is $2$, as
shown in the following evaluation:

${\begin{array}[t]{l@{}l}\mathrm{val}_{\sigma}(s_{at})=&\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[x\mapsto
1][y\mapsto\mathrm{val}_{\sigma[x\mapsto 1]}(x+1)]\cdot\mathrm{K}(x:=2)\\}\
\cup\\\
&\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[x\mapsto
2]\cdot\mathrm{K}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
atomic}}}}}}(x:=1;y:=x+1))\\}\ .\end{array}$

Now the trace in which $y$ has the final value $3$, is no longer produced;
starting from state $I_{at}=I_{co}$ we have
$\mathbf{Tr}(s_{at},I_{at})=\\{\langle I_{at}\rangle\curvearrowright[x\mapsto
1]\curvearrowright[x\mapsto 1,y\mapsto 2]\curvearrowright[x\mapsto 2,y\mapsto
2],\ \langle I_{at}\rangle\curvearrowright[x\mapsto
2]\curvearrowright[x\mapsto 1]\curvearrowright[x\mapsto 1,y\mapsto 2]\\}$.

####  5.2.3 Calculus

Rules for atomic are remarkably simple, because non-interleaved execution is
the _default_ in the calculus while interleaving is modeled with a case
distinction. We let atomic(st) be an atomic statement which matches $ar$ and
$as$ in Section 5.1.3, such that rule (Par) applies, and introduce a rule
which captures that an atomic statement is equivalent to the statement itself
in a sequential setting:

${\begin{array}[]{@{}c@{}}\textsc{\footnotesize(Atomic)}\\\
\Gamma,\,pc\Rightarrow\tau\left[st;s\right]\phi\\\
\hline\cr\Gamma,\,pc\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
atomic}}}}}}(st);s\right]\phi\end{array}$

###  5.3 Local Memory

We extend WHILE with local variable declarations by introducing a syntactic
category of variable declarations $\mathit{VarDecl}$ and add blocks to the
syntax for statements from Figure 2:

$\begin{array}[t]{r@{\hspace{2pt}}r@{\hspace{2pt}}l}s\in\mathit{Stmt}\hskip
2.0&::=\hskip 2.0&\\{\ d\ s\ \\}\mid\ldots\\\ d\in\mathit{VarDecl}\hskip
2.0&::=\hskip 2.0&\varepsilon\ |\ x;\ d\end{array}$

For simplicity, we omit an empty list of variable declarations in a scope
$\\{\ \varepsilon\ s\ \\}$ and just write $\\{\ s\ \\}$.

####  5.3.1 Local Evaluation

A block $\\{\ d\ s\ \\}$ introduces a local variable scope such that the
program variables $d$ should only be accessible for the statement $s$. To
avoid interference among variable declarations in different scopes, possibly
introducing the same variable name, the evaluation rule renames the variables
in $d$ to unused names and adds the renamed program variables to the state.
The local program variables are correspondingly renamed in $s$. The local
evaluation rules cover a non-empty and empty list of local variable
declarations, respectively.

$\begin{array}[]{@{}r@{\,}c@{\,}l@{}}\mathrm{val}_{\sigma}(\\{\ x;d\ s\
\\})&=&\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[x^{\prime}\mapsto
0]\cdot\mathrm{K}(\\{\ d\ s[x\leftarrow x^{\prime}]\ \\})\mid
x^{\prime}\notin\operatorname{dom}(\sigma)\\}\end{array}$ (20)
$\begin{array}[]{@{}r@{\,}c@{\,}l@{}}\mathrm{val}_{\sigma}(\\{\ s\
\\})&=&\mathrm{val}_{\sigma}(s)\end{array}$ (21)

Here, $s[x\\!\leftarrow\\!x^{\prime}]$ denotes the textual substitution of
program variable $x$ by $x^{\prime}$ in the statement $s$.

####  5.3.2 Trace Composition

Trace composition in rule (13) is unchanged. It will gradually extend the
state with fresh variables, bound to the default value $0$, until the local
variable declarations of the scope have been reduced to an empty list, at
which point the scope is removed and execution can continue as normal.

####  5.3.3 Calculus

The rules are straightforward. We model initialisation by an assignment to the
default value, for which a rule already exists. Actually, this requires a
slight generalisation of the language syntax, such that variable declarations
can occur anywhere in a block, not just at the beginning.

$\begin{array}[]{@{}c@{}}\textsc{\footnotesize(local${}_{1}$)}\\\
\Gamma,\,pc\Rightarrow\tau\left[x^{\prime}:=0;\,\\{s^{\prime}\\}\right]\phi\quad
x^{\prime}\text{ fresh}\quad s^{\prime}=s[x\leftarrow x^{\prime}]\\\
\hline\cr\Gamma,\,pc\Rightarrow\tau\left[\\{x;\,s\\}\right]\phi\end{array}\qquad\qquad\begin{array}[]{@{}c@{}}\textsc{\footnotesize(local${}_{2}$)}\\\
\Gamma,\,pc\Rightarrow\tau\left[s\right]\phi\\\
\hline\cr\Gamma,\,pc\Rightarrow\tau\left[\\{s\\}\right]\phi\end{array}$

###  5.4 Introducing Events and Symbolic Traces

Symbolic traces can contain states in which variables may be bound to unknown
values. A simple case where this become necessary is when WHILE is extended
with a statement to express user input, such that the syntax for statements
from Figure 2 becomes

${s\in\mathit{Stmt}::=\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
input}}}}}}(x)\mid\ \ldots\ .$

For the input-statement, Proposition 2 does not hold, because we do not know
the value of the user input $x$ when locally evaluating the statement. To
represent these unknown values in the local semantics, we use symbolic
variables introduced in Definition 3. Events can be used to introduce a point
of interaction; we define an event type $\textit{inpEv}(Y)$ that captures the
introduction of a symbolic variable $Y$ by an input-statement. The local
evaluation rule for input($x$) can be formalised as follows:

${\begin{array}[]{@{}r@{\,}c@{\,}l@{}}\mathrm{val}_{\sigma}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
input}}}}}}(x))=\\{\emptyset\triangleright\textit{inpEv}_{\sigma}^{\\{Y\\}}(Y)\curvearrowright\sigma[Y\mapsto*][\,x\mapsto
Y]\cdot\mathrm{K}(\mbox{\bottle})\mid Y\not\in\operatorname{dom}(\sigma)\\}\
.\end{array}$ (22)

The trace is well-formed, because the variable $Y$ inside the event is
symbolic.

The composition rule accommodates Proposition 2 by using a concretisation
mapping to concretise the emitted trace. Concretisation captures the actual
user input when the statement is executed in a concrete trace.

$\begin{array}[]{c}\sigma=\mathrm{last}(sh)\quad
pc\triangleright\tau\cdot\mathrm{K}(s^{\prime})\in\mathrm{val}_{\sigma}(s)\quad\rho\text{
concretises }\tau\quad\rho(pc)\text{ consistent}\\\\[1.0pt]
\hline\cr\\\\[-7.0pt] sh,\mathrm{K}(s)\to
sh\mathbin{\ast\ast}\rho({\tau}),\mathrm{K}(s^{\prime})\end{array}$ (23)

The concretisation mapping $\rho$ ensures that the resulting trace
$sh\mathbin{\ast\ast}\rho({\tau})$ is concrete.

The previous composition rule (13) is a special case of this one, when all the
states are concrete (this follows from Proposition 1).

###### Example 16

${\mathbf{Tr}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
input}}}}}}(x),I_{seq})=\\{\langle
I_{seq}\rangle\mathbin{\ast\ast}\textit{inpEv}_{\sigma}^{\\{Y\\}}(Y)\curvearrowright\sigma[Y\mapsto
v][\,x\mapsto v]\mid v\in\mathit{Val}\\}=\\{\langle
I_{seq}\rangle\curvearrowright\textit{inpEv}(v)\curvearrowright
I_{seq}[Y\mapsto v]\curvearrowright I_{seq}[Y\mapsto v,\,x\mapsto v]\mid
v\in\mathit{Val}\\}$. All possible values $v$ may occur as an input. Variable
$Y$ has a concrete value now; $x,\,Y$ are needed to propagate the input value
correctly, for example, in subsequent code of the form “if ($x>0$) then …”.

##### Calculus

The calculus rule directly follows the local evaluation rule (22) by
introducing a fresh variable $Y$ to model the unknown user input. By
definition we have $\sigma_{\ast}(Y)=\ast$, so we do not need this assignment.

${\textsc{\footnotesize(Input)}\quad\begin{array}[]{c}\mathrm{last}(\tau)=\sigma\quad\Gamma,\,pc\Rightarrow\tau\mathbin{\ast\ast}\textit{inpEv}_{\sigma}^{\\{Y\\}}(Y)\left[x:=Y;\,s\right]\phi\quad
Y\text{ fresh}\\\
\hline\cr\Gamma,\,pc\Rightarrow\tau\left[\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
input}}}}}}(x);\,s\right]\phi\end{array}$

Interestingly, the abstract composition rule (23) has no effect on the
calculus, which is already symbolic, but the soundness proof needs to be
adapted.

###  5.5 Procedure Calls

${{{{{{{\begin{array}[t]{r@{\hspace{2pt}}r@{\hspace{2pt}}l}P\in\mathit{Prog}\hskip
2.0&::=\hskip 2.0&\overline{M}\,\\{s\\}\\\ M\in\mathit{Meth}\hskip
2.0&::=\hskip 2.0&m(x)\\{s\\}\\\ s\in\mathit{Stmt}\hskip 2.0&::=\hskip
2.0&\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
skip}}}}}}\mid
x:=e\mid\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
if}}}}}}\leavevmode\nobreak\ e\leavevmode\nobreak\ \\{\leavevmode\nobreak\
s\leavevmode\nobreak\ \\}\mid
s;s\mid\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
while}}}}}}\ e\,\\{\,s\,\\}\\\ \hskip 2.0&\hskip
2.0&\mid\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\ s\leavevmode\nobreak\ ||\leavevmode\nobreak\ s\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}}\mid\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
atomic}}}}}}(s)\mid\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
call}}}}}}(m,e)\end{array}$

Figure 4: Program Syntax with Procedure Calls.

Figure 4 introduces procedure666Historically, it is more common to use the
term _procedure_ , whereas in object-oriented programming the term _method_ is
usual, which is where the LAGC concept originated from. We use both terms
interchangeably. calls with the statement
${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
call}}}}}}(m,e)$: A program is a set of method declarations $\overline{M}$
with main block $\\{s\\}$. We consider $\overline{M}$ to be a _method table_
that is implicitly provided with a program. Each method declaration associates
a unique name $m$ with the statement in its body. To reduce technicalities, we
assume without loss of generality that a method call has one argument and no
return value on which the caller needs to synchronise.777Synchronisation on
return values is discussed in Section 7.3.

In contrast to parallel
${{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
co}}}}}}\ s\leavevmode\nobreak\ ||\leavevmode\nobreak\ s\
\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
oc}}}}}}$ statements, where parallelism is explicit in the program syntax,
procedure calls introduce implicit parallel execution: there is a context
switch between the syntactic call site and the processor, whereupon the call
is executed in parallel. This decoupling has an important consequence:
according to the local evaluation principle, method bodies are evaluated
independently of the call context. This necessitates a new composition rule
that starts the execution of a called method. We also need to ensure that a
method is not executed before it is called, requiring the introduction of
suitable _events_.

####  5.5.1 Local Evaluation

The new events are $\textit{invEv}(m,\mathrm{val}_{\sigma}(e))$ and
$\textit{invREv}(m,\mathrm{val}_{\sigma}(e))$ for a given state $\sigma$.
These events denote the _invocation_ and the _activation_ (also called the
_invocation reaction_) of a method $m$ with argument $e$, respectively. Recall
from Section 2.3 that events inserted into a trace at a state $\sigma$ are
preceded and succeeded by that state. The local evaluation rule (24) for a
call to $m$ with argument $e$ has an empty path condition, inserts an
_invocation_ event $\textit{invEv}(m,\mathrm{val}_{\sigma}(e))$ into the
trace, and continues with the empty continuation. This means that the call is
_non-blocking_ : the code following the call could be executed immediately, if
scheduled. The rule is formalised as follows:

${\begin{array}[]{@{}r@{\,}c@{\,}l@{}}\mathrm{val}_{\sigma}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
call}}}}}}(m,e))=\\{\emptyset\triangleright\textit{invEv}_{\sigma}(m,\mathrm{val}_{\sigma}(e))\cdot\mathrm{K}(\mbox{\bottle})\\}\
.\end{array}$ (24)

####  5.5.2 Trace Composition: Concrete Variant

The concurrency model so far is still very simple: method invocations and
processors are anonymous, there is no way to distinguish between two calls to
the same method: these execute identical code and all executions can be
interleaved. For this reason, it is sufficient to represent continuation
candidates for the next execution step as a multiset $q$. We denote with
“${+}$” the _disjoint_ multiset union. We add a rewrite rule to simplify empty
continuations in the multisets of tasks; this rule is applied exhaustively
when adding tasks in multisets.

$q{+}\\{\mathrm{K}(\mbox{\bottle})\\}\rightsquigarrow q.$

The judgment representing trace extension by one step has the form: $sh,\,q\to
sh^{\prime},\,q^{\prime}$ where $q$, $q^{\prime}$ are multisets of
continuations of the form $\mathrm{K}(s)$.

$\begin{array}[]{c}\sigma=\mathrm{last}(sh)\quad
pc\triangleright\tau\cdot\mathrm{K}(s^{\prime})\in\mathrm{val}_{\sigma}(s)\quad
pc\text{ consistent}\\\\[1.0pt] \hline\cr\\\\[-7.0pt]
sh,q{+}\\{\mathrm{K}(s)\\}\to
sh\mathbin{\ast\ast}\tau,q{+}\\{\mathrm{K}(s^{\prime})\\}\end{array}$ (25)

The difference between rule (13) and rule (25) is that we no longer commit to
one possible continuation, because the continuation code is now located in a
method. Therefore, the rule selects and removes one matching continuation from
the pool $q$, executes it to the next continuation marker, exactly like rule
(13), and then puts the code remaining to be executed back into $q$. We also
need a new composition rule that adds method bodies to the pool $q$.

$\begin{array}[]{c}m(x)\\{s\\}\in\overline{M}\quad\sigma=\mathrm{last}(sh)\quad\mathit{wf}(sh\mathbin{\ast\ast}\textit{invREv}_{\sigma}(m,v))\quad
y\not\in\operatorname{dom}(\sigma)\\\\[1.0pt] \hline\cr\\\\[-7.0pt] sh,q\to
sh\mathbin{\ast\ast}\textit{invREv}_{\sigma}(m,v)\curvearrowright\sigma[y\mapsto
v],q{+}\\{\mathrm{K}(s[x\leftarrow y])\\}\end{array}$ (26)

The rule handles the creation of a new execution thread. We select a method
with body $s$ from table $\overline{M}$ and create a new continuation
$\mathrm{K}(s[x\leftarrow y])$, where the call parameter $x$ is substituted
with a fresh variable $y$ for disambiguation. The new continuation is added to
the pool $q$. Next, we need to record that a new method with argument $v$ has
started to execute, as a consequence of a previous method call. The existence
of this call is ensured by the premise expressing the well-formedness of the
extended trace, which requires an invocation event of the form
$\textit{invEv}(m,v)$ to be present in $sh$. We extend the current trace with
the _invocation reaction_ event888Recall that $\textit{invREv}_{\sigma}(m,v)$
is a triple with two copies of $\sigma$ around $\textit{invREv}(m,v)$.
$\textit{invREv}_{\sigma}(m,v)$ to mark the start of method execution and
record the extension of the current state in which the parameter $y$ has the
value $v$. It remains to formalise well-formedness.

####  5.5.3 Well-Formedness

A trace is well-formed if its events obey certain ordering restrictions.
Whenever a trace $sh$ is extended with an invocation reaction event of the
form $\textit{invREv}(m,v)$, there must be a corresponding invocation event
$\textit{invEv}(m,v)$ in $sh$. This ordering restriction can be captured by
counting the number of occurrences of both event forms in $sh$ using the
comprehension expression $\\#_{sh}({\textit{ev}(\overline{e})})$. In all other
cases, the trace stays well-formed when it is extended with a new event. We
formalise well-formedness as a predicate on traces.

######  Definition 23 (Well-Formedness)

The _well-formedness_ of a concrete trace sh is formalised by a predicate
$\mathit{wf}(\textit{sh})$, defined inductively over the length of sh:

$\begin{array}[t]{r@{\hspace{2pt}}r@{\hspace{2pt}}l}\mathit{wf}(\varepsilon)\hskip
2.0&=\hskip 2.0&true\\\ \mathit{wf}(sh\curvearrowright\sigma)\hskip
2.0&=\hskip 2.0&\mathit{wf}(sh)\\\
\mathit{wf}(sh\curvearrowright\textit{invEv}(m,v))\hskip 2.0&=\hskip
2.0&\mathit{wf}(sh)\\\
\mathit{wf}(sh\curvearrowright\textit{invREv}(m,v))\hskip 2.0&=\hskip
2.0&\mathit{wf}(sh)\wedge\\#_{sh}({\textit{invEv}(m,v)})>\\#_{sh}({\textit{invREv}(m,v)})\end{array}$

The well-formedness predicate is used in the global composition rules to
ensure that only a valid concrete trace for a given program can be generated
during the trace composition. Any trace emitted by the trace composition rules
is well-formed, because it is an invariant established each time a trace is
extended. It is sufficient to define well-formedness on concrete traces,
because in the end it has to hold for them. It follows that well-formedness is
always a simple, decidable property.

####  5.5.4 Global Trace Semantics

######  Definition 24 (Program Semantics with Procedure Calls)

Given a finite program $P$ with a method table $\overline{M}$ and a main block
$s_{main}$. Let $sh_{0},\,q_{0}\rightarrow sh_{1},\,q_{1}\rightarrow\cdots$ be
a maximal sequence obtained by the repeated application of the composition
rules (25)–(26), starting with $\langle
I_{P}\rangle,\,\\{\mathrm{K}(s_{main})\\}$. If the sequence is finite, then it
must have the form

$\langle I_{P}\rangle,\\{\mathrm{K}(s_{main})\\}\to\dots\to
sh,\emptyset\enspace.$

If the sequence is infinite, let $sh=\lim_{i\rightarrow\infty}sh_{i}$. In
either case, $sh$ is a trace of $P$. The set of all such traces is denoted by
$\mathbf{Tr}(P,I_{P})$.

###### Example 17

Consider the following program $P$:

${\begin{array}[t]{l}m(x)\ \\{y:=x;\,x:=x+1\\}\\\
\\{\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
call}}}}}}(m,1);\,z:=2\\}\end{array}$

The method table for this program is $\overline{M}=\\{m(x)\
\\{y:=x;\,x:=x+1\\}\\}$. The evaluation of the main method is as follows:

${{\begin{array}[h]{r@{\hspace{2pt}}r@{\hspace{2pt}}l}\mathrm{val}_{\sigma}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
call}}}}}}(m,1))\hskip 2.0&=\hskip
2.0&\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\textit{invEv}(m,1)\curvearrowright\sigma\cdot\mathrm{K}(\mbox{\bottle})\\}\\\
\mathrm{val}_{\sigma}(z:=2)\hskip 2.0&=\hskip
2.0&\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[z\mapsto
2]\cdot\mathrm{K}(\mbox{\bottle})\\}\\\
\mathrm{val}_{\sigma}(\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
call}}}}}}(m,1);z:=2)\hskip 2.0&=\hskip
2.0&\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\textit{invEv}(m,1)\curvearrowright\sigma\cdot\mathrm{K}(z:=2)\\}\end{array}$

To prepare the evaluation of the method body of $m(x)$ (where $x$ is any
integer):

$\begin{array}[]{r@{\hspace{2pt}}r@{\hspace{2pt}}l}\mathrm{val}_{\sigma}(y:=x)\hskip
2.0&=\hskip
2.0&\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[y\mapsto\mathrm{val}_{\sigma}(x)]\cdot\mathrm{K}(\mbox{\bottle})\\}\\\
\mathrm{val}_{\sigma}(x:=x+1)\hskip 2.0&=\hskip
2.0&\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[x\mapsto\mathrm{val}_{\sigma}(x+1)]\cdot\mathrm{K}(\mbox{\bottle})\\}\\\
\mathrm{val}_{\sigma}(y:=x;x:=x+1)\hskip 2.0&=\hskip
2.0&\\{\emptyset\triangleright\langle\sigma\rangle\curvearrowright\sigma[y\mapsto\mathrm{val}_{\sigma}(x)]\cdot\mathrm{K}(x:=x+1)\\}\end{array}$
(27)

Let $I_{P}$ be the initial state of $P$. We consider the state where the
statement
${\mbox{\leavevmode\lstinline{{\lst@@@set@language\lst@@@set@numbers\lst@@@set@frame\lst@@@set@rulecolor\lst@@@set@frame\lst@@@set@frame\lst@@@set@language{\@listingGroup{ltx_lst_keyword}{\bf
call}}}}}}(m,1)$ in main has already been executed, and explore the possible