CS 353: Principles of Concurrency and Parallelism

January 9, 2023


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


Office Hours:

M, W. 3 - 4


This course examines the design and implementation of concurrent programming languages, data structures, algorithms, and computing systems, 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, a property that relates the behavior of a concurrent data structure with its sequential specification, 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 the Rust language enforces a datarace-free guarantee through its type system, and how languages like Erlang and Go express concurrency through message-passing abstractions. We will also consider more advanced (and less widely-adopted) designs, including 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. The project can be framed either as a research problem or as an evaluation study. Examples of the former may include (a) proposals for new concurrent data structures or applications that develop new algorithms, models, or reasoning principles; (b) implementing and assessing extensions to existing language abstractions; or, (c) developing tool extensions for verifying or testing data structure or program correctness. Examples of the latter may include (a) a comparative assessment of tools for testing or verifying consistency models; (b) detailed performance and scalability studies of these tools, or (c) comparative analysis of different concurrent algorithms, data structures, or languages against a common set of benchmarks exercising a particular set of features.

Initial Proposal (2 pages): February 10, 2023 (10%). Proposal outline { .tex, .pdf}
Final Proposal (5 pages): March 8, 2023 (20%). Proposal outline { .tex, .pdf}
Report and Demonstration (10 page report): April 28, 2023 (70%)

The LaTex proposal and report template class file can be found here.


Part 1: Foundations

January 9 - 13
     Introduction; Coroutines, Threads, Processes, Locks

January 16 - 20
Mutual Exclusion

January 23 - 27
Simple Concurent Data Structures

January 30 - February 3
Non-Blocking Data Structures

February 6 - February 10
Consistency and Linearizability

Part 2: Models

February 13 - February 17
Data Races

February 20 - February 25
Hardware Memory Models

February 27 - March 3
Software Memory Models

Part 3: Abstractions

March 6 - March 10
Message Passing

March 27 - April 3

April 5 - April 9
Atomicity and Software Transactions

April 10 - April 14
Deterministic Parallelism and Safe Futures

April 17 - April 21
Testing and Verification

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-Grained 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. Prusti: Automated Program Verifier for Rust, Astrauskas et al.
  28. Atomizer: A Dynamic Atomicity Checker for Multithreaded Programs, Flanagan and Freund
  29. CHESS: A Systematic Testing Tool for Concurrent Software, Musuvathi, Qadeer, and Ball
  30. KISS: Keep it Simple and Sequential, Qadeer and Wu
  31. A Randomized Scheduler with Probabilistic Guarantees fo Finding Bugs, Burchkhardt et. al
  32. The Model Checker SPIN, Holzmann
  33. The Temporal Logic of Actions, Lamport
  34. The Rely-Guarantee Method for Verifying Shared Variable Concurrent Programs, Xu et. al
  35. Atomicity Refinement for Verified Compilation, Jagannathan et. al


  1. Linearizability Checker for Kotlin
  2. Cave: Concurrent Algorithm Verifier
  3. A Linearizability Checker based on P-compositionality

  4. Diy Release 7
  5. MemAlloy
  6. MemSynth
  7. CDS Checker
  8. CppMem: Interactive C/C++ Memory Model Visualization

  9. Locksmith: A Static Datarace Detector for Multithreaded C Programs
  10. ThreadSanitizer: A Dynamic Datarace Detector for Multithreaded C Programs
  11. FastTrack: A Dynamic Datarace Detector for Java
  12. Java Pathfinder
  13. Go Dynamic Datarace Detector

  14. Open-Source Implementation of Chess
  15. Shuttle: Concurrency Testing for Rust
  16. Armada: A Language and Tool for Automated Verification of Concurrent Programs
  17. Spin: A Model-Checker for Concurrent Program Verification
  18. TLA+: Temporal Logic of Actions