# An Abstraction Technique for Verifying Shared-Memory Concurrency +
## 3 Formalisation
### Programs
#### 3.2.9 Operational Semantics  
The denotational semantics of programs is defined in terms of a binary small-step reduction relation \(\leadsto\,\,\subseteq\mathit{Conf}\times\mathit{Conf}\) between program configurations. A program configuration \(\mathfrak{C}=(C,h,s)\in\mathit{Conf}\triangleq\mathsf{Conf}\times\mathit{Conf}\) is called _\(\mathsf{Conf}\)_. **Definition 14** (Basic programs, well-formed programs). : _Any command \(C\) is defined to be a user-program, denoted \(\mathsf{user}(C)\), if,_Cmd \(\times\) Heap \(\times\) Store_ is a triple, consisting of a command \(C\) as well as a _heap \(h\)_ that models shared memory, and a store \(s\in\)_Store_ that models thread-local memory. Any program configuration of the form \((\texttt{skip},h,s)\) is defined to be _final_ or _terminated_. Heaps \(h\in\) Heap \(\triangleq\) Val \(\rightharpoonup_{\text{fin}}\) Val_ are defined to be finite partial mappings from values to values. Heap locations are themselves values, so that they can be assigned to, and read from, local variables, and thus be handled as any value. The function \(\text{dom}:\) Heap \(\to\) 2\({}^{\textit{Val}}\) denotes the _mapped domain_ of a given heap, so that \(\text{dom}(h)\triangleq\{v\mid h(v)\
eq\text{undefined}\}\). **Definition 11** (Small-step operational semantics of programs). :  
\(\sim\)-ASIGN  
\((X:=E,h,s)\leadsto(\texttt{skip},h,s[X\mapsto[\![E]\! ]s])\)  
\(\sim\)-WRITE  
\(\frac{v\in\text{dom}(h)}{([E_{1}]:=E_{2},h,s)\leadsto(\texttt{skip},h[v\mapsto[ \![E_{2}]\! ]s],s)}\)  
_where \(v=[\![E_{1}]\! ]s\)_  
\(\sim\)-ALLOC  
\(\frac{v\
ot\in\text{dom}(h)}{(X:=\texttt{alloc}\,E,h,s)\leadsto(\texttt{skip },h[v\mapsto[\![E]\! ]s],s[X\mapsto v])}\)  
\(\sim\)-DISPOSE  
\(\sim\)-SEQ-L  
\(\frac{(C_{1},h,s)\leadsto(C_{1}^{\prime},h^{\prime},s^{\prime})}{(C_{1};C_{2},h,s)\leadsto(C_{1}^{\prime},C_{2},h^{\prime},s^{\prime})}\)  
\(\sim\)-IF-TRUE  
\(\sim\)-IF-FALSE  
\(\frac{[\![B]\! ]s}{(\texttt{if}\ B\ \texttt{then}\ C_{1}\ \texttt{else}\ C_{2},h,s)\leadsto(C_{1},h,s)}\)  
\(\sim\)-WHILE  
\(\sim\)-PAR-L  
\(\sim\)-PART-R  
\(\sim\)-locked\((C_{2})\)  
\(\frac{(C_{1},h,s)\leadsto(C_{1}^{\prime},h^{\prime},s^{\prime})}{(C_{1}\ \ \|\ C_{2},h,s)\leadsto(C_{1}^{ \prime}\ \|\ C_{2},h^{\prime},s^{\prime})}\)  
\(\sim\)-PAR-SKIP  
\((\texttt{skip}\ \|\ \texttt{skip},h,s)\leadsto(\texttt{skip},h,s)\)  
\(\sim\)-INATOM-step  
\(\frac{(C,h,s)\leadsto(C^{\prime},h^{\prime},s^{\prime})}{(\texttt{inatom}\,C,h,s)\leadsto(\texttt{inatom}\,C^{\prime},h^{\prime},s^{\prime})}\)  
\(\sim\)-PROC  
\((X:=\text{process}\ (\lambda x.P)(E)\ \texttt{over}\ \Pi,h,s)\leadsto(\texttt{skip},h,s)\)  
\(\sim\)-ACT  
\(\sim\)-inACT-STEP  
\((\texttt{action}\ E\ a(E^{\prime})\ \texttt{do}\ C,h,s)\leadsto(\texttt{inact}\ C,h,s)\)  
\(\sim\)-INACT-SKIP  
\(\sim\)-INACT-SKIP  
\((\texttt{inact}\ \texttt{skip},h,s)\leadsto(\texttt{skip},h,s)\)  
\(\sim\)-Query  
\((\texttt{query}\ E,h,s)\leadsto(\texttt{skip},h,s)\)Most of the transition rules are standard; see for example [34]. The _update_ notation \(s[X\mapsto v]\) defines a store that is equal to \(s\), except that \(X\) is mapped to \(v\). A similar notation is used for heaps, namely \(h[v_{1}\mapsto v_{2}]\). Moreover, the notation \(h\setminus v\) denotes the _removal_ of the entry at \(v\) in \(h\). An interesting aspect of the operational semantics is that atomic programs are executed using a small-step reduction strategy (via \(\leadsto\)-inatom-step and \(\leadsto\)-inatom-skip), rather than a big-step execution, which is more customary. This is done for technical reasons: it simplifies the establishment of a simulation/refinement between programs and their models. Consequently, we use a notion of a _locked program_ to define the transition rules for atomic programs. Any command \(C\) is said to be _(globally) locked_ if \(C\) executes an atomic program, i.e., if \(C\) has inatom\(C^{\prime}\) as a subprogram for some \(C^{\prime}\). **Definition 12** (Locked programs).