CS 353: Principles of Concurrency and Parallelism

January 10, 2022


Prof. Suresh Jagannathan
Room 3154J
Lawson Computer Science Building
Ph: x4-0971


Office Hours:

Tu, Th. 3 - 4


This course will examine the design and implementation of programming languages and computing systems that support concurrency and parallelism with a focus on foundations and principles. It will be broadly partitioned into four units.

The first part of the course covers foundational aspects of concurrency. We will discuss the design choices underlying modern thread sytems, mutual exclusion algorithms, and the implementation of performant concurrent data structures. The second part of the course discusses consistency models, the core principles used to govern visibility and causality constraints among concurrently executing actions that determines a concurrent programs valid behaviors. We will specifically focus our attention on linearizability as the desired correctness criterion for sequentially consistent executions. We will also examine in detail the kinds of (weaker) consistency support provided by modern hardware platforms and programming language definitions/compilers. The third part of the course surveys how concurrency manifests in a programming language. We will focus specifically on how Rust enforces a datarace-free guarantee through its type system, how Erlang and Go express concurrency through message-passing abstractions, the compositional event abstraction found in Concurrent ML, and Haskell's software transactional memory mechanism. The fourth (and last) set of lectures covers testing and verification approaches for validating the correctness of concurrent programs. In this unit, we will discuss testing tools like Chess and PCT, model-checkers, and classical verification methodologies.


The grading for the course will be based on a single semester-long project that can be developed individually or in pairs. Possible examples of projects include (a) a detailed investigation of language abstractions along with qualtitative and quantitative assessments; (b) implementation and evaluation of highly-concurrent data structures; (c) evaluation of tools that can be used used to (i) test for the presence of or verify the absence of concurrency bugs (e.g., data races), (ii) check the linearizability of a concurrent data structure, or (iii) explore the behaviors allowed by various kinds of weak/relaxed consistency models; or, (d) development of new concurrent applications that exercise novel algorithms, models, or reasoning principles.

Initial Proposal (2 pages): February 10, 2022 (10%). Sample proposal format can be found here.
Final Proposal (5 pages): March 4, 2022 (20%). Sample proposal format can be found here.
Report and Demonstration (10 page report): April 28, 2022 (70%)

(Reports are to be formatted using acmconf.sty.)


Part 1: Foundations

January 10 - 15
     Lecture 1: Introduction
     Lecture 2: Coroutines, Threads, Processes, and Locks

January 17 - 21
     Lecture 3: Mutual Exclusion Algorithms
     Lecture 4: Simple Concurrent Objects

January 24 - 28
     Lecture 5: Concurrent Data Structures - Sets
     Lecture 6: Concurrent Data Structures - Queues, Stacks

Part 2: Models:

January 31 - February 4
     Lecture 7: Sequential Consistency
     Lecture 8: Linearizability

February 7 - February 11
     Lecture 9: Data Races

February 14 - February 18
     Lecture 10: Hardware Memory Models (x86)
     Lecture 11: Hardware Memory Models (Power, ARM)

February 21 - February 25
     Lecture 12: Language Memory Models (C11)
     Lecture 13: Language Memory Models (Java)

Part 3: Language and Abstractions

February 28 - March 4
     Lecture 14: Rust Concurrency

March 21 - March 25
     Lecture 15:
     Lecture 16: Erlang, Go

March 28 - April 1
     Lecture 17: Atomicity and Software Transactions
     Lecture 18: Deterministic Concurrency

April 4 - April 8
     Lecture 19: STM Haskell

Part 4: Testing and Verification

April 11 - April 15
     Lecture 20: Testing - Iterative Context-Bounded Checking (Chess) and Probabilistic Concurrency Testing (PCT)

April 18 - April 22
     Lecture 21: Model Checking

Project Presentations

April 25 - April 29

Partial Bibliography

  1. Art of Multiprocessor Programming, Herlihy, Shavit
  2. On the Duality of Operating System Structures, Lauer and Needham
  3. Why Threads are a Bad Idea for Most Purposes, Ousterhout
  4. Threads Cannot be Implemented as a Library, Boehm
  5. Lamport Bakery Algorithm, Lamport

  6. Linearizability: A Correctness Condition for Concurrent Objects, Herlihy and Wing
  7. Lineup: A Complete and Automatic Linearizability Checker, Burckhardt et. al
  8. Deriving Linearizable Fine-Graind Concurrent Objects, Vechev et. al
  9. Eraser: A Dynamic Datarace Detector for Multithreaded Programs, Savage, et. al
  10. FastTrack: Efficient and Precise Dynamic Race Detection, Flanagan and Freund
  11. RacerD: Compositional Static Race Detection, Blackshear et. al
  12. X86-TSO: A Rigorous and Usable Programmer's Model For X86 Multiprocessors, Sewell et. al
  13. Understanding POWER Multiprocessors, Sarkar et. al
  14. Common Compiler Optimisations are Invalid in the C11 Memory Model and What We Can Do About It, Vafeiadis et. al
  15. Foundations of the C++ Concurrency Memory Model, Boehm and Adve
  16. Fixing the Java Memory Model, Pugh
  17. Repairing Sequential Consistency in C/C++11, Lahav et. al
  18. A Case for an SC-Preserving Compiler, Marino et. al
  19. On Validity of Program Transformations in the Java Memory Model, Sevcik and Aspinall

  20. Fearless Concurrency in Rust
  21. Go Concurrency
  22. Erlang Concurrency
  23. Parallel Concurrent ML, Reppy
  24. Transactional Events, Donnelly and Fluet
  25. Composable Memory Transactions, Harris et. al
  26. A Type and Effect System for Deterministic Parallel Java, Bocchino et. al

  27. Atomizer: A Dynamic Atomicity Checker for Multithreaded Programs, Flanagan and Freund
  28. Iterative Context-Bounding for Systematic Testing of Multithreaded Programs, Musuvathi and Qadeer
  29. KISS: Keep it Simple and Sequential, Qadeer and Wu
  30. A Randomized Scheduler with Probabilistic Guarantees fo Finding Bugs, Burchkhardt et. al
  31. The Model Checker SPIN, Holzmann
  32. The Temporal Logic of Actions, Lamport
  33. The Rely-Guarantee Method for Verifying Shared Variable Concurrent Programs, Xu et. al
  34. Atomicity Refinement for Verified Compilation, Jagannathan et. al