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 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%)