CMSC 712: Distributed Algorithms and Verification (Fall 2003)
http://www.cs.umd.edu/~shankar/712-F03
Please check (reload) this page at least twice a week
Last updated January 1 2004
Overview
- News
- Texts
- Grading/MS comp
- Projects/HW
- Grades
News
-
(Jan 1)
Grades available.
-
(Dec 22)
Typo in problems 2b and 2d:
reference is made to "u[i].st",
which hasn't been defined in the system program.
Obvously, "u[i].st=H" should be "u[i] on 2 OR 3"
and "u[i].st=E" should be "u[i] on 4".
-
(Dec 19)
Error in Exam1a solution to Problem 1a:
S_3 does not satisfy the invariance rule.
It may not even be invariant.
-
(Dec 19)
Corrections to Exam1a solution to Problem 1a:
- In assertion S_4 consequent, "st_k \neq E" should be "st_k \neq T"
- Assertion S_6 consequent should be:
( st_k=T \OR st_k=H) \AND req_j[j]=req_k[j])
-
(Dec 15)
In problem 1 of the final exam, the lc events for eating-read
and eating-write are both named 'bE()'.
You can change them to 'bEr()' and 'bEw()' to avoid confusion
(it does not influence the solution).
-
(Dec 11)
Final exam available:
ps,
pdf,
tex.
Due
Friday December 19 5:00pm Monday December 22.
Please check for the next few days for any corrections to the exam.
-
(Nov 25)
Final exam will be take-home and a very good score there
can overcome a very poor score in exam 1.
-
(Nov 23)
Exam 1a solution:
ps,
pdf.
Exam 1b solution:
ps,
pdf.
Grades (link above) available.
-
(Nov 21)
Transport layer stuff available:
-
Transport layer correctness principles (read this first),
-
Verified data transfer protocols with variable flow control,
-
Minimum-latency transport protocols with modulo-N incarnation numbers.
-
(Nov 19)
Theory chapters 4-6 available (chapter 4 has some minor changes).
-
(Nov 12)
Version 2 of take home exam available (same links as before).
Changes from version 1:
-
Cosmetic changes in page 1 and 2.
-
Lc-event rec(int j):
changed "int" in header to "0..N-1";
added "ack[j] := t" to action.
-
Lc-event bE():
strengthened enabling condition with
"req[i]<ack[j]" conjunct.
-
(Nov 11)
Reminder: In class exam this friday (November 14).
-
(Nov 11)
Take home exam available:
ps,
pdf,
tex.
Due Monday November 17.
Please keep checking once a day for any corrections to the exam.
-
(Oct 29)
Chapter 4 (service programs) available.
-
(Oct 28)
Examples 7-9 (termination detection and snapshot) available.
-
(Oct 21)
The termination detection papers package have been in the folder
of my office door since Friday.
-
(Oct 10)
Examples 1-6 on web.
Try hard to solve the problems before looking at the solutions.
-
(Oct 8)
Chapter 3 addendum (effective atomicity, lock manager assertional proof)
on web.
-
(Oct 2) Tomorrow's class will start at 11:45, in case you
want to go for SysChat.
-
Chapter 3 on web.
-
Peterson alg analysis on web.
-
Bakery alg analysis on web (for next class).
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
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).