# An Abstraction Technique for Verifying Shared-Memory Concurrency +
## 3 Formalisation
### Programs
#### 3.3.6 Process Maps  
The models of the logic also use _process maps_ in addition to permission heaps, to give a semantic meaning to process ownership predicates \(\mathsf{Proc}_{\pi}\) in the logic. Process maps and their entries are defined as follows, where _binders_\(\Lambda\) are finite partial mappings from process variables to heap locations (i.e., values). These binders are the models for the abstraction binders \(\Pi\) defined earlier in Definition 8. **Definition 22** (Process map entries, process maps, binders). : \[me\in\mathit{ProcMapEntry} ::= \mathsf{free}\mid\langle P,\Lambda\rangle^{\pi}\mid\mathsf{inv}\] \[pm\in\mathit{ProcMap} \triangleq \mathit{Val}\to\mathit{ProcMapEntry}\] \[\Lambda\in\mathit{Binder} \triangleq \mathit{ProcVar}\rightharpoonup_{\mathsf{fin}}\mathit{Val}\]  
Process maps are total mappings from values (identifying program abstractions) to _process map entries_, which are, in turn, inductively defined to one of the following three elements:  
* free, which models _unoccupied_ or _free_ entries in \(pm\). * \(\langle P,\Lambda\rangle^{\pi}\), which is an _occupied_ process map entry. These are used as models for the \(\mathsf{Proc}_{\pi}(E,\widetilde{P},\Pi)\) assertions, where \(E\) identifies the process map entry in \(pm\), and the binder \(\Lambda\) is a model for \(\Pi\). * inv, which denotes an _invalid_, or _corrupted_, process map entry. Likewise to permission heaps, process maps are defined as total functions with entries that can explicitly be free or invalid, as this provides desirable algebraic properties. Corrupted entries represent the erroneous result of taking the disjoint union of two incompatible, non-disjoint entries. The _unit process map_ is defined to be \(\mathbb{1}_{\mathsf{pm}}\triangleq\lambda v\in\mathit{Val}\,.\,\mathsf{free}\), containing free at every entry. We now define several operations and relations on process maps that are analogous to the operations defined earlier for permission heaps, starting with bisimilarity. **Bisimilarity. ** Any two process maps are said to be _bisimilar_, if all their entries are equal point-wise, or contain occupied entries with process components that are bisimilar. **Definition 23** (Process map bisimilarity). : _Two process maps \(pm_{1}\) and \(pm_{2}\) are defined to be bisimilar, denoted \(pm_{1}\cong_{\mathsf{pm}}pm_{2}\), if \(pm_{1}(v)\cong_{\mathsf{mc}}pm_{2}(v)\) for every \(v\in\mathit{Val}\), with the relation \(\cong_{\mathsf{mc}}\) defined as follows._  
\[me_{1}\cong_{\mathsf{mc}}me_{2}\triangleq \begin{cases}\mathsf{true}&\text{if } \;me_{1}=\mathsf{free}\wedge me_{2}=\mathsf{free}\\ P_{1}\cong P_{2}\wedge\Lambda_{1}=\Lambda_{2}\wedge\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}}\\ \mathsf{true}&\text{if }\;me_{1}=\mathsf{inv}\wedge me_{2}=\mathsf{inv}\\ \mathsf{false}&\text{otherwise}\end{cases} \]  
Both \(\cong_{\mathsf{pm}}\) and \(\cong_{\mathsf{mc}}\) are equivalence relations. A notion of bisimilarity of process maps is needed in addition to ordinary equality, since for example disjoint union of process maps is not associative nor commutative with respect to ordinary equality, as opposed to bisimilarity. Moreover, we will later see that the program logic always allows replacing processes \(\widetilde{P}\) inside \(\mathsf{Proc}_{\pi}(X,\widetilde{P},\Pi)\) predicates by bisimilar ones, as discussed earlier. But to handle such replacements at the semantic level, we allow process maps and their entries to be handled up to \(\cong_{\mathsf{pm}}\) and \(\cong_{\mathsf{mc}}\), respectively. **Validity. ** Any process map \(pm\) is said to be _valid_ intuitively if none of \(pm\)'s entries are corrupt and all occupied entries of \(pm\) hold a valid associated fractional permission. **Definition 24** (Process map validity).