# An Abstraction Technique for Verifying Shared-Memory Concurrency +
## 1 Introduction
### Motivation  
Reasoning about complex concurrent program behaviours is only practical if conducted at a suitable level of abstraction that hides implementation details that are irrelevant for the properties to prove. Furthermore, any real concurrent programming language with shared memory, threads and locks, has only very little algebraic behaviour. In contrast, _process algebras_ offer an abstract, mathematically elegant way of expressing program behaviour. Process algebras have been used widely in the past for modelling and analysing the behaviour of concurrent programs at an adequate level of abstraction [20; 21]. Our approach therefore uses a process algebra as a language for _specifying_ program behaviour. Such a specification can be seen as a model, the properties of which can additionally be checked (say by interactive theorem proving, or by model checking against temporal logic formulas, which can be seen as even more abstract behavioural specifications). The main difficulty of this approach is dealing with the typical abstraction gap between program implementations and their abstract models. The unique contribution of our approach is that it bridges this gap by providing a deductive technique for formally linking programs with their process-algebraic models. These formal links preserve _safety_ properties [22]; we leave the preservation of liveness properties for future work.  
The key idea of the approach rests in the use of concurrent separation logic (CSL) to reason not only about data races and memory safety, which is standard [23; 24], but also about process-algebraic models (that is, specified program behaviours), viewing the latter as _resources_ that can be split and consumed. This results in a modular and compositional approach to establish that a program behaves as specified by its abstract model. Our approach is formally justified by (mechanically proven) correctness results stating that any verified program is a _refinement_ of its abstract, process-algebraic model.  
Process-algebraic models are composed out of individual _actions_ that abstract atomic behaviours of program components. Our approach allows specifying program components to follow a particular sequence/pattern of actions--a protocol. One can then reason about the interaction behaviour of different program components by reasoning about the composition of their models, for example by using a model checker for process algebra, like mCRL2 [25]. This approach of specifying the interactions of program components is different from classical Hoare logic, which is purely transformational in the sense that it considers verified (terminating) program components essentially as transformers from states satisfying the specified precondition to states satisfying the specified postcondition.  
A benefit of our combined approach compared to model checking is that it allows reasoning soundly about both data and control-oriented properties in a single framework. Model checkers typically specialise in reasoning about temporal, control-oriented specifications (e.g., send actions must always be matched by a recv), and generally have limited support for handling data due to the risk of state-space explosions. Hoare logic based techniques, on the other hand, tend to specialise in reasoning about data specifications (e.g., a sorting function should yield a sorted permutation of its input), and are typically limited in their capabilities to reason about control-flow properties. Since realistic concurrent systems often deal with both data and control-flow, it is beneficial to be able to reason about both in a single framework. Additionally, our technique addresses the typical \"abstraction gap\" problem of model checking: is the model actually a faithful abstraction of the modelled system? We propose techniques to formally link programs to their abstract models, allowing one to prove that all program behaviours that should be captured by the abstract model are indeed soundly abstracted.