The Theory and Practice of Concurrent Programming

Module aims

This course focuses on the theory and practice of concurrent programming, in order to familiarise the students with a range of modern concurrent programming models, and with the challenges of correct concurrent programming. It is divided into two parts: a largely practical part that gives an overview of shared memory and message passing concurrency in a variety of programming languages, and a more theoretical part that treats shared memory concurrency from the ground up, covering low-level topics such as hardware memory models, primitives for shared-memory concurrency, building up towards higher-level synchronisation techniques such as locks, mutexes and transactional memory. Throughout the course, a main objective is to reinforce correct concurrent programming through the use of tools, formal specification and verification techniques.

Learning outcomes

Upon successful completion of this module you will be able to:

  • write correct and efficient concurrent software in modern programming languages using a range of concurrency models
  • evaluate the differences between, and strengths and weaknesses of, a variety of concurrency models
  • explain the architectural mechanisms for supporting shared memory concurrency
  • formalise the semantics of shared memory concurrency
  • specify, test and verify properties of concurrent systems using state-of-the-art practical tools and formal methods

Module syllabus

The course will be split into two halves. One half will focus on practical concurrent programming in a variety of programming languages using a range of paradigms. It will cover:

+ Shared memory concurrent programming in C++
+ Synchronisation using locks and atomic operations
+ Implementation of synchronisation primitives
+ Functional programming and concurrency
+ Dynamic data race detection

The other half will explore the theory and practice of shared memory concurrency, which underpins many of the concurrency models studied in the first half. It will focus on:

+ Primitives for shared-memory concurrency
+ Architecture support for single- and multi-core shared memory
+ Strong and weak memory models
+ Challenges of correct concurrent programming (races, deadlocks, livelocks, progress guarantees)
+ Design patterns for synchronisation (mutexes, locks, monitors)
+ Concurrent objects and linearisability

The practical part of the course will use the C++ programming language. A series of videos providing a crash course in C++ tailored to the needs of this course will be provided.

The course will rely heavily on knowledge from the Java concurrency material in Computing Practical 1 (40009), the material on concurrency in operating systems in Computing Practical 2 (50007), and on Models of Computation (50003). JMC students who have not already taken Models of Computation should consider taking it in parallel with this course - it will be tough to succeed in the theoretical part of this course without background from Models of Computation.

Teaching methods

This module will be taught via a combination of live lectures and problem solving classes applied to unassessed, formative, exercises. Interaction will also be encouraged through the use of Mentimeter Q&A, which will test student understanding of the often very subtle issues that pervade the subject.
 

An online service will be used as a discussion forum for the module. 

Assessments

There will be two assessed coursework exercises designed to reinforce your understanding of the taught material. The first will be a practical coursework involving solving a concurrency-related problem using one of the programming models studied during the course. The second will be a written coursework addressing the more theoretical aspects of the subject. These collectively contribute 20% of the module mark; the remaining 80% comes from a written examination.

Written feedback will be given on the two assessed coursework exercises and there will be additional class-wide feedback highlighting common strengths and weaknesses. In-class feedback will also be facilitated through Mentimeter Q&A.
 

Reading list

Supplementary reading

Module leaders

Dr Azalea Raad
Professor Alastair Donaldson