# An Abstraction Technique for Verifying Shared-Memory Concurrency +
## 3 Formalisation
### Programs
#### 3.3.2 Process Ownership  
The \(\mathsf{Proc}_{\pi}(E,\widetilde{P},\Pi)\) assertion expresses _ownership_ of a program abstraction that is identified by \(E\), where the abstraction is represented by the process \(\widetilde{P}\). Ownership in this sense means that the thread has knowledge of the existence of the process-algebraic model \(\widetilde{P}\), as well as the right to execute as prescribed by this model. The mapping \(\Pi\) connects the abstract model to the concrete program by mapping the process-algebraic variables in the abstraction to heap locations in the program, as discussed before. And last, the fractional permission \(\pi\) is needed to implement the ownership system of program models. Fractional permissions are only used here to be able to reconstruct the full \(\mathsf{Proc}_{1}\) predicate. We shall later see that \(\mathsf{Proc}_{\pi}\) predicates can be split and merged along \(\pi\) and parallel compositions inside \(\widetilde{P}\), and be consumed in the proof system by action programs.  
Even though reasoning about process-algebraic models is done purely on the level of process-algebraic state, in the program logic it is allowed to mix program state with process-algebraic state. This is indicated by the tilde above the \(\widetilde{P}\), which means that \(P\) can have both program variables and process-algebraic variables. Such processes are called _hybrid processes_ and are defined as follows.  
**Definition 16** (Hybrid expressions, conditions and processes).: \[\widetilde{E}\in H\Sigma pr ::= v\mid x\mid\widetilde{E}+\widetilde{E}\mid\widetilde{E}- \widetilde{E}\mid\cdots\] \[\widetilde{B}\in H\mathsf{Cond} ::= \mathsf{true}\mid\mathsf{false}\mid\
eg\widetilde{B}\mid \widetilde{B}\wedge\widetilde{B}\mid\widetilde{E}=\widetilde{E}\mid\widetilde{ E}<\widetilde{E}\mid\cdots\] \[\widetilde{P},\widetilde{Q}\in H\mathsf{Proc} ::= \varepsilon\mid\delta\mid a(E)\mid?(\widetilde{B})\mid\widetilde{P }\cdot\widetilde{Q}\mid\widetilde{P}+\widetilde{Q}\mid\widetilde{P}\parallel \widetilde{Q}\mid\widetilde{P}\parallel\widetilde{Q}\mid\Sigma_{x}\,\widetilde {P}\mid B:\widetilde{P}\mid\widetilde{P}^{*}\]  
These hybrid processes thus allow mixing process-algebraic reasoning with deductive reasoning using our program logic. The function \(\mathsf{fv}(\widetilde{P})\) is used for obtaining the set of free _process-algebraic_ variables in \(\widetilde{P}\), and \(\mathsf{FV}(\widetilde{P})\) for obtaining all free _program_ variables in \(\widetilde{P}\) (and likewise for \(\widetilde{E}\) and \(\widetilde{B}\)).  
We shall later see that the program logic allows replaces processes \(\widetilde{P}\) inside \(\mathsf{Proc}_{\pi}(E,\widetilde{P},\Pi)\) predicates by bisimilar ones. However, note that one cannot use the standard notion of bisimilarity as defined in Definition 7 for this in case \(\widetilde{P}\) has any program variables occurring freely in it. To resolve this, we include a relation \(\widetilde{P}\approx\widetilde{Q}\) in the assertion language, stating that \(\widetilde{P}\) and \(\widetilde{Q}\) are bisimilar while taking into account any (pure) information that is available from the context. This is further clarified in Section 3.3.7, after we discussed the models of the logic.