Cancelled Concurrent and Distributed Systems

Course content

A large set of computer applications are inherently asynchronous, meaning that the program execution order is cannot be scheduled at the time the program is written. The asynchronicity may arise from several sources, such as events, instrument observations, human input, or a combination of program states that trigger a new state. The challenges that stems from asynchronicity are amplified by the fact that any computer CPU has a number of processor-cores, and this number is steadily rising. Thus, working with programs that may have an enormous state-space, and processing these on many-core systems, often triggers errors such as program deadlock, race-conditions, and other more exotic errors. These errors are impossible to test for and hard eliminate with debugging. Thus, the class will introduce a formal algebra, CSP, that provides programmers the means of formally proving that a program is free from a set of known concurrency errors. Tools that automate these proofs and techniques for writing efficient concurrent and correct programs are central to the class. Tools that map solutions to hardware, rather than programs, are also covered.

Many application domains include several, independent, computers that communicate through a network, forming a distributed system. In addition to concurrency errors, such systems must also function in the presence of hardware errors. The class introduces the additional error-models that may arise in distributed systems and the common techniques for addressing these.


MSc Programme in Physics

Learning outcome

At course completion, the successful student will have:

Knowledge of:

  • Multi- and many-core hardware
  • The CSP programming abstraction: concepts, notation, and reasoning principles.
  • CSP-based tools, libraries and verification systems.
  • Implementation techniques for efficiently executing concurrent programs on highly parallel platforms.
  • Distributed systems and managing errors in these


Skills to:

  • Write programs that may be formally verified.
  • Design and implement highly concurrent programs.
  • Design a distributed, fault tolerant, system.


Competences to:

  • Construct and validate maintainable, high-performance concurrent and/or parallel applications according to sound structuring and reasoning principles.
  • Construct and manage distributed systems.

Lectures and mandatory assignments. Independent work at home will be a major part of the workload.

See Absalon for final course material.

Solid sequential programming competences; BSc-level background in computer architecture (CPU organization, memory hierarchy, ...) and multiprogramming (threads, locks, monitors, semaphores,,,,); basic discrete mathematics (sets, sequences, functions, relations, quantifiers, induction, ...).

Academic qualifications equivalent to a BSc degree is recommended.

Continuous feedback during the course of the semester
7,5 ECTS
Type of assessment
Written assignment, 12 days
An individually written report based on a fixed assignment, containing both design, reasoning and programming tasks. The report is due on the last day of the exam period and is submitted electronically.
All aids allowed
Marking scale
7-point grading scale
Censorship form
No external censorship
Several internal examiners
Criteria for exam assessment

See learning outcome.

Single subject courses (day)

  • Category
  • Hours
  • Lectures
  • 28
  • Preparation
  • 128
  • Exam
  • 50
  • English
  • 206