# An Abstraction Technique for Verifying Shared-Memory Concurrency +
## 3 Formalisation
### Proof System
#### 3.4.1 Entailment Rules  
Figure 3 presents the structural rules of the program logic. The notation \(\mathcal{P}\dashv\hskip-1.0 pt\vdash\mathcal{Q}\) is a shorthand for both \(\mathcal{P}\vdash\mathcal{Q}\) and \(\mathcal{Q}\vdash\mathcal{P}\), and indicates that the rule can be used in both directions. The rules for the standard connectives are mostly as expected. plain-dupl expresses that plain expressions can freely be duplicated, whereas \(*\)-plain shows that \(*\) has the same meaning as \(\wedge\) in the case of plain assertions. The rule \(*\)-weak shows that our concurrent separation logic is affine (intuitionistic) by allowing to forget about resources. The rules \(*\)-assoc and \(*\)-comm express that the separating conjunction is associative and commutative, respectively, whereas \(*\)-true allows composing any resource with true. The rule true-intro is the introduction rule for true, while false-elim is the elimination rule for false stating that anything can be derived from falsehood. The \(*\)-intro and \(\dashv\)-elim rules show that magic wands can be used similarly to the modus ponens inference rule of propositional logic, with respect to \(*\). The rules \(\forall\)-intro, \(\forall\)-elim, \(\exists\)-intro and \(\exists\)-elim are the standard introduction and elimination rules for universal and existential quantifiers. iter-split-merge enables splitting and merging iterated separating conjunctions along the associated (finite) index set. Clarifying the rules for handling heap ownership; \(\hookrightarrow\)-split-merge expresses that heap ownership predicates \(\hookrightarrow^{\pi}_{t}\) of any type \(t\) may be _split_ (in the left-to-right direction) as well as be _merged_ (right-to-left) along \(\pi\). Note however, that multiple points-to predicates for the same heap location may only co-exist if they have the same ownership type, as indicated by the \(\hookrightarrow\)-incompatible rule. Any heap ownership assertion with an invalid fractional permission associated to it entails false by \(\hookrightarrow\)-invalid Furthermore, the \(*\)-procact-split-merge inference rule states that iterated procact heap ownership predicates can be split into disjoint iterated proc and act predicates, or be merged into one such iteration. together show that \(\approx\) is a congruence relation in the logic for all process-algebraic connectives. The rules \(\approx\)-cond-true and \(\approx\)-cond-false allows eliminating conditionals in any processes (together with the \(\mathsf{Proc}\)-\(\cong\) rule that is). Moreover, \(\approx\)-sum-alt allows singling out a single choice out of a process-algebraic summation of choices. Notice here that one can pick any arbitrary _program_ expression for singling out such a choice, which makes this rule particularly useful. Similarly to heap ownership, any process ownership with an invalid fractional permission entails false by \(\mathsf{Proc}\)-invalid. The rule \(\approx\)-term again makes explicit the intuitive meaning of successful termination, matching Proposition 1. Finally, \(\mathsf{Proc}\)-split-merge allows splitting and merging process ownership predicates in the same style as \(\stackrel{{\tau_{\mathcal{R}}}}{{\rightarrow}}\), to distribute parallel processes over parallel threads. Notably, by splitting a predicate \(\mathsf{Proc}_{\pi_{1}+\pi_{2}}(X,\widetilde{P}_{1}\parallel\widetilde{P}_{2 },\Pi)\) into two, both parts can be distributed over different concurrent threads in the program logic, so that thread \(i\) can establish that it executes as prescribed by its part \(\mathsf{Proc}_{\pi_{i}}(X,\widetilde{P}_{i},\Pi)\) of the abstract model. Afterwards, when the threads join again the remaining partial abstractions can be merged back into a single \(\mathsf{Proc}_{\pi_{1}+\pi_{2}}\) predicate. This system of splitting and merging thus provides a compositional, thread-modular way of verifying that programs meet their abstraction. The logical machinery of this is further discussed in Section 3.4.2.