# An Abstraction Technique for Verifying Shared-Memory Concurrency +
## 3 Formalisation
### Programs
#### 3.3.6 Process Maps
: _Any process map \(pm\) is defined to be valid, denoted \(\mathsf{valid}_{\mathsf{pm}}(pm)\), if \(\mathsf{valid}_{\mathsf{mc}}(pm(v))\) holds for every \(v\in\mathit{Val}\), with the \(\mathsf{valid}_{\mathsf{mc}}:\mathit{ProcMapEntry}\to\mathit{Prop}\) predicate defined as follows._\[\mathsf{valid}_{\mathsf{mc}}(me)\triangleq \begin{cases}\mathsf{true}&\text{if }\;me= \mathsf{free}\\ \mathsf{valid}_{\mathsf{Q}}(\pi)&\text{if }\;me=\langle P,\Lambda\rangle^{\pi}\text{ for some }P\text{ and }\Lambda\\ \mathsf{false}&\text{if }\;me=\mathsf{inv}\end{cases} \]  
It is not difficult to see that \(\mathbb{1}_{\mathsf{pm}}\) is trivially valid, and that bisimilarity is validity-preserving, i.e., \(\mathsf{valid}_{\mathsf{pm}}(pm_{1})\) and \(pm_{1}\cong_{\mathsf{pm}}pm_{2}\) implies \(\mathsf{valid}_{\mathsf{pm}}(pm_{2})\) for every \(pm_{1}\) and \(pm_{2}\); and likewise for \(\mathsf{valid}_{\mathsf{mc}}\). **Disjointness. ** Two process maps are said to be _disjoint_ if none of their entries are corrupt, and all fractional permissions of their entries are point-wise disjoint, as captured by the following definition. **Definition 25** (Process map disjointness). : _Any two process maps \(pm_{1}\) and \(pm_{2}\) are defined to be disjoint, denoted \(pm_{1}\perp_{\mathsf{pm}}pm_{2}\), if \(pm_{1}(v)\perp_{\mathsf{mc}}pm_{2}(v)\) for every \(v\in\text{Val}\), with the \(\perp_{\mathsf{mc}}\) relation defined as follows._  
\[me_{1}\perp_{\mathsf{mc}}me_{2}\triangleq \begin{cases}\mathsf{valid}_{ \mathsf{mc}}(me_{1})&\text{if }\;me_{2}=\mathsf{free}\\ \mathsf{valid}_{\mathsf{mc}}(me_{2})&\text{if }\;me_{1}=\mathsf{free}\\ \pi_{1}\perp_{\mathsf{Q}}\pi_{2}\wedge\Lambda_{1}=\Lambda_{2}&\text{if }\;me_{1}= \langle P_{1},\Lambda_{1}\rangle^{\pi_{1}}\wedge me_{2}=\langle P_{2},\Lambda_ {2}\rangle^{\pi_{2}}\text{ for some }P_{1}\text{ and }P_{2}\\ \mathsf{false}&\text{otherwise}\end{cases} \]  
The intuition of disjointness is that disjoint process maps can safely be composed without corrupting any of their entries. Disjointness is a symmetric relation and is a congruence with respect to bisimilarity, meaning that \(pm_{1}\perp_{\mathsf{pm}}pm_{2}\) and \(pm_{1}\cong_{\mathsf{pm}}pm_{1}^{\prime}\) and \(pm_{2}\cong_{\mathsf{pm}}pm_{2}\) implies \(pm_{1}^{\prime}\perp_{\mathsf{pm}}pm_{2}^{\prime}\). **Disjoint union. ** The following operation defines the disjoint union of two process map (entries). **Definition 26** (Disjoint union of process maps). : _The disjoint union of two process maps \(pm_{1}\) and \(pm_{2}\) is defined as \(pm_{1}\uplus_{\mathsf{pm}}pm_{2}\uplus\forall v\,pm_{1}(v)\uplus_{\mathsf{mc}}pm _{2}(v)\), with \(\uplus_{\mathsf{mc}}\) defined as follows._  
\[me_{1}\uplus_{\mathsf{mc}}me_{2}\triangleq \begin{cases}me_{1}&\text{if }me_{2}= \mathsf{free}\\ me_{2}&\text{if }me_{1}=\mathsf{free}\\ \langle P_{1}\parallel P_{2},\Lambda_{1}\rangle^{\pi_{1}+\pi_{2}}&\text{if }me_{1}= \langle P_{1},\Lambda_{1}\rangle^{\pi_{1}}\wedge me_{2}=\langle P_{2},\Lambda_ {2}\rangle^{\pi_{2}}\wedge\Lambda_{1}=\Lambda_{2}\\ \mathsf{inv}&\text{otherwise}\end{cases} \]  
Likewise to disjoint union of permission heaps, the composition of incompatible process map entries produces a corrupted inv entry. The free entry is again neutral, whereas inv is absorbing (that is, composing inv with any entry results in inv). Disjoint union is a congruence with respect to bisimilarity, so that \(pm_{1}\cong_{\mathsf{pm}}pm_{2}\) and \(pm_{1}^{\prime}\cong_{\mathsf{pm}}pm_{2}\) implies \(pm_{1}\uplus_{\mathsf{pm}}pm_{2}^{\prime}\)\(pm_{2}\uplus_{\mathsf{pm}}pm_{2}^{\prime}\). **Lemma 6**. : _(The analogous operations on process map entries have the exact same properties. )_  
1. \(pm_{1}\uplus_{\mathsf{pm}}(pm_{2}\uplus_{\mathsf{pm}}pm_{3})\cong_{\mathsf{pm} }(pm_{1}\uplus_{\mathsf{pm}}pm_{2})\uplus_{\mathsf{pm}}pm_{3}\)_._
2. \(pm_{1}\uplus_{\mathsf{pm}}pm_{2}\uplus_{\mathsf{pm}}pm_{2}^{\prime}\)_._
3. \(pm_{1}\uplus_{\mathsf{pm}}pm_{2}\uplus_{\mathsf{pm}}pm_{2}\)_._
4.