Skip to main content

Concurrency:  2020-2021

Lecturer

Degrees

Schedule S1(CS&P)Computer Science and Philosophy

Schedule S1Computer Science

Schedule S1(M&CS)Mathematics and Computer Science

Schedule AMSc in Computer Science

MSc in Mathematics and Foundations of Computer Science

Term

Links

Overview

The lectures for this course will be live via MS Teams, via the live lectures channel here. Lectures will also be recorded and made available via the Computer Science Panopto site.
Computer networks, multiprocessors and parallel algorithms, though radically different, all provide examples of processes acting in parallel to achieve some goal. All benefit from the efficiency of concurrency yet require careful design to ensure that they function correctly. The concurrency course introduces the fundamental concepts of concurrency using the notation of Communicating Sequential Processes. By introducing communication, parallelism, deadlock, livelock, etc., it shows how CSP represents, and can be used to reason about, concurrent systems. Students are taught how to design communicating processes, how to construct realistic models of real systems, and how to write specifications that can be used to verify the correctness of the system models. One important feature of the module is its use of both algebraic laws and semantic models to reason about reactive and concurrent designs. Another is its use of FDR to animate models and verify that they meet their specifications.

Learning outcomes

At the end of the course the student should: 

  • understand some of the issues and difficulties involved in Concurrency;
  • be able to specify and model concuurent systems using CSP;
  • be able to reason about CSP models of systems using both algebraic laws and semantic models;
  • be able to analyse CSP models of systems using the model checker FDR.

Synopsis

  • Processes and observations of processes; point synchronisation, events, alphabets. Sequential processes: prefixing, choice, nondeterminism. Operational semantics; traces; algebraic laws.
  • Recursion. Fixed points as a means of explaining recursion; approximation, limits, least fixed points; guardedness and unique fixed points.
  • Concurrency. Hiding. Renaming.
  • Non-deterministic behaviours, refusals, failures.
  • Hiding and divergence, the failures-divergences model.
  • Specification and correctness.
  • Communication, buffers, sequential composition.

Syllabus

Deterministic processes: traces, operational semantics; prefixing, choice, concurrency and communication. Nondeterminism: failures and divergences; nondeterministic choice, hiding and interleaving. Advanced CSP operators. Refinement, specification and proof. Process algebra: equational and inequational reasoning.

Reading list

Lecture Notes: The lecture notes for this year's course appear online on the course materials page.

Course Text:

Alternatives:

Background reading:

Overheads: This year's slides will appear on the course materials page over the course of the term.

 

 

Related research

Activities