COMP31212: Concurrency and Process Algebra (2012-2013)
This course will provide a systematic treatment of concepts and issues in concurrency. The subject will be introduced via a small process algebra language, FSP, for specifying the concurrent behaviour of finite state processes. The Java language has built-in concurrency constructs and will be used to illustrate implementations of example specifications. Also the FSP language comes with software tools for animation and verification and these will be used in examples.
A wide variety of common concurrency problems will be investigated. Some of the underlying theory of the process algebra FSP and related algebras such as Milner's CCS and Hoare's CSP will be studied.
The course aims to:
Provide students with an understanding of concurrent systems, in particular how to model them using the process algebra FSP and how to implement them using Java.
Study techniques for the analysis of concurrent systems.
Introduce, via a set of case-studies, typical methods for solving concurrency problems.
Allow students to use a suite of tools for analysing FSP systems.
|Programme outcome||Unit learning outcomes||Assessment|
|A1 D6||Have a knowledge and understanding, both practical and theoretical, of the FSP Process Algebra.|
|Have a knowledge and understanding of the difficulties involved in designing and implementing concurrent systems, and the limitations of the FSP modelling approach.|
|A2||Have a knowledge and understanding of the behaviour of concurrent Java programs.|
|A5 B3||Have a knowledge and understanding of solutions to a range of concurrency problems and be able to evaluate the effectiveness of these.|
|B1||Be able to construct models for concurrent systems using FSP.|
|B1||Be able to reason about FSP systems, including analysis of their behaviour, properties and equivalencies.|
|Understand how to use Java concurrency primitives.|
|C5||Be able to translate FSP models to Java implementations for small problems.|
Problems and challenges in concurrency (1 lecture).
Modelling processes and concurrency using FSP
Communicating processes, labelled transition systems (2 lectures).
Concurrency in Java
Threads, constructs, behaviour, interacting multiple threads (3 lectures).
From specification to implementation
Translating FSP to Java (1 lecture).
Semantics and equivalence (3 lectures).
Mutual exclusion, monitors, semaphores (3 lectures)
Deadlock, safety, liveness, fairness (4 lectures).
Readers/writers, message-passing, termination (4 lectures).
Extending the model
Other process algebras (CSP, CSS) (1 lecture).
Exercises/revision (2 lectures)
Title: Concurrency: state models and Java programs (2nd edition)
Author: Magee, Jeff and Jeff Kramer