CS 353: Principles of Concurrency and Parallelism

January 10, 2022

Instructor

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

suresh@cs.purdue.edu

Office Hours:

Tu, Th. 3 - 4

Syllabus

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.

Grading

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 used to test or verify 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%)
Final Proposal (5 pages): March 4, 2022 (20%)
Report and Demonstration (10 page report): April 28, 2022 (70%)

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

Syllabus

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 - Stacks, Lists
     Lecture 6: Concurrent Data Structures - Sets, Queues

Part 2: Models:

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

February 7 - February 11
     Lecture 9: Data Races
     Lecture 10: Causality

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

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

Part 3: Language and Abstractions

February 28 - March 4
     Lecture 14: Rust Concurrency (Introduction)
     Lecture 15: Rust Concurrency (Type-checking)

March 7 - March 11
     Lecture 16: Message-Passing
     Lecture 17: Erlang, Go

March 21 - March 25
     Lecture 18: Concurrent ML, Transactional Events
     Lecture 19: Deterministic Parallelism

March 28 - April 1
     Lecture 20: Atomicity
     Lecture 21: STM Haskell

Part 4: Testing and Verification

April 4 - April 8
     Lecture 22: Testing - Iterative Context-Bounded Checking (Chess)
     Lecture 23: Testing - Probabilistic Concurrency Testing (PCT)

April 11 - April 15
     Lecture 24: Model Checking
     Lecture 25: Temporal logic (TLA)

April 18 - April 22
     Lecture 26: Verification via Refinement
     Lecture 27: Rely/Guarantee Reasoning

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


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