# An Abstraction Technique for Verifying Shared-Memory Concurrency +
## 3 Formalisation
### Proof System
#### 3.5.3 Preservation of Process Execution Safety  
As already hinted upon in the preamble of this section, establishing soundness of the program logic requires maintaining an invariant stating that all active program abstractions retain their execution safety throughout program execution, with respect to Definitions 5 and 6. Since process maps are used to administer the status of all active program abstractions, we lift the notion of process configuration safety (Definition 5) to _safety of process maps_. Process map safety is expressed in terms of judgments of the form \(h\models_{\text{\sf pm}}pm\) stating that _pm_ is _safe_ if all process-algebraic models stored in _pm_ execute safely with respect to Definition 5 together with a process store that is constructed (reified) from \(h\). **Definition 32** (Process map safety). : \[h\models_{\text{\sf pm}}pm\ \ \ \forall v\in\mathit{Val}\,.\,h\models_{\text{\sf mc}}pm(v)\]  
_where \(h\models_{\text{\sf mc}}mc\) is defined by case distinction on \(mc\), so that_  
\[h\models_{\text{\sf mc}}me\ \ \ \begin{cases}\text{\sf true}&\text{if }\ m=\text{\sf free}\\ \text{\sf$\bigvee$}(P,\|\Lambda\|(h))&\text{if }\ m=\langle P,\Lambda\rangle^{\pi}\ \text{ for some }\pi\\ \text{\sf false}&\text{if }\ m=\text{\sf inv}\end{cases} \]  
Free process cells are always safe whereas corrupted entries \(\text{\sf inv}\) are never safe. Moreover, both \(\models_{\text{\sf pm}}\) and \(\models_{\text{\sf mc}}\) are closed under bisimilarity of process maps and their entries, respectively. **Lemma 9**. : \[\text{1. \quad}\text{If }h\models_{\text{\sf pm}}pm\text{and }pm\cong_{\text{\sf pm}}pm\text{, }pm^{\prime}\text{, then }h\models_{\text{\sf pm}}pm^{\prime}\text{.}\]
2. \[\text{If }h\models_{\text{\sf mc}}me\text{and }me\cong_{\text{\sf mc}}me^{\prime}\text{, then }h\models_{\text{\sf mc}}me^{\prime}\text{.}\]  
In a moment we will also define a notion of execution safety for commands. This notion of _program execution safety_ maintains the aforementioned invariant that \(h\models_{\text{\sf pm}}pm\text{ always holds throughout program execution, where }h\) and \(pm\) are constructed from the current state, at every execution step. This invariant is needed to establish soundness of the HT-PROC-QUERY proof rule. However, one must be careful on how to exactly state this invariant, to allow re-establishing it after every computation step. In most cases re-establishing the invariant is straightforward. For example, \(h\models_{\text{\sf pm}}pm\text{can be re-established after initialising a new program abstraction using the HT-proc-init proof rule, by Definition 6 and by the structure of that proof rule. The invariant can also trivially be re-established after finalising an abstraction using HT-proc-FINISH, as the abstraction is then no longer active and thereby removed from _pm_. However, computation steps that involve heap writing (i.e., handling of \([E]:=E^{\prime}\) programs) may be problematic, as illustrated below. **Technicality 1** (Potential problems due to heap writing). : _To see the potential problem, consider the following code snippet._\(\{\text{{P}ro}_{\pi}(E,\text{reset}\cdot\widetilde{P}+\widetilde{Q},\{x\mapsto E ^{\prime}\})\ast\cdots\}\)  
\(\llbracket E^{\prime}\rrbracket\)s. Moreover, the process map \(\pi\) has not been changed, since the action program (lines 5-8) has not fully been executed yet. Nevertheless, \(h[\llbracket E^{\prime}\rrbracket s\mapsto-2]\models_{\text{pm}}pnn\) may now be violated, as the reset action can no longer be performed, since \(x=-2\) after reification, while reset's guard requires \(x\) to be positive. The root of the problem is that the invariant should not necessarily have to hold during intermediate reduction steps while executing action programs, but only at the pre- and poststate of such programs. Program execution safety will solve this by making a _snapshot of the heap_ every time an action program is being started on (likewise to ghost-act-init), and expressing the invariant over these snapshot heaps.