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.
Grading
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.