This module introduces the basic principles of concurrent programming
and their use in designing programs.
Outline Syllabus
The module focuses on four main themes
- Introduction to concurrency: what concurrency is, hardware
support for concurrency, the core problems of mutual exclusion and
conditional synchronisation, concurrency primitives for shared memory
and distributed concurrent programming including semaphores, monitors,
RPC and rendezvous
- Design of simple concurrent algorithms in Java: the use of
threads, synchronized methods, and monitors.
- Correctness of concurrent algorithms: safety and liveness
properties of concurrent algorithms, proving properties using assertional
reasoning and model checking.
- Design patterns for common concurrency problems: the lectures
and exercises also illustrate the use of concurrency primitives and
algorithms to solve some common problems in concurrent programming, e.g.,
the producer-consumer problem, the readers and writers problem, client
server problems etc.
Lectures
Lectures are on Wednesdays at 10:00 in LT3 (Exchange Building) and
Fridays at 15:00 in A25 (Business School South). Note that there are
no lectures on 4th, 9th and 11th of April or on the 14th of May.
Reading List
Recommended Reading
Further Reading
- Ben-Ari (1982), Principles of Concurrent Programming, Prentice Hall.
- Andrews (1991), Concurrent Programming: Principles & Practice,
Addison Wesley.
- Burns & Davies (1993), Concurrent Programming, Addison Wesley.
- Hartley (1998), Concurrent Programming: The Java Programming
Language, Oxford.
- Magee & Kramer (1999), Concurrency: State Models and Java Programs,
John Wiley.
- Bishop (2000), Java Gently, 3rd Edition, Addison-Wesley.
- Huth & Ryan (2000), Logic in computer science:
modelling and reasoning about systems, Cambridge University Press.
You may also find the
Java Tutorial useful for the material on Java.
Note that there is also
a version of the reading list
with links to the University Library catalogue.
Suggested Reading
Note that the following list of suggested reading is provisional,
as it may necessary to change the order in which topics are presented.
- Lecture 1: Introduction.
Andrews (2000), chapter 1, sections 1.1-1.2;
Ben-Ari (1982), chapter 1.
- Lecture 2: Processes and Threads.
Bishop (2000), chapter 13;
Lea (2000), chapter 1;
Java Tutorial, Threads.
- Lecture 3: Synchronisation.
Andrews (2000), chapter 2, section 2.1, chapter 3, section 3.1;
Ben-Ari (1982), chapter 2.
- Lecture 4: Atomic Actions.
Andrews (2000), chapter 2, sections 2.1 and 2.4, chapter 3, section 3.2;
Ben-Ari (1982), chapter 2.
- Lecture 5: Mutual Exclusion Algorithms I.
Andrews (2000), chapter 3, sections 3.1--3.2;
Ben-Ari (1982), chapter 2;
Andrews (1991), chapter 3, section 3.1.
- Lecture 6: Mutual Exclusion Algorithms II.
Ben-Ari (1982), chapter 3;
Burns & Davies (1993), chapter 3, section 3.4.
for the Java Memory Model.
Lea (2000), chapter 2; Java Language Specification, chapter 17.
- Lecture 7: Semaphores I.
Andrews (2000), chapter 4, sections 4.1--4.2;
Ben-Ari (1982), chapter 4;
Burns & Davies (1993), chapter 6.
- Lecture 8: Semaphores II.
Andrews (2000), chapter 4, sections 4.1--4.2;
Ben-Ari (1982), chapter 4;
Burns & Davies (1993), chapter 6.
for Producer-Consumer Problems.
Andrews (2000), chapter 1, section 1.6;
Ben-Ari (1982), chapter 4.
- Lecture 9: Monitors I.
Andrews (2000), chapter 5;
Ben-Ari (1982), chapter 5;
Burns & Davies (1993), chapter 7, sections 7.4-7.9.
- Lecture 10: Monitors II.
Andrews (2000), chapter 5;
Ben-Ari (1982), chapter 5;
Burns & Davies (1993), chapter 7, sections 7.4-7.9.
for Readers and Writers Problems.
Andrews (2000), chapter 4, section 4.4, chapter 5, section 5.4;
Ben-Ari (1982), chapter 5, section 5.4;
Burns & Davies (1993), chapter 6, section 6.8;
- Lecture 11: Synchronisation in Java I.
Lea (2000), chapter 2;
Java Tutorial, Synchronizing Threads.
- Lecture 12: Synchronisation in Java II.
Lea (2000), chapter 3.
- Lecture 13: Message Passing.
Andrews (2000), chapter 7;
Burns & Davies (1993), chapter 4;
Andrews (1991), chapters 7 & 8.
for Client-Sever problems.
Andrews (2000), chapters 7 & 8.
- Lecture 14: Remote Inovcation.
Andrews (2000), chapter 8;
Ben-Ari (1982), chapter 6;
Burns & Davies (1993), chapter 5;
Andrews (1991), chapter 9.
- Lecture 15: Distributed Processing in Java I.
Andrews (2000), chapter 8;
Java Tutorial, Sockets.
- Lecture 16: Distributed Processing in Java II.
Andrews (2000), chapter 8;
Java Tutorial RMI.
- Lecture 17: Proving Correctness.
Andrews (2000), chapter 2, sections 2.6--2.8;
Ben-Ari (1982), chapter 3.
- Lectures 18 & 19: Model Checking.
Huth & Ryan (2000), chapter 3.
Exercises
There will be a number of (unassessed) exercises covering
some of the programming constructs and proof techniques introduced in the
module. Model answers will be given in the lectures.
Lecture Slides
Warning: the slides are not `lecture notes': they are there to help
present the material, not to act as a reference to the main points covered
in the lecture. Simply reading the slides won't necessarily give you a good
grasp of the syllabus. They are specifically not a substitute for
taking your own notes or reading the suggested reading for the lecture.
- Lecture 1: Introduction
Slides
- Lecture 2: Processes and Threads
Slides
and the ParticleApplet example
- Lecture 3: Synchronisation
Slides
and the Ornamental Gardens applet
(from Magee & Kramer (1999))
- Lecture 4: Atomic Actions
Slides
- Lecture 5: Mutex Algorithms I
Slides
- Lecture 6: Mutex Algorithms II
Slides
- Lectures 7 & 8: Semaphores I
Slides
- Lecture 9: Semaphores II
Slides
and the Producer-Consumer/Bounded Buffer
applet
(from Magee & Kramer (1999))
- Lecture 10: Monitors I
Slides
- Lecture 10: Monitors II
Slides
- Lecture 11: Synchronisation in Java I
Slides
- Lecture 12: Synchronisation in Java II
Slides
- Lecture 13: Synchronisation in Java III
Slides
- Lecture 14: Remote Invocation
Slides
- Lecture 15: Distributed Processing in Java
Slides
- Lecture 16: Proving Correctness
Slides,
the Ornamental Gardens applet
(from Magee & Kramer (1999)), and the
the "Proof Garden" applet
- Lecture 17: Model Checking I
Slides
- Lecture 18: Model Checking II
Slides
Copyright © 2014
Brian Logan
This file is maintained by Brian Logan
Last modified: 26-Jan-2014, 17:02