# An Abstraction Technique for Verifying Shared-Memory Concurrency +
## 3 Formalisation
### Programs
#### 3.3.5 Permission Heaps  
The models of our program logic use _permission heaps_ to give a semantic meaning to heap ownership. Permission heaps and their heap cells are defined as follows, and are slightly richer than ordinary program heaps \((\mathit{Heap})\) to be able to administer the access permissions and the different ownership types. **Definition 18** (Permission heap cells, Permission heaps). : \[\mathit{hc}\in\mathit{PermHeapCell} ::=\mathsf{free}\mid\langle v\rangle_{\mathsf{std}}^{\pi}\mid \langle v\rangle_{\mathsf{proc}}^{\pi}\mid\langle v_{1},v_{2}\rangle_{ \mathsf{act}}^{\pi}\mid\mathsf{inv}\] \[\mathit{ph}\in\mathit{PermHeap} \triangleq\mathit{Val}\to\mathit{PermHeapCell}\]  
Permission heaps \(\mathit{ph}\) are defined to be total functions from values (representing heap locations) to _permission heap cells_, \(\mathit{hc}\), which in turn are inductively defined to be one of the following:  
* free, which is an _unoccupied heap cell_. * \(\langle v\rangle_{\mathsf{std}}^{\pi}\), which is a _standard heap cell_ that stores the value \(v\in\mathit{Val}\). Standard heap cells are the models of the standard heap ownership predicates, \(\stackrel{{\pi}}{{\longrightarrow}}_{\mathsf{std}}\). * \(\langle v\rangle_{\mathsf{proc}}^{\pi}\), which is a _process heap cell_ that stores the value \(v\). These are used as models of the \(\stackrel{{\pi}}{{\longrightarrow}}_{\mathsf{proc}}\) ownership predicates. * \(\langle v_{1},v_{2}\rangle_{\mathsf{act}}^{\pi}\), which is an _action heap cell_ that stores the value \(v_{1}\). Action heap cells are used as the models for the \(\stackrel{{\pi}}{{\longrightarrow}}_{\mathsf{act}}\) predicates. Moreover, action heap cells store a second value \(v_{2}\). This extra value is maintained for technical reasons, to help in establishing soundness of the program logic. The value \(v_{2}\) is referred to as a _snapshot value_: a copy of the original value stored by the heap cell, that is made when an action block was entered. * inv, which is an _invalid_, or _corrupted_, permission heap cell. Note that, unlike program heaps, permission heaps are defined to be total functions, where the heap cells have an explicit notion of being free. This is done to give permission heaps and their cells nicer algebraic properties. The _unit permission heap_ is defined to be \(\mathbb{1}_{\mathsf{ph}}\triangleq\lambda v\in\mathit{Val}\,.\) free, containing free at every entry. Furthermore, permission heap cells also have an explicit notion of being invalid. Invalid heap cells inv represent the erroneous result of composing two incompatible heap cells. We now define several operations on permission heaps. **Validity. ** Any permission heap \(\mathit{ph}\) is defined to be _valid_ if the permissions of all \(\mathit{ph}\)'s heap cells are valid, where free is always valid and inv is never valid. **Definition 19** (Validity of permission heaps). : _A permission heap ph is defined to be valid, written \(\mathsf{valid_{ph}}(ph)\), if \(\mathsf{valid_{hc}}(ph(v))\) holds for every \(v\in\mathit{Val}\), where the \(\mathsf{valid_{hc}}\) predicate is defined as follows._  
\[\mathsf{valid_{hc}}(hc)\triangleq \begin{cases}\mathsf{true}&\text{if }\ hc= \mathsf{free}\\ \mathsf{valid_{Q}}(\pi)&\text{if }\ hc=\langle v\rangle_{\mathsf{std}}^{\pi} \lor hc=\langle v\rangle_{\mathsf{proc}}^{\pi}\lor\langle v,v^{\prime} \rangle_{\mathsf{act}}^{\pi}\ \text{ for some }v,v^{\prime}\\ \mathsf{false}&\text{if }\ hc=\mathsf{inv}\end{cases} \]  
**Disjointness. ** Two permission heaps \(ph_{1}\) and \(ph_{2}\) are _disjoint_ if all their heap cells are pairwise _compatible_ and their underlying permissions are disjoint. **Definition 20** (Disjointness of permission heaps). : _Two permission heaps, \(ph_{1}\) and \(ph_{2}\), are disjoint, denoted \(ph_{1}\perp_{\mathsf{ph}}ph_{2}\), if \(ph_{1}(v)\perp_{\mathsf{hc}}ph_{2}(v)\) holds for every \(v\in\mathit{Val}\), where the \(\perp_{\mathsf{hc}}\) relation is defined as follows._  
\[hc_{1}\perp_{\mathsf{hc}}hc_{2}\triangleq