CMSC 712: Distributed Algorithms and Verification

Fall 96 A. Udaya Shankar

Time and place

Tuesday, Thursday: 12:30-1:45pm. AVW 1112.

Prerequisites

Familiarity with concurrent programs, e.g. CMSC 412 or 612, or permission of instructor.

Description

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 covers both syntatic (e.g. C++ prototypes) and semantic properties (e.g. order of calling, dependencies between paramenters). The semantic properties include both safety (e.g. consistency of distributed memory accesses) and progress (e.g. termination of every memory access). Time permitting, we will also consider concurrent real-time systems.

The methodology emphasizes separation of interfaces (i.e. specifications) and modules (i.e. implementations). The methodology will be applied to operating systems and networking problems, for example, cache coherence and distributed shared memory, sequential and other types of consistency, atomic broadcasts and multicasts, file systems, transaction processing, atomic commits and serializability, networking layers such as the TCP/IP stack, etc.

Textbooks

Notes and papers distributed in class.

Grades

Midterm exam         approx 30%
Final exam           approx 40%
Homework/project     approx 30%

MS requirement

The MS comprehensive exam in this course consists of both the midterm exam and final exam.

CMSC 712 F96 Homework 1 do by Sept 10

1.

• Critical-section (or mutual exclusion) problem and solutions to it, including the Peterson algorithm and the Bakery algorithm.

• Bounded-buffer problem and solutions.

• Readers-writers problem and solutions.

• Dining philosophers problem and solutions.

• Semaphores and monitors