News

• (Dec 16) HOT  Page 7 of last posting (section 2.3): the offerer system in the termination detection for diffusing computations has a mistake in the "Deliver()" event: if x is not an ack and engaged is false, it should update engaged and engager and not send an ack. (This change would make it consistent with the algorithm (first rule) given on previous page.)
• (Dec 14) HOT  Termination detection service (same as before), termination detection for diffusing, and distributed snapshot service. Note: The snapshot service is more complicated than it has to be (see in Concluding Remarks). If you cannot understand the above snapshot service, then solve the problem using only the fifo channels of the service. If you can understand the above snapshot service, it can simplify your algorithm. For the MS comp, you also need to state the satisfaction conditions (instantiated for this problem) and give an assertional analysis (give assertions that you consider insightful and omit assertions you consider trivial).
• (Dec 13) HOT  Corrected termination detection service. Same link as before.
• (Dec 13) HOT  Termination detection service
• (Dec 13) HOT  The take home exam problem is to obtain a system that offers the termination detection service (for an arbitrary initial activation) using the snapshot service. These services have been described in class. Service specifications will be put up this evening, but they will be consistent with what was shown in class and so you can start on the problem without them. Due date is this Friday (Dec 17, 12 noon).
• (Nov 30) Chapters 11 (notation for data structures) and 12-16 (diners/drinkers services and solutions) available. Link below.
• (Nov 19) Links to papers on timestamps, general mutual exclusion, drinking philosophers, termination detection, distributed snapshots. You are expected to read and digest the ones marked ESSENTIAL. We will be doing them in class from number 4 onwards.
• (Nov 18) Chapters 9 (bakery algorithm) and 10 (timestamps) available. Link below. (The previous chapter 9 was preliminary.)
• (Nov 8) Reminder: Exam 1 this Friday (Nov 12).
• (Nov 4) Chapters 8 and a preliminary chapter 9 now available. Chapter 9 discussses the simplified bakery algorithm and gives a precise statement of the second problem in hw2.
• (Nov 2) Note on channels now available. The second problem in Exercises is a precise statement of the first problem in hw2.
• (Oct 26) Revised chapter 3 (reliable channels from unreliable channels) available (same link as before). The real-time model in LRDml subsection in section 3.2 is different. The assertional proof of invariance of C_1 and C_2 is now included in section 3.4 (for SWP over lossy channels) and in section 3.5 (for SWP over LRDml channels).
• (Oct 22) Homework 1 problem 2 (assertional proof of sliding window over lossy channels.
• (Oct 21) Chapter 7 available (link below).
• (Oct 20) Chapter 6 available (link below).
• (Oct 6) Homework 1 clarifications.
• (Oct 6) Chapters 4-5 available (link below).
• (Sep 19) Chapter 3 available (link below).
• (Sep 10) Chapter 2 available (link below).
• (Sep 3) Read chapter 1 and the notes.

Overview

This course deals with the specification and design and verification of concurrent systems, particularly layered concurrent systems as found in operating systems and networking. The methodology emphasizes separate specifications of concurrent systems and concurrent services. We develop a formal framework for specifying services, specifying systems, and establishing that a system satisfies its services. Time permitting, we will also consider concurrent real-time systems.

We apply this to concurrency problems in networking and operating systems for example, TCP, routing, ad-hoc networks, distributed shared memory, sequential consistency, transaction processing, atomic commits and serializability, etc.

Grading / MS comp

• Exam 1 --- 50%
• Exam 2 --- 50%
• Weightages are approximate and may change by upto 10%.
• The MS comprehensive exam in this course consists of both exams.

Notes and papers

• Chapter 1 (186K pdf)
• The following notes are from my 412 (operating systems) course. They cover various classical synchronization problems and their operational analyses. Read them and solve problems mentioned in them.
  • Note-5: N process mutual exclusion
  • Note-6: Peterson's 2-process mutual exclusion solution
  • Note-7: Bakery algorithm
  • Note 8: Low-level ready-modify-write atomicty
  • Note 9: Semaphores
  • Note 10: Binary Semaphores
  • Note 11: No Busy Waiting
  • Note 12: Bounded-buffer Producer-Consumer Problem
  • Note 13: Readers-Writers Problem
  • Note 14: Dining Philosophers Problem
  • Note 15: East-West Bridge Problem
• BACKGROUND MATERIAL: An Introduction to Assertional Reasoning for Concurrent Systems. ACM Computing Surveys, September 1993. Available in pdf from ACM (via dept library page).
• Chapter 2 (118K pdf)
• Chapter 3 (133K pdf)
• Chapters 4,5 (177K pdf)
• Chapter 6 (59K pdf)
• Chapter 7 (30K pdf)
• Chapters 8 and preliminary chapter 9
• Chapters 9 and 10 (123K pdf)
• Papers (please read those marked ESSENTIAL):
  1. (ESSENTIAL, except for "Physical Clocks" section and after). Timestamps paper: Leslie Lamport, Time, clocks, and the ordering of events in a distributed system, Communications of the ACM, v.21 n.7, p.558-565, July 1978
  2. Ricart-Agrawala distributed mutex: Glenn Ricart , Ashok K. Agrawala, An optimal algorithm for mutual exclusion in computer networks, Communications of the ACM, v.24 n.1, p.9-17, Jan. 1981
  3. (ESSENTIAL) General exclusion problem: EWD625: Two starvation-free solutions of a general exclusion problem
  4. (ESSENTIAL) Drinking Philosophers: K. M. Chandy , J. Misra, The drinking philosophers problem, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.4, p.632-646, Oct. 1984
  5. Limitations of deterministic algorithms: Daniel Lehmann , Michael O. Rabin, On the andvantages of free choice: a symmetric and fully distributed solution to the dining philosophers problem, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.133-138, January 26-28, 1981, Williamsburg, Virginia.
  6. (ESSENTIAL) Derivation of a termination detection algorithm for distributed computations (with W.H.J.Feijen and A.J.M. van Gasteren)
  7. (ESSENTIAL) EWD 687a: Termination detection for diffusing computations, Dijkstra and Scholten, Information Processing Letters 11, 1: 1.
  8. (ESSENTIAL) EWD864a: The Distributed Snapshot of K.M.Chandy and L. Lamport, Dijkstra
  9. K. Mani Chandy , Leslie Lamport, Distributed snapshots: determining global states of distributed systems, ACM Transactions on Computer Systems (TOCS), v.3 n.1, p.63-75, Feb. 1985
  10. On-the-fly garbage collection: an exercise in cooperation. 4, copyright ) 1980.Edsger W. Dijkstra, Leslie Lamport, A. J. Martin, C. S. Scholten, E. F. M. Steffens November 1978. Communications of the ACM, Volume 21 Issue 11
• Chapters 11-16 (183K pdf)

Projects / Homeworks

This page and all problem sets, lecture notes, and exams linked to it are copyrighted. Use of these pages for the class CMSC712 at the University of Maryland is permitted. Any other use requires permission of the author (Udaya Shankar, shankar@cs.umd.edu).