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: iductive 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.
2) Mordechai Ben-Ari. Principles of Concurrent and Distributed Programming, 2/e. Addison-Wesley, 2006.
Learning Objectives
This course aims at providing students with the basic principles of programming, specification and verification of concurrent systems. This goal is pursued by the introduction of a reference model, in some fundamental synchronization algorithms are described and their correctness is analyzed.
Prerequisites
Familiarity with the basics of sequential programming, a few elements of propositional logic.
Teaching Methods
Lectures in class.
Further information
Office hours: by appointment.
Type of Assessment
Written test. The examination consists of a selection of exercises and questions. The exercises are designed to assess students' ability to apply theoretical and technical knowledge to model and solve problems in Concurrent Programming. Special attention is devoted to evaluating the correctness of the procedures followed, as well as the originality and effectiveness of the methods adopted.
The questions are structured to verify the students' knowledge and level of understanding of the theory covered in the course. A set of sample exams is available for students on the official course website.
Course program
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: iductive 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.