# An Abstraction Technique for Verifying Shared-Memory Concurrency +
## 3 Formalisation
### Process-Algebraic Models  
Program abstractions are defined using the following ACP-style [30] process-algebraic specification language, where \(x,y,z,\cdots\in\mathit{ProCVar}\) are _process-algebraic variables_; \(v,w,\cdots\in\mathit{Val}\) are _values_ from an infinite domain \(\mathit{Val}\); and \(a,\cdots\in\mathit{Act}\) are _(process-algebraic) actions_.  
**Definition 1** (Processes).: \[e\in\mathit{ProCExpr} := v\mid x\mid e+e\mid e-e\mid\cdots\] \[b\in\mathit{ProCond} := \mathsf{true}\mid\mathsf{false}\mid\
eg b\mid b\wedge b\mid e=e\mid e <e\mid\cdots\] \[P,Q\in\mathit{Proc} := \varepsilon\mid\delta\mid a(e)\mid?(b)\mid P\cdot Q\mid P+Q\mid P \parallel Q\mid P\mathbin{\bigsqcup}Q\mid\Sigma_{x}\,P\mid b:P\mid P^{*}\]  
Clarifying the different connectives and constructs, \(\varepsilon\) is the _empty process_, which has no behaviour The \(\delta\) process is the _deadlocked process_ which neither progresses nor terminates. Processes of the form \(a(e)\) are _actions_, which model the basic, observable (shared-memory) system behaviours. Actions are parameterised by data, in the form of expressions \(e\). The process \(P\cdot Q\) is the _sequential composition_ of \(P\) and \(Q\), whereas \(P+Q\) is their non-deterministic _choice_. The _parallel composition_ of processes \(P\) and \(Q\) is written \(P\parallel Q\). The process \(P\mathbin{\bigsqcup}Q\) is the _left-merge_ of \(P\) and \(Q\), which is similar in spirit to parallel composition, however \(\mathbin{\bigsqcup}\) insists that the left-most process \(P\) proceeds first. The left-merge is an auxiliary connective commonly used to axiomatise parallel composition [31], by having \(P\mathbin{\bigsqcup}Q=P\mathbin{\bigsqcup}Q+Q\mathbin{\bigsqcup}P\). The process \(\Sigma_{x}\,P\) is the infinite summation \(P[x/v_{0}]+P[x/v_{1}]+\cdots\) over all values \(v_{0},v_{1},...\in\mathit{Val}\). Any summation \(\Sigma_{x}\,P\) is a _binder_ for the summation variable \(x\). In the remainder we assume without loss of generality that all variables bound by summation are unique (since any such  
Figure 1: The annotated Owicki-Gries example (the annotations are coloured blue).  
variables can be renamed to unique ones if this is not yet the case). Sometimes \(\Sigma_{x_{0},\ldots,x_{n}}\,P\) is written to abbreviate \(\Sigma_{x_{0}}\cdots\Sigma_{x_{n}}\,P\). The conditional (guarded) process \(b:P\) behaves as \(P\) if the Boolean condition \(b\) holds, and otherwise behaves as \(\delta\). Finally, \(P^{*}\) is the _repetition_, or _iteration_ of \(P\), and denotes a sequence of zero or more \(P\)'s. The infinite iteration of \(P\) is derived to be \(P^{\omega}\triangleq P^{*}\cdot\delta\). Finally, \(?(b)\) is the _assertive process_, which is very similar to guarded processes: \(?(b)\) is behaviourally equivalent to \(\delta\) in case \(b\) does not hold. However, assertive processes have a special role in our approach: they are the main subject of process-algebraic analysis, as they encode the properties \(b\) to verify, as logical assertions. Moreover, they are a key component in connecting process-algebraic reasoning with deductive reasoning, as their properties can be relied upon in the deductive proofs of programs via the query \(b\) ghost command.