Analysing concurrent datatypes in CSP
AbstractThe aim of this project would be to model some concurrent datatypes in CSP, and to analyse them using the model checker FDR. The concurrent datatypes could be some of those studied in the Concurrent Algorithms and Datatypes course. Typical properties to be proved would be linearizability (against a suitable sequential specification) and lock freedom.
Prerequisites: Concurrency and Concurrent Algorithms and Datatypes.
Reading: Analysing Lock-Free Linearizable Datatypes using CSP, Gavin Lowe.