ITA | ENG
B006810 - CONCURRENT PROGRAMMING
Main information
Course Content
Suggested readings
Learning Objectives
Prerequisites
Teaching Methods
Further information
Type of Assessment
Course program
Academic Year 2012-13
Course year
Second year - First Semester
Belonging Department
Statistics, IT and its applications "G. Parenti" (DISIA)
Course Type
Single education field course
Scientific Area
INF/01 - INFORMATICS
Credits
9
Teaching Hours
72
Teaching Term
24/09/2012 ⇒ 21/12/2012
Attendance required
No
Type of Evaluation
Final Grade
Course Content
show
Course program
show
Lectureship
Course Content
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. The Linda model. Introduction to model checking.
Suggested readings (Search our library's catalogue)
Mordechai Ben-Ari. Principles of Concurrent and Distributed Programming, 2/e. Addison-Wesley, 2006.
Learning Objectives
The 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.
Further information
Office hours: by appointment.
Type of Assessment
Written examination. Discussion of the written examination.
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: Java and Promela.
The problem of the Critical Section: 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.
Advanced algorithms for the CS: the Bakery algorithm. Correctness proofs.
Semaphores and their implementation. The problem of the Dining Philosophers. Correctness proofs.
The concept of the Monitor and its properties. The problem of readers-writers. Correctness proofs.
Communication via channels. Implementations.
The Linda model.
Introduction to automatic verification: LTL, Promela and the SPIN model-checker.
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: Java and Promela.
The problem of the Critical Section: 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.
Advanced algorithms for the CS: the Bakery algorithm. Correctness proofs.
Semaphores and their implementation. The problem of the Dining Philosophers. Correctness proofs.
The concept of the Monitor and its properties. The problem of readers-writers. Correctness proofs.
Communication via channels. Implementations.
The Linda model.
Introduction to automatic verification: LTL, Promela and the SPIN model-checker.