# An Abstraction Technique for Verifying Shared-Memory Concurrency +
## 3 Formalisation
### Programs
#### 3.3.1 Heap Ownership  
The assertion \(E_{1}\overset{\iota\pi}{\rightarrow}_{t}E_{2}\) is the _heap ownership assertion_ and expresses that the heap contains the value represented by the expression \(E_{2}\) at heap location \(E_{1}\). Moreover, \(\pi\) and \(t\) together determine the access rights to this heap location. In more detail, depending on the ownership type \(t\), the \(\overset{\pi}{\rightarrow}_{t}\) ownership predicates express different access rights to the associated heap location:  
* _Standard heap ownership_. \(E_{1}\overset{\iota\pi}{\rightarrow}_{\mathsf{std}}E_{2}\) is the _standard heap ownership predicate_ from (intuitionistic) separation logic that provides read-access whenever \(0<\pi<1\), and write-access in case \(\pi=1\). Moreover, the subscript std indicates that the associated heap location \(E_{1}\) is _not_ bound to any process-algebraic model. We say that a heap location \(v\in\mathit{Val}\) is _bound by_, or _subject to_, a program abstraction, if there is an active program abstraction with a binder \(\Pi\) that contains a mapping to \(v\), that is, \(v\in\mathsf{dom}(\Pi)\). * _Process heap ownership_. \(E\overset{\pi}{\hookrightarrow}_{\mathsf{proc}}E^{\prime}\) is the _process heap ownership predicate_, which indicates that the heap location at \(E\) is bound by an active process-algebraic abstraction, but in a purely _read-only_ manner. More precisely, \(\overset{\pi}{\hookrightarrow}_{\mathsf{proc}}\) assertions exclusively grant read-access, even in case \(\pi=1\). * _Action heap ownership_. \(E\overset{\pi}{\hookrightarrow}_{\mathsf{act}}E^{\prime}\) is the _action heap ownership predicate_, which indicates that the heap location \(E\) is bound by an active process-algebraic model, and is used in the context of an action block, in a _read/write_ manner. Observe that action points-to assertions \(\overset{\pi}{\hookrightarrow}_{\mathsf{act}}\) essentially give the same access rights as \(\overset{\iota\pi}{\rightarrow}_{\mathsf{std}}\) assertions. Nevertheless, they are both needed, to be able to distinguish between bound and unbound heap locations in the logic. For example, the program logic must not allow to deallocate memory that is currently bound to (protected by) an active process-algebraic model, as this would be unsound. Moreover, even though \(\overset{\iota\pi}{\rightarrow}_{\mathsf{proc}}\) predicates never grant write access, we will later see that the proof system allows \(\overset{\iota\pi}{\rightarrow}_{\mathsf{proc}}\) predicates to be upgraded to \(\overset{\iota\pi}{\rightarrow}_{\mathsf{act}}\) inside action blocks, and \(\overset{\iota\pi}{\rightarrow}_{\mathsf{act}}\) again provides write access when \(\pi=1\). More precisely, \(E\overset{1}{\hookrightarrow}_{\mathsf{proc}}E^{\prime}\) predicates grant the _capability to regain write access to \(E\)_, in the context of an action program. This system of upgrading enforces that all modifications to \(E\) happen in the context of action\(E_{abstr}\)\(a(E^{\prime}_{abstr})\) do \(C\) commands, so that the modifications are protected and can be recorded by the program abstraction identified by \(E_{abstr}\), as the action \(a\). In addition to these three heap ownership predicates, we derive a fourth such predicate, called the _process-action heap ownership predicate_. This ownership predicate is equivalent to \(\overset{\iota\pi}{\rightarrow}_{\mathsf{act}}\) only if \(\pi\) denotes write access, and otherwise it is equivalent to \(\overset{\iota\pi}{\rightarrow}_{\mathsf{proc}}\). **Definition 15** (Process-action heap ownership). : \[E_{1}\overset{\iota\pi}{\rightarrow}_{\mathsf{procact}}E_{2}\triangleq \begin{cases}E_{1}\overset{\iota\pi}{\rightarrow}_{\mathsf{act}}E_{2}&\text{ if }\pi=1\\ E_{1}\overset{\iota\pi}{\rightarrow}_{\mathsf{proc}}E_{2}&\text{ otherwise}\end{cases} \]  
This derived predicate is for later use, in the proof system of our program logic.