# An Abstraction Technique for Verifying Shared-Memory Concurrency +
## 3 Formalisation
### Proof System
#### 3.5.4 Adequacy  
This section defines _program execution safety_ and uses it to define the semantic meaning of program judgments, from which the soundness theorem (i.e., adequacy of the logic) can be formulated. Program execution safety extends on the well-known notion of _configuration safety_ of [34], by adding permission accounting, process-algebraic state, and the machinery introduced earlier in this section.  
First, in order to help connect the models of the program logic to concrete program state, we define a _concretisation function_ for permission heaps in the same style as snapshot heaps.  
**Definition 34** (Concretisation).: _Concretisation of permission heaps is defined as a total function \(\lfloor\cdot\rfloor_{\text{concr}}:\text{PermHeap}\to\text{Heap}\), so that \(\lfloor ph\rfloor_{\text{concr}}\triangleq\lambda v\in\text{Val}\,.\, \lfloor ph(v)\rfloor_{\text{concr}}\), with \(\lfloor ph(v)\rfloor_{\text{concr}}\) defined as_  
\[\lfloor hc\rfloor_{\text{concr}}\triangleq\begin{cases}v&\text{if }\,hc= \langle v\rangle_{\text{std}}^{\pi}\text{ for some }\pi\\ v&\text{if }\,hc=\langle v\rangle_{\text{proc}}^{\pi}\text{ for some }\pi\\ v_{1}&\text{if }\,hc=\langle v_{1},v_{2}\rangle_{\text{act}}^{\pi}\text{ for some }\pi\text{ and }v_{2}\\ \text{undefined}&\text{otherwise}\end{cases}\]The heap concretisation operator constructs (program) heaps out of permission heaps by simply discarding all internal structure regarding process-algebraic models. Only the information relevant for regular program execution is retained. \([\ \cdot\ ]_{\mathsf{snapshot}}\) essentially does the same, but only retains heap cells bound to program abstractions and takes snapshot values whenever possible.  
We now have all the ingredients for defining adequacy. _Program execution safety_ is defined in terms of a predicate \(\mathsf{safe}_{n}(C,ph,pm,s,\mathcal{R},\mathcal{Q})\), stating that \(C\) is _safe_ for \(n\) reduction steps with respect to a permission heap \(ph\), process map \(pm\), two stores \(s\) and \(g\), a resource invariant \(\mathcal{R}\) and postcondition \(\mathcal{Q}\).  
**Definition 35** (Program execution safety).: _The \(\mathsf{safe}_{0}(C,ph,pm,s,g,\mathcal{R},\mathcal{Q})\) predicate always holds, whereas \(\mathsf{safe}_{n+1}(C,ph,pm,s,g,\mathcal{R},\mathcal{Q})\) holds if and only if the following five conditions hold._  
1. _If_ \(C=\mathsf{skip}\)_, then_ \(ph,pm,s,g\models\mathcal{Q}\)_._
2. _For every_ \(ph_{F}\) _and_ \(pm_{F}\) _such that_ \(ph\perp_{\mathsf{hc}}ph_{F}\) _and_ \(pm\perp_{\mathsf{mc}}pm_{F}\)_, it holds that_ \(\mathsf{\sharp ghost}(C,\lfloor ph\uplus ph\,ph_{F}\rfloor_{\mathsf{conc}},pm \uplus pm_{F},s,g)\)_._
3. _For any_ \(v\in\mathsf{acc}(C,s)\) _it holds that_ \(ph(v)\
ot\in\{\mathsf{free},\mathsf{inv}\}\)_._
4. _For any_ \(v\in\mathsf{writes}(C,s)\) _it holds that_ \(\mathsf{full}_{\mathsf{hc}}(ph(v))\)_._
5. _For any_ \(ph_{I}\)_,_ \(ph_{F}\)_,_ \(pm_{I}\)_,_ \(pm_{I}\)_,_ \(pm_{I}\)_,_ \(pm_{I}\)_,_ \(pm_{  
_If \(\mathsf{safe}_{n}(C,ph,pm_{1},s,g,\mathcal{R},\mathcal{Q})\) and \(pm_{1}\cong_{\mathsf{pm}}pm_{2}\), then \(\mathsf{safe}_{n}(C,ph,pm_{2},s,g,\mathcal{R},\mathcal{Q})\)._  
_If \(\mathsf{safe}_{n}(C,ph,pm,s,g,\mathcal{R},\mathcal{Q})\) and \(\mathcal{Q}\models\mathcal{Q}^{\prime}\), then \(\mathsf{safe}_{n}(C,ph,pm,s,g,\mathcal{R},\mathcal{Q}^{\prime})\)._  
1 in Lemma 10 states monotonicity in the sense that being safe for \(n\) reduction steps implies safety for less than \(n\) steps. 2 in Lemma 10 states that process maps can always be replaced by bisimilar ones in safe configurations. Finally, 3 in Lemma 10 states that postconditions may always be weakened.