Course Information

Instructor: Ernie Cohen (ernie.cohen@acm.org)
When: TH 1:30-3:00 (office hours TH 12:00-1:30, Levine 268)
Where: Towne 309

Description
This is a course about how to write correct and efficient low-level concurrent code. With the standardization of C11 and C++11, it is possible for the first time to write portable code that leverages the superior performance of weak memory models on modern multicore processors and memory-model-aware compilers. Such programming is generally considered too difficult for most programmers; in particular, you cannot practically debug such code by testing, but must understand why it is guaranteed to work. Thus, a central component of the course is how to reason effectively about such programs, and how to use such reasoning to guide program design. We will also on occasion go beyond software to consider concurrent system design in general.

We focus on software in which concurrency introduces nontrivial nondeterminism, which is characteristic of almost all serious system code and most modern applications. We do not go deeply into parallel algorithms (where the logical course of computation is determined in advance), benchmarking, or the organization of parallel computations to maximize performance; these are central topics of CIS 534. (We do, however, explore the efficient implementation of parallel programming abstractions). Nor do we go deeply into the large body of concurrent and distributed programming theory (e.g. impossibility results, atomic register constructions), but instead focus on practical programming techniques. 

A typical class will consist of taking a programming problem and working our way to one or more solutions. 

Outline
Here are some of the subjects we will likely explore:
  • multicore memory architecture
  • the Java and C11/C++11 memory models
  • invariants and simulation
  • ownership and permissions
  • ghost programming for strong and weak memory
  • reduction theorems
  • locking and the hypergraph protocol
  • concurrent reading while writing
  • dataflow programming
  • message passing
  • multiversioning
  • clocks and timestamps
  • read-copy-update
  • ABA and hazard pointers
  • descriptors and helping
  • optimism
  • durability and fault tolerance
  • modular reasoning and verification
  • hardware transaction support
and some applications we are likely to address:
  • implementing synchronization primitives (locks, barriers, turnstiles,...)
  • monitors
  • concurrent data structures (queues, sets, maps, lists, work queues,...)
  • dataflow programming
  • dynamic hashtables
  • concurrent garbage collection
  • software transactional memory
  • optimistic multiversion transaction processing
  • atomic snapshots
  • implementing parallel programming models
  • resource contention resolution (diners, drinkers, committees)
  • MMU programming
  • embedded control
  • file systems
Prerequisites
There are no formal prerequisites for this course. However, you should be comfortable reading/writing C code and mathematical formulas and willing to think. The course is open to all adventurous students, including undergraduates. 

While this course is primarily intended for serious programmers and system designers, it might also be of interest to students interested in verification, programming logics, and or programming methodology.

Grading
Grading will be based on final exam (probably oral, depending on class size); students who do poorly have an option to do additional work and take a retest. In addition, students are expected to participate in class and complete homework exercises. Students who wish can also take on a graded project. Students who wish can take the course pass-fail (subject to departmental approval). 

Who am I?
Over the last 20 years I've been a researcher at Bellcore/Telcordia, and a researcher, software engineer, software architect, test architect, and verification architect at Microsoft. My research has mostly been in systems, security, verification, and programming methodology. These days, my focus is on verified programming - making it practical for programmers to verify the functional correctness of their real-world concurrent C/C++ code.