712-F09-index

CMSC 712

Distributed Algorithms and Verification

Fall 2009

http://www.cs.umd.edu/~shankar/712-F09
Please check at least twice weekly. See News for last update

Professor	A. Udaya Shankar (email: shankar@cs.umd.edu). Office hours: after class or by appointment (AVW 4141)
Classes	TuTh 3:30-4:45pm. Room CSIC 3120

News

(Nov 22b) HOT Typos:
- Figure 7.3. In mysid.tx: "oc" should be "ia"; "ia" should be "oc".
- Figure 7.3. In mysid.rx: first "oc" should be "ia".
- Figure 7.3. "progress condition" should be "progress assumption".
- Figure 7.3. "progress condition" should be "progress assumption".
- Figure 7.4. First row: "mytid.taSlack <- Tnow + U" should be "mytid.taSlack <- U".
(Nov 22a) HOT Homework 5 (due Dec 1 in class).
(Nov 8) Exam grades and current course totals posted on grades.cs.umd.edu.
- Course total = (hw1 + hw2 + hw3 + hw4 + exam1) * 100/120
- Approximate course grade cutoffs I would use if I had to give the grades today:
  A > 70%; B > 60%; C > 50%.
- If you took exam 1 as an MS comp, here is the comp grade as of today:
  A > 36 (out of 40); B > 33 (out of 40).
(Nov 2) If you want to meet, I can come early tomorrow. I can't stay long after class.
(Oct 30) Revised homework 4 solution available at www.cs.umd.edu/users/shankar/712-F09/hw-4-sol-revised-oct-30-2009.pdf. I'll remove it after a couple of days.
(Oct 26) Exam 1 on Thu Nov 5 (last day to drop course is Mon Nov 9).
(Oct 21) Hw 1, 2 and 3 scores posted on grades.cs.umd.edu.
(Oct 19c) Homework 4 (due Oct 27 in class or earlier).
(Oct 19b) Regarding Oct15a, last entry: the typo fix ("ns(t2) > k") affects the next few inequalities: "na(t2) ≥ k-SW" becomes "na(t2) > k-SW"; "na(t2) ≥ k-N+RW" becomes "na(t2) > k-N+RW"; "j ≥ k-N+RW" becomes "j > k-N+RW" (which is equivalent to "j ≥ k+1-N+RW").
(Oct 15a) More chapter 4 typos:
- Page 4-8, last paragraph: In second sentence, "falisifes A_3's antecedent" should be "falisifes A_3's consequent". In third sentence, "preserves A_3's antecedent" should be "preserves A_3's consequent".
- Page 4-9: Sentence 1 would be clearer if it said: "The only other way to falsify A_3 is to increase nr to an extent that violates the lower bound in A_3's consequent for some data message j in transit".
- Page 4-9, paragraph after A_5, line 2: "ns(t2) ≥ k" should be "ns(t2) > k".
(Oct 14a) Chapter 4 typos (last three from class):
- Page 4-7, paragraph, line 3: "y2 returns call y1.tx(.)" should be "y1 returns call y1.tx(.)".
- Page 4-4, define SwpConsts: second "(0 < SW < N)" should be "(0 < RW < N)".
- Page 4-8, paragraph after A_2, line -1: "j is in [n..nd+RW-1]" should be "j is in [nr..nd+RW-1]".
- Page 4-8, last paragraph, line -2: "because ns ≥ na - SW" should be "because na ≥ ns - SW".
(Oct 9b) Hw 3: Chapter 4, exercise 2. Due oct 15 in class.
All you have to supply is a predicate B satisfying the requirements stated in exercise 2 for SwProtocol with LossyChannel. You don't need to explain how your B satisfies the requirements.
(Oct 9a) Chapter 3, problem 9, line 5: "y.tx(msg)" should be "y.tx(k,msg)" to be consistent with skeleton.
(Oct 8d) Regarding office hours, I'll be available TuTh afternoons/late mornings if you email me earlier.
(Oct 8c) Regarding item Oct 8a below, ignore the note about the typos. The sid prefix can either "y.tx(.)" or "y[Addr j].tx(.)"; in either case, the input condition has to relate the sid prefix to some state inside the service.
(Oct 8b) In case you want to meet, I'll be in my office before class (starting from 11am).
(Oct 8a) Homework 2: Due date extended to next tuesday (oct 13) because of typos in problem 9 and some of your questions.
(Oct 1) Homework 2 (due oct 8):
- Obtain inverse of Lock Service with Forced-Release; use the service program in my hw 1 solution.
- Chapter 3, problem 9.
- Chapter 3, problem 11.
(Sep 25) Chapter 2, page 2-9. Only D_0 through D_5 have been re-worked.
(Sep 25) Here is an old tutorial introduction to assertional reasoning, in case you want more examples of assertional proofs right now. If you can wait, then don't bother with this right now.
(Sep 25) Chapter 2:
- Page 2-8, definition of z(j). Change "Let z(j) denote that j does not have the lock nor is about to get it" to "Let z(j) denote that j has the lock or is about to get it".
- Page 2-9, D_0 through D_5: There are numerous errors here ("xreq[j]" and "j on a6" should appear in more places, C_6 should be C_7, ...). I'll post a revised page 2-9 tonight.
(Sep 23) Late, but hopefully less embarrassing. Chapter 2, section 2.4 onward. Only section 2.4 has been re-worked.
(Sep 22) Hw 2 (i.e., exercise 7 in chapter 2): As I mentioned in class, this is not due tomorrow or anytime soon. But do think about how to solve it.
(Sep 22) Chapter 2: I'll post a cleaned-up version of the assertional proof probably by tonight but definitely by tomorrow noon.
(Sep 20) Chapter 2 correction: page 2-6, paragraph preceding A_4, last but one sentence, "When this happens, acqd[xp] becomes true and ...". Change "true" to "false".
(Sep 18) Clarification to previous (Sep 17) item: There is no need for the conjunct "call statement before b1" because there is only one place in program Z that calls lck.aq, so we know where call goes back and what input condition is to be satisfied. If there were more than one place that calls lck.acq and their return input conditions were sufficiently different, then one would need to track where the thread goes back after lck.acq's return.
(Sep 17) Chapter 2: correction to predicate A_3 in page 2-6:
Remove the conjunct "(i at b1)" from the consequent of A_3. It's wrong. It would be ok if b1 is replaced by "call statement before b1". But it's not needed anyway.
(Sep 15) Chapter 2: corrections to figures 2.2 and 2.3 (mentioned in class)
(Sep 10) The progress assumption in LockService (figure 1-11, page 1-12) should also state that a rel() call eventually returns. So add either of the following:
- (forall user u: (u at mysid.rel.oc) leads-to (u returns from mysid.rel))
- (weak fairness for all threads)
Same addition in the progress condition of LockServiceInverse (figure 1-18, page 1-14).
(Sep 7) Hw: absorb chapter 1.
(Aug 31) Chapter 1 to be handed out on first day of class.

Overview

distributed systems

services

implement

We apply the theory to problems in concurrent programming, networking, and operating systems (for example, centralized and distributed locks, termination detection, global snapshot computation, TCP-style connection management and data transfer, wide-area routing, sequentially-consistent distributed shared memory, serializable transaction processing, atomic commits and consensus).

Time permitting, we will look at analyzing security (authentication) properties of distributed programs.

Grading / MS comp in systems area

Homeworks --- approx 50%
Exam 1 -------- approx 25%
Exam 2 -------- approx 25%
Weightages are approximate and may change by upto 10%.
The two exams together count as an MS comprehensive exam in the systems area.

Notes and papers

Chapters from a book (in preparation) will be handed out.
Homeworks will involve papers from the area.
In case you want a refresher on process synchronization problems, the following notes (from my 412 course) may be helpful.

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