# An Abstraction Technique for Verifying Shared-Memory Concurrency +
## 3 Formalisation
### Proof System
#### 3.5.5 Semantics of Program Judgments  
The semantics of program judgments is defined in terms of a quintuple \(\Gamma;\mathcal{R}\models\{\mathcal{P}\}\,C\,\{\mathcal{Q}\}\), expressing that \(C\) is safe for any number of reduction steps starting from any state satisfying \(\mathcal{P}\).  
**Definition 36** (Semantics of program judgments).: \(\Gamma;\mathcal{R}\models\{\mathcal{P}\}\,C\,\{\mathcal{Q}\}\) _holds if and only if:_  
1. \(\mathsf{user}(C)\)_, and_
2. _If_ \(\models_{\mathsf{env}}\Gamma\) _and_ \(\mathsf{wf}(C)\)_, then for any_ \(ph,pm,s,g\) _such that_ \(\mathsf{valid}_{\mathsf{ph}}(ph)\) _and_ \(\mathsf{valid}_{\mathsf{pm}}(pm)\) _and_ \(\lfloor ph\rfloor_{\mathsf{snapshot}}\models_{\mathsf{pm}}pm\) _and_ \(pl,pm,s,g\models\mathcal{P}\) _hold, it holds that:_ \[\forall n\.\ \mathsf{safe}_{n}(C,ph,pm,s,g,\mathcal{R},\mathcal{Q})\]  
The underlying idea of the above definition, i.e., having a continuation-passing style definition for program judgments, has first been applied in [40] and has further been generalised in [41; 42]. Moreover, the idea of defining execution safety in terms of an inductive predicate originates from [43]. These two concepts have been reconciled in [34] into a formalisation for the classical CSL of Brookes [23], that has been encoded and mechanically been proven in both Isabelle and Coq. Our definition builds on the latter, by having a refinement between programs and abstractions encoded in safe.  
Observe that only judgments of user programs (i.e., commands free of runtime constructs like \(\mathsf{inatom}\) and \(\mathsf{inact}\)) have a semantic meaning. Also observe that the semantics of program judgments is conditional on the safety of \(\Gamma\). It states that \(C\) executes safely for any number \(n\) of computation steps with respect to any state satisfying \(\mathcal{P}\), only if \(\Gamma\) is safe--that is, only if all process-algebraic models for \(C\) are (assumed to be externally) verified. From the above definition it trivially follows that \(\Gamma;\mathcal{R}\models\{\mathsf{false}\}\,C\,\{\mathcal{P}\}\) for any \(\Gamma\), \(\mathcal{R}\), \(\mathcal{P}\) and user program \(C\). Notice however that \(\Gamma;\mathcal{R}\models\{\mathcal{P}\}\,C\,\{\mathsf{true}\}\) does not hold in general, since \(C\) might be able to fault, for example by having data-races.  
The following main soundness theorem states that verified programs (i.e., programs for which a proof can be derived according to the proof rules given earlier in Figures 4 and 5) are semantically valid (that is, are fault-free, memory-safe, and refine their process-algebraic models).  
**Theorem 4** (Soundness).: \(\Gamma;\mathcal{R}\vdash\{\mathcal{P}\}\,C\,\{\mathcal{Q}\}\)__\(\implies\)__\(\Gamma;\mathcal{R}\models\{\mathcal{P}\}\,C\,\{\mathcal{Q}\}\).  
The soundness proofs of all proof rules have been mechanised using the Coq proof assistant and can be found on the Git repository accompanying this article [19].  
The \(\textsc{ht-proc-update}\) and \(\textsc{ht-proc-query}\) proof rules were the most difficult to prove sound, as their proofs require, among other things, (1) showing that the abstract model can always match the program with a simulating execution step, as well as (2) maintaining the invariant that any process-algebraic abstraction inside the process map is safe with respect to the reified program state. On top of that, the combination of (1) and (2) requires some extra bookkeeping to ensure that the snapshot heaps stored in ghost metadata agree with the snapshot values stored in permission heaps. This additional bookkeeping has been left out of the formalisation presented so far, but the details of this can be studied in the Coq formalisation.