ON THIS PAGE:

Course Objectives

Prerequisites

Approach

Typical Text

Course Outline

Course Objectives
To present fundamental algorithms and impossibility results from the concurrent programming literature, and to cover techniques for formally specifying and verifying concurrent systems. Both message-passing and shared-memory models of concurrency will be considered.

Prerequisites
Comp 530, 550.

Approach
A combination of lectures, discussions of papers, and homework assignments, the latter including a significant project or research paper.

Typical Text
Papers from the literature will serve as the primary text. Useful supplemental texts include:

• G. R. Andrews, Concurrent Programming: Principles and Practice
• K. M. Chandy and J. Misra, Parallel Program Design: A Foundation
• K. R. Apt and E. R. Olderog, Verification of Sequential and Concurrent Programs
• Gerard Tel, Distributed Systems
• Sape Mullender, ed., Distributed Systems, Second Edition, mainly chapters 2-8.

Course Outline
Numbers in parentheses indicate approximate number of weeks

• Reasoning about concurrent and distributed programs (3)
  • state assertions
  • temporal assertions
  • safety properties
  • invariants
  • liveness properties
  • fairness
  • proof rules
  • verification examples

• Synchronization algorithms for shared-memory systems (3)
  • mutual exclusion
  • barrier synchronization
  • readers/writers
  • local-spin algorithms
  • wait-free and lock-free synchronization
  • performance issues

• Synchronization algorithms for message-passing systems (1)
  • mutual exclusion
  • logical clocks
  • dining philosophers
  • drinking philosophers

• Algorithms for detecting stable properties in message-passing systems (2)
  • deadlock detection
  • termination detection
  • diffusing computations
  • distributed snapshots

• Fault tolerance in message-passing systems (2)
  • Byzantine agreement: algorithms and impossibility results
  • distributed consensus: algorithms and impossibility results
  • self-stabilizing systems
  • fail-stop models

• Broadcast and multicast in message-passing systems (2)
  • broadcast algorithms
  • multicast algorithms
  • lower bounds
  • ISIS
  • applications

• Clock synchronization: algorithms and lower bounds (1)