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 cosists of two parts:
1. a test in written form, with theoretical and programming exercises on the course topics (*);
2. Oral exam, mainly based on a discussion of the written test.
(*) a number of examples of such tests are made 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.