# An Abstraction Technique for Verifying Shared-Memory Concurrency +
## 6 Related Work  
Significant progress has been made on the theory of concurrent software verification over the last years [1; 2; 3; 4; 5; 51; 52; 53]. This line of research proposes advanced program logics that all provide some notion of expressing and restricting thread interference of various complexity, via _protocols_[54]--formal descriptions of how shared program state is allowed to evolve over time. In our approach protocols have the form of processes. The original work on CSL [24] allows specifying simple thread interference in shared-memory concurrent programs via resource invariants and critical regions. Later, RGSep [55] merges CSL with rely-guarantee reasoning to enable describing more fine-grained inter-thread interference by identifying atomic concurrent actions. Many modern program logics build on these principles and propose even more advanced ways of verifying shared-memory concurrency. For example, TaDa [5] and CaReSL [3] express thread interference protocols through state-transition systems. iCAP [51] and Iris [56] propose a more unified approach by accepting user-defined monoids to express protocols on shared state, together with invariants restricting these protocols. Iris provides reasoning support for proving language properties in Coq, whereas our focus is on proving (concrete) programs correct. In the distributed setting, Disel [6] allows specifying protocols for distributed systems. Disel builds on dependent type theory and is implemented as a shallow embedding in Coq. Even though their approach is more expressive than ours, it has to be used in the context of Coq and thus can be applied only semi-automatically at the moment. [PERSON] et al. [57] present a program logic for message passing concurrency, where threads may communicate over channels using native send/receive primitives. This program logic allows specifying protocols via _contracts_, which are state-machines in the style of Session Types [58] to describe channel behaviour. Our technique is more general however, as the approach of [PERSON] et al. is tailored specifically to reason about basic shared-memory message passing (Section 5 for example demonstrates how a system of message passing can be realised using process-algebraic abstractions). Actor Services [59] is a program logic with assertions to express the consequences of asynchronous message transfers between actors--independent program units that communicate via message passing. The meta-theory of Actor Services has not been proven sound. Most of the related work given so far is essentially theoretical and tend to focus primarily on expressivity--on contributing approaches that are expressive yet not necessarily easy to implement into SMT-based program verifiers like for example VerCors of Viper. In fact, for most of these approaches it is very challenging to implement such automated tool support. Instead, they have to be applied in pen-and-paper style, or in the context of an interactive theorem prover like Coq or Isabelle. Our abstraction approach is different, in the sense that its aim is not to maximise expressivity (for example by integrating into higher-order separation logics, like for example [60]). Instead, we aim for a verification approach that balances expressivity and usability--an approach that is expressive enough to reason about real-world concurrent programs that follow some protocol, while being implementable into automated code verifiers; in this case, VerCors and Viper. Related concurrency verifiers are SmallfootRG [61], VeriFast [7], CIVL [62], Threader [63] and Viper [9; 10]; the latter tool is used as the main back-end of VerCors. SmallfootRG is a memory-safety verifier based on RGSep. VeriFast is a rich toolset for verifying (multi-threaded) Java and C programs using separation logic. The CIVL framework can reason about race-freedom and functional correctness of MPI programs written in C [64; 65]. The reasoning is done via bounded model checking combined with symbolic execution.