Skip to main content

Analysing concurrent datatypes in CSP

Supervisor

Suitable for

Computer Science, Part C

Abstract

The 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.