News

• HOT  (June 4) Grades
• (May 18) Changes to exam 2 (current ps/tex files have these fixes):
  • Problem 1: add SFair(P(rcmutex)) and SFair(P(xlock)) to system's progress assertions.
  • Problem 2, part a: A(i,j) and B(i,j) are equivalent, so it suffices to have only one.
  • Due date extended to Thursday May 22, 5pm (slip under my office door).
• (May 16) exam 2.ps (42K), exam 2.tex.
• (May 14) Exam 1(a+b) scores (out of 16): 14, 13, 11, 9, 9, 9, 9, 8, 7, 7, 7, 6, 6, 4.
• (May 14) exam 1a solution (ps) and exam 1b solution (ps). I have not yet checked the solutions, so there probably are errors. Also exam 1a progress solution definitely needs more work.
• (April 30) Assume read-write atomicity, just like in Peterson and Bakery algorithms. (So some ai or bi may not be atomic.)
• (April 30) Correction: In line a3, "st[j]" should be "st[p]". The ps/tex now have this fix.
• (April 30) In exam 1a, suppose you decide to prove a property. Should your proof be assertional or operational?
  • In general, your proof can have both assertional and operational parts. The key issue is to have your proof be readable and convincing. Your proof should cover all the cases.
  • A "non-obvious" assertion is usually best proved assertionally, i.e., by a proof rule application (in which other assertions may be inputs). But this is not always the case (e.g., consider the use of commuting actions in the analysis of the snapshot detection algorithm).
  • In any case, properties must be expressed by assertions.
• (April 29) exam 1a.ps (42K), exam 1a.tex.
• The following relevant articles are available in pdf from ACM (via dept library page).
  • Verified data transfer protocols with variable flow control. ACM Transactions on Computer Systems, August 1989.
  • A Stepwise Refinement Heuristic for Protocol Construction. ACM Transactions on Programming Languages and Systems, July 1992.
  • An Introduction to Assertional Reasoning for Concurrent Systems. ACM Computing Surveys, September 1993.
• (April 22) Transport Layer Principles, Minimum Latency Transport Protocols with Modulo-N Incarnation Numbers
• (April 22) Stepwise Design of Distance-Vector Routing Algorithms
• (April 15) realtime slides (210K ps)
• (April 12) For class on Thursday April 17, attend the UMIACS/LTS seminar at 2:00 pm AVW 2460: CODEX: An Application of Distributed Trust Michael Marsh (www.cs.cornell.edu/people/mmarsh) Abstract: Distributed trust is a design principle that allows us to construct systems that are both fault-tolerant and secure under realistic assumptions about real-world distributed computing environments. Applications of distributed trust will be presented, and a technique will be described for constructing systems from distributed components playing roles of trusted hosts.
• (Mar 4) Chapter 5 reposted.
• (Mar 3) Chapter 5 posted.
• (Feb 27) Posted specs of lock service and mutex-based lock managers.
• (Feb 16) Bakery algorithm analysis posted. Peterson's algorithm analysis has some corrections.
• (Feb 13) Peterson's algorithm analysis posted.
• (Feb 11) Chapters 2,3,4 posted.
• (Jan 30) 412 notes posted.
• (Jan 29) Chapter 1 posted.

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 (280K ps)
• 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
• Chapters 2,3,4 (300K ps)
• Peterson's algorithm analysis (85K ps)
• Bakery algorithm analysis (110K ps)
• Lock service (49K ps)
• Mutex-based lock managers (76K ps)
• Chapters 5 (250K ps)

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