# An Abstraction Technique for Verifying Shared-Memory Concurrency +
## 3 Formalisation
### Proof System
#### 3.5.1 Ghost Operational Semantics  
To establish the refinements between programs and their abstractions, an intermediate semantics is used that administers the states of all active program abstractions. This intermediate semantics is referred to in the sequel as the _ghost operational semantics_. The ghost semantics is expressed as a transition relation \(\leadsto_{\text{ghost}}\subseteq\textit{GhostConf}\) between _ghost configurations_\(\mathfrak{G}=(C,h,pm,s,g)\in\textit{GhostConf}\), which extend program configurations by two extra components, namely:  
* A process map \(pm\in\textit{ProcMap}\) that is used to administer the state of all _active_ (initialised, but not yet finalised) process-algebraic abstractions; and
* An extra store \(g\in\textit{Store}\), referred to as a _ghost store_, as it is used to map variable names to process identifiers in the context of \"ghost\" instructions. The ghost operational semantics uses two stores instead of one, to keep the administration of program data and specification-only (ghost) data strictly separated. Doing so eases establishing that variables referred to in ghost code do not interfere with regular program execution, and vice versa. Ghost reductions essentially describe the _lock-step execution_ of concrete programs (\(\leadsto\) steps) and their abstractions (\(\xrightarrow{a}\) steps). Figure 6 presents an excerpt of the transition rules. This excerpt only contains the reduction rules related to program abstraction; all other rules are essentially the same as those of \(\leadsto\), with the two extra configuration components simply carried over and left unchanged. Recall that the blue colourings are merely visual cues and do not have any special semantical meaning. Clarifying the ghost reduction rules, ghost-proc-init instantiates a new program abstraction and stores it in a free entry in \(pm\). ghost-proc-finish finalises program abstractions that are able to terminate successfully. The rules ghost-act-init, ghost-act-step and ghost-act-end handle the execution of action blocks. Before discussing these, first observe that the ghost semantics maintains an extra component \(m\) in intact\(m\)\(C\) commands, containing _(ghost) metadata_: extra runtime information about the process-algebraic model in whose context the program \(C\) is being executed. Concretely, ghost metadata \(m\) is defined as a quadruple \(m=(a,v,v^{\prime},h)\in\textit{Act}\times\textit{Val}\times\textit{Val}\times \textit{Heap}\), consisting of:  
1. The label \(a\) of the action that is being executed;
2. The input argument \(v\) for this action;The identifier \(v^{\prime}\) of the corresponding process-algebraic model in the process map, in which the action \(a\) is to be executed; and
4. A copy \(h\) of the heap, made when the program started to execute the action block; that is, when the action program was reduced to inact by \(\leadsto\). The ghost-act-INIT reduction rule starts executing an action block by reducing it to an inact program, thereby assembling and attaching ghost metadata. In particular, a copy of the heap is made at this point, so that the ghost-act-end rule for finalising inact programs is able to access the original contents of the heap. This is needed to allow the abstraction to make a matching \(\xrightarrow{\alpha}\) step; in particular to determine the pre-state of such a step. To see how this works, first recall that the process-algebraic state of program abstractions are linked to concrete program state--entries in the heap--via the \(\Lambda\) binders maintained in process maps. Therefore, to be able to make an \(\xrightarrow{\alpha}\) step, the ghost-act-end rule first needs to construct process-algebraic state out of the current program state. This is done using the auxiliary function \(\|\cdot\|:\text{\eminder}\to\text{\em heap}\to\text{\em ProcStore}\) referred to as the _abstract state reification function_. **Definition 31** (Abstract state reification). : \[\|\Lambda\|(h)\triangleq\lambda x\in\text{\em ProcVar}\cdot