Analysing a Library of Concurrency Primitives using CSP

We carry out an analysis of message-passing concurrency primitives, namely a synchronous channel and an alt (alternation) construct, implemented in Scala. We model these primitives using the process algebra CSP, and analyse them using the model checker FDR. We consider the correctness properties of synchronisation linearisation (informally, that each completed operation execution corresponds to a correct synchronisation) and progressibility (informally, that executions don’t get stuck if they could synchronise): we show how these properties can be captured in CSP. Our initial analysis discovered an error in a previous implementation; our subsequent analysis helped us to produce a correct implementation. It turns out that a direct analysis of the composition of an alt and corresponding channels scales quite poorly. To overcome this, we perform a compositional analysis: we show that a channel and an alt each satisfies a more abstract description; and show that the composition of these abstract descriptions satisfies synchronisation linearisation and progressibility.