# An Abstraction Technique for Verifying Shared-Memory Concurrency +
## 3 Formalisation
### Proof System
#### 3.4.4. Process Ownership  
Figure 5 gives the Hoare rules for introducing, eliminating and updating process-algebraic abstractions. The ht-proc-init rule handles initialisation of an abstract model \(P\) with input parameter \(y\), over a set of heap locations as specified by \(\Pi\). This rule requires _standard_ heap write ownership for any heap location that is to be bound by \(P\) according to \(\Pi\), and these are converted to \(\xint_{\mathsf{proc}}\). Moreover,  
Figure 5. The extended proof rules related to handling process-algebraic models. HT-PROC-INIT requires that the precondition \(B\) of \(P\) holds, which is constructed from \(\widetilde{B}\) by replacing all process variables \(x_{i}\) by the values \(E_{i}\) at the corresponding heap locations as specified by \(\Pi\). (Here we slightly abuse notation for ease of presentation. In the proof rule, we write \(\widetilde{B}[x_{i}/E_{i}]_{\forall i\in I}\) for converting a condition \(\widetilde{B}\) to a condition over only program variables, by substituting all free process variables \(x_{i}\) occurring in \(\widetilde{B}\) by a program expression \(E_{i}\). However, in our Coq formalisation we of course have a special operation for such conversions.) A \(\mathsf{Proc}_{1}\) predicate with full permission is ensured, giving the current thread full ownership of the abstraction. The HT-PROC-UPDATE rule handles updates to program abstractions, by performing an action \(a(E^{\prime})\) in the context of an action \(E\)\(a(E^{\prime})\) do \(C\) program. This rule imposes four preconditions on handling action programs. First, a predicate of the form \(\mathsf{Proc}_{\pi}(E,a(E^{\prime})\cdot\widetilde{P}+\widetilde{Q},\Pi)\) is required for some \(\pi\). In particular, the process component must be of the form \(a(E^{\prime})\cdot\widetilde{P}+\widetilde{Q}\) and therewith allow performing the \(a\) action. After performing \(a\) the process will be reduced to \(\widetilde{P}\), and \(\widetilde{Q}\) will be discarded as the choice is made not to follow execution as prescribed by \(\widetilde{Q}\). To get processes in the required format, the entailment rules in Figure 3 can be used together with the bisimulation equivalences given earlier in Figure 2. To give an example, processes of the form \(a(E^{\prime})\cdot\widetilde{P}\) can always be rewritten to \(a(E^{\prime})\cdot\widetilde{P}+\delta\) to obtain the required choice. Second, \(\stackrel{{\pi}}{{\rightarrow}}\!\! Our definition of execution safety extends the well-known inductive definition of configuration safety of Vafeiadis [34] by adding machinery to handle process-algebraic abstractions. The most important extension is a _simulation argument_ between concrete program executions (with respect to \(\leadsto\)) and the executions of all active models (with respect to \(\xrightarrow{\alpha}\)). However, as the reduction steps of these two semantics do not directly correspond one-to-one, this simulation is established via an intermediate instrumented semantics referred to as the _ghost operational semantics_. This intermediate semantics is defined in Section 3.5.1 in terms of _ghost transitions_\(\leadsto\)_ghost that essentially define the lock-step execution of program transitions \(\leadsto\) and the transitions \(\xrightarrow{\alpha}\) of their abstractions. Our definition of _\"executing safely for \(n\) execution steps\"_ includes that all \(\leadsto\) steps can be simulated by \(\leadsto\)ghost steps, and vice versa, for \(n\) execution steps. Thus, the end-result is a _refinement_ between programs and their abstractions. In addition to establishing such refinements, our definition of execution safety must ensure that the ht-proc-query proof rule is sound. In other words, it must allow relying on any assertions embedded in the process-algebraic models in a sound manner, as these are (assumed to be) verified externally.