Compiling shared variable programs into CSP
Andrew William Roscoe · 2009
We present a compiler from a simple shared variable language into CSP. This allows the application of CSP-based tools such as FDR when analysing programs written in the other language. The translation into CSP makes it easy to be flexible about the semantics of execution, most particularly the amount of atomicity that is enforced. We examine ways available to translate specifications we may wish to prove into the refinement checks supported by FDR, in particular looking at ways of proving liveness specifications under fairness assumptions. Various examples are given, including mutual exclusion algorithms. Keywords— CSP; FDR; shared variable; compilation; mutual exclusion; model checking; fairness