6CM504 — Concurrency and Communication
Concurrent systems modelling using CSP and the FDR4 model checker.
Instructor: Ioannis Tsioulis
Term: Level 6 (UG)
Location: Mediterranean College, Athens
Overview
This module introduces the formal modelling and verification of concurrent systems using Communicating Sequential Processes (CSP) and the FDR4 model checker. Students specify, analyse, and verify system properties such as deadlock-freedom and trace refinement in realistic concurrent scenarios.
Topics
- CSP: syntax, semantics, and process primitives
- Prefixing, choice, and parallel composition
- Trace, failures, and divergences semantic models
- Deadlock and livelock analysis
- Refinement checking with FDR4
- Case studies in concurrent system verification
Companion material
The programming labs of the module are written in C and use OpenMP and MPI. The repository C for Concurrency is a C refresher written for those labs. Its lessons are read directly on GitHub, and every example can be run in an online compiler, with nothing to install.
| Lesson | Topic |
|---|---|
| 1 | The structure of a C program, compiling and running |
| 2 | Variables, types, printf and scanf |
| 3 | Operators and decisions |
| 4 | Loops |
| 5 | Arrays |
| 6 | Functions |
| 7 | Pointers |
| 8 | Dynamic memory |
| 9 | Structs |
Each lesson has runnable examples, short questions to check understanding, and exercises with solutions. Along the way it points out the parts of C that parallel programs rely on, such as loops with independent iterations and passing part of an array to a worker.