Semantics of Concurrency

Aims

Concurrent computation is now pervasive, from multicore processors to large-scale distributed systems. Yet it remains notoriously challenging to program, model and verify, due to the intrinsic non-determinism and rich computational structures that arise from interactions between the components of a concurrent system.

This module explores the semantics of concurrent computation, surveying some of the major approaches to modelling concurrency developed in concurrency theory, programming language semantics, logic and verification.

Syllabus and structure

Each week, students will be assigned two to three papers to read, as well as a short assignment of one to two questions, both to be completed before the seminar. Each seminar will consist of two parts. The first part will be a guided discussion of the week's papers and assignment, potentially aided by additional exposition, in which students are expected to participate actively. The second part will consist of a lecture providing background for the following week's seminar.

Topics may vary but will be drawn from the following list:

● Operational Semantics

● Trace Theory

● Behavioural Equivalence

● Game Semantics

● Denotational Semantics

● Causal Models

● Process Algebras

● Logics for Concurrency

At the midpoint and at the end of the course, students will be asked to write a critique of a recent paper (assigned by the instructor) in one of the topics covered in previous weeks.

Objectives

Students should leave this module with a solid grasp of the major approaches to modelling concurrency, and with sufficient background to pursue further independent study in the subject. Beyond developing technical skills, the course aims to hone students' ability to engage critically with primary literature, evaluate technical work on its merits, and articulate their arguments effectively.

Assessment

Assessment consists of three parts:

1. Paper Overviews (10%):

Each week, one student will be assigned to each of the week's papers. That student will open the discussion of the paper with a short presentation (~10 minutes) introducing it and summarising its major themes. Each student will present at most twice.

2. Six weekly assignments (30%):

Students will be assigned one or two questions weekly on the topic of the corresponding week. These might be technical questions or short essays.

The weekly assignments will be paused on weeks when paper critiques are due.

Technical questions will be marked for correctness, thoroughness, and the ability to communicate mathematics clearly, through precise definitions and well-structured proofs.

Short essays will be marked for understanding, insight and analysis, quality of argumentation and ability to communicate ideas clearly.

3. Paper Critiques (60%):

Students will be assigned a paper published in the past few years, in one of the topics covered in previous weeks, two weeks before the critique is due.

The paper critique is a well-structured written assessment of the assigned paper, similar to a review written during peer review for conferences or journals, but held to a higher standard of writing and argumentation.

Students will be provided guidance on how to write paper critiques. The second paper critique will be weighted more heavily (35%) than the first (25%).

Paper critiques will be evaluated on their structure, ability to communicate ideas clearly, demonstrated understanding of the paper, strength of argumentation, and insight.

Recommended reading material and resources

The following survey covers some of the major topics in the module. Students are not expected to be able to follow it prior to taking the module, but it may serve as a useful reference during it.

- Glynn Winskel and Mogens Nielsen. 1995. Models for concurrency. In Handbook of Logic in Computer Science, Vol. 4: Semantic Modelling, Samson Abramsky, Dov M. Gabbay, and Tom S. E. Maibaum (Eds.). Oxford University Press, Oxford, UK, 1–148.