# An Abstraction Technique for Verifying Shared-Memory Concurrency +
## 3 Formalisation
### Proof System
#### 3.5.2. Faulting Ghost Configurations  
In addition to faulting program configurations (Definition 13) we also define a fault semantics for ghost configurations. This _ghost fault semantics_ is expressed in terms of a predicate \(\dot{\iota}_{\mathsf{ghost}}(\mathfrak{G})\) over ghost configurations \(\mathfrak{G}\). Figure 7 gives an excerpt of the rules. Only the rules related to specification-only constructs are shown. All other rules are essentially the same as those of Definition 13. We shall later show and prove properties that connect the two faulting semantics.  
Clarifying the ghost fault semantics; the initialisation of any process-algebraic model faults if there is no free entry available in _pm_ (by \(\dot{\iota}_{\mathsf{ghost}}\)-PROC-FULL). The finalisation of program abstractions can fault if the corresponding entry in the process map is (1) either unoccupied or invalid (\(\dot{\iota}_{\mathsf{ghost}}\)-PROC-FINISH-1), or (2) contains a process-algebraic abstraction that is unable to successfully terminate (by the rule \(\dot{\iota}_{\mathsf{ghost}}\)-PROC-FINISH-2). Reductions within action blocks \(\mathsf{inact}\;m\;C\) may fault if (1) \(m\) does not refer to an abstraction (\(\dot{\iota}_{\mathsf{ghost}}\)-\(\mathsf{act}\)-SKIP-1), or (2) the abstraction relies on process variables that have an incorrect binding (by the rule \(\dot{\iota}_{\mathsf{ghost}}\)-\(\mathsf{act}\)-SKIP-2), or (3) the process is not able to make a matching step (\(\dot{\iota}_{\mathsf{ghost}}\)-\(\mathsf{act}\)-SKIP-3), or (4) the subprogram \(C\) is able to fault (by \(\dot{\iota}_{\mathsf{ghost}}\)-\(\mathsf{act}\)-STEP). Any query program can fault under similar conditions as those of action programs.  
The ghost semantics enjoys the same progress property as the standard operational semantics.  
**Theorem 3** (Progress of \(\leadsto_{\mathsf{ghost}}\)).: _For any ghost configuration \(\mathfrak{G}\) for which \(\
eg\dot{\iota}_{\mathsf{ghost}}(\mathfrak{G})\) holds, either \(\mathfrak{G}\) is final, or there exists a \(\mathfrak{G}^{\prime}\) such that \(\mathfrak{G}\leadsto_{\mathsf{ghost}}\mathfrak{G}^{\prime}\)._  
Moreover, it is quite straightforward to establish a _forward simulation_ between \(\leadsto\) and \(\leadsto_{\mathsf{ghost}}\). A matching backward simulation is ensured by the soundness argument of the program logic, as is customary for establishing refinements [39].  
Figure 7. An excerpt of the fault semantics of ghost configurations.  
**Lemma 8** (Forward simulation).: _The standard operational semantics and the fault semantics of programs are embedded in the ghost operational semantics and ghost fault semantics, respectively:_  
1. _If_ \((C,h,pm,s,g)\leadsto_{\text{\sf ghost}}(C^{\prime},h^{\prime},pm^{\prime},s^{ \prime},g^{\prime})\)_, then_ \((C,h,s)\leadsto(C^{\prime},h^{\prime},s^{\prime})\)_._
2. _If_ \(\dot{\iota}(C,h,s)\)_, then also_ \(\dot{\iota}_{\text{\sf ghost}}(C,h,pm,s,g)\)_, for any pm and_ \(g\)_._  
The above theorem also shows that the ghost fault semantics extends \(\dot{\iota}\). The soundness argument of the program logic establishes that verified programs do not fault with respect to \(\leadsto_{\text{\sf ghost}}\), and thus also do not fault with respect to \(\leadsto\) by the above Lemma.