Overview of Concurrent Programming. The interleaving model. Correctness: Properties of Safety, Liveness, Fairness. Languages: Java and Promela. The issue of Critical Section. Formal methods of verification: inductive proofs and LTL logic. Advanced algorithms for the C.S. problem. Semaphores and their implementation. The problem of the Dining Philosophers. The concept of Monitor. The problem of readers-writers. Communication via channels. Introduction to model checking.
1. Mordechai Ben-Ari. Principles of Concurrent and Distributed Programming, 2/e. Addison-Wesley, 2006.
2. Teacher's class notes.
Learning Objectives
- Knowledge. The course aims at providing students with the basic principles of programming, specification and verification of concurrent systems.
- Competence. This goal is pursued by the introduction of a reference model. Mastering this model, fundamental synchronization algorithms can be described and reasoned about.
- Skills. Analyze correctness of concurrent algorithms; write and reason on the correctness of concrete concurrent programs.
Prerequisites
Familiarity with the basics of sequential programming, a few elements of propositional logic.
Teaching Methods
Lectures.
Further information
Office hours: by appointment.
Type of Assessment
The exam consists of two parts:
1. written test, comprising theoretical and programming exercises, which may focus on any of the topics of the course (*);
2. oral test, mainly centered on a discussion of the written test.
The written test will assess the student's understanding of the models, linguistic primitives and concurrent algorithms seen in class, her/his ability to analyze resource management and synchronization problems in a concurrent scenario, her/his ability to apply acquired knowledge to solve new problems. Having passed the written test is a prerequisite to access the oral test.
The oral test will assess knowledge of the topics presented, mastering of a technical language appropriate to the context, ability to relate different topics of the program to each other.
The mark reported in the written test has the greatest impact (90%) on the final mark.
(*) A number of examples of such tests is available through the e-learning platform.
Course program
Overview of Concurrent Programming: systems, languages and models.
An abstract model: atomic command execution and interleaving model. States, trransitions, state diagrams, computations.
Correctness: Safety and Liveness properties. The Fairness assumption.
Programming and specification languages: concurrency in Java.
The Critical Section problem: Dekker's algorithm.
Formal methods of verification: inductive proofs of invariants, the LTL logic and deductive reasoning, deductive proof of correctness of the Dekker algorithm.
Semaphores and their implementation. The problem of the Dining Philosophers. Correctness proofs.
Semaphores in Java.
The concept of the Monitor and its properties. The problem of readers-writers. Correctness proofs.
Monitors in Java.