News

• (Dec 6) HOT  MS comp problem (not needed for course grade). This problem is about extending the compositionality theory (chapter 5) to real-time systems (as modeled in section 3.7). Specifically, you have two tasks:
  1. Extend the definition of system A implements system B (section 5.2) to the case where A and B are real-time systems. Your extension should continue to preserve compositionality (section 5.3, theorem 5.2). Note: I want only the definition, not a proof of compositionality.
     [Hint: The current definition assumes that B is a non-real time system (although it does not explicitly say so, A can be a real-time system). The extension also requires you to extend the definitions of safe wrt B and complete wrt B.]

  2. Extend the program-based formulation of system A implements service B (section 5.4, theorem 5.3) to the case where A and B are real-time systems. Note: I want only the statement of the theorem, not a proof of the theorem.

• (Nov 29) HOT  Exam 2.1 deals with the paper http://doi.acm.org/10.1145/151646.151651. Lazy caching. Afek, Brown, Merritt. ACM TOPLAS, January 1993, pp 182-205.

  The above paper describes a shared memory system that supposedly implements sequential consistency. You are asked to prove this in our formalism. Specifically, augment the algorithm (specified formally in section 4.2 of the paper) to define (1) an auxiliary variable smh that records the sequence of read and write requests and returns, and (2) an auxiliary variable (or function) hs such that hs is sequential and has the same order of operations for each user as smh. Alternatively, if you think the algorithm does not work, present an execution that violates sequential consistency.

• (Sep 1) Chapters 1 and 2 handed out in class.

Overview

This course deals with the specification and design and verification of concurrent (including distributed) systems. 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 implements its service. 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

• Chapters from a book in preparation will be handed out.
• The following notes are from my 412 (operating systems) course. They cover various classical synchronization problems and their operational analyses, in case you want some background.
  • 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).

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