News

• (Jan 15) HOT 
  • Final scores and grades (same format as before) posted.
  • Some grades went up.
  • Solutions will be given out after one remaining student hands in hw7/exam2 (it may be a while).
• (Jan 6)
  • For those who submitted hw7 and exam2, course/comp grades are posted. If you took the comp, your grade has the form "X/Y", where X is the course grade and Y is the comp grade.
  • Solutions will be given out after all hw7/exam2 submissions are turned in (it may be a while).
• (Dec 16b)
  • Hw7 and exam2 scores posted (for the ones submitted).
  • Course grade given as a comment for those who submitted hw7 and exam2. These will be officially submitted later this evening.
  • For those who have not submitted hw7 or exam2, you will have an official course grade of Incomplete for now.
• (Dec 16a) Exam 2:
  • If you want you can assume that when a node receives [ACK,t,j], it updates clk to max(clk,t). (So at most one request is in transit from i to j.)
• (Dec 14e) In page 3, second bullet:"mod(N,t)" should be "mod(t,N)". In page 4, underlined part of doRx: "mod(N,msg[1])" should be "mod(msg[1],N)".
• (Dec 14d) Exam 2
  • You can add additional parameters to function unMod(.). (I assumed that its body can access the variables of the program and local variables of doRx, but if you don't like the latter then feel free to add "msg" (and anything else) as a parameter.)
  • As mentioned in the exam, messages contain unbounded timestamps but only the modulo-N value is available to the program at reception. (The intentions is to make the unbounded timestamps available for analysis without having to introduce an auxiliary field in the messages.)
• (Dec 14c) Exam3 (MS-comp) scores posted. (MS-comp grade after I get exam2.)
• (Dec 14b) As mentioned in class, the tuesday 6pm deadline for hw7-exam2 applies if you want your class grade issued before Dec 22 (campus deadline). If you don't mind getting the grade later, you can hand it in later (upto say, Jan 4). Personally, I'd prefer an immaculate submission.
• (Dec 14a) Hw 7, function "loopOn": add the "while(true)" to surround 1..13.
• (Dec 13b) In case you're stuck in hw 7, you can try the approach in the proof of the original bakery algorithm.
• (Dec 13a) Hw 5 and 6 grades posted.
  • Hw 6: 10/20 if you gave me an algorithm with no explanation (of working, meaning of variables, etc.).
• (Dec 11a) Please fill out the class evaluations if you haven't yet: https://www.courseevalum.umd.edu/portal.
• (Dec 10c) Please email me your hw6 scores. Got the scores.
• (Dec 10b) Homework 7 and Exam 2 - version 4. Typos (hopefully all) fixed in hw 7.
  One more fixed (bullet in line 11).
• (Dec 9b) MS comp exam 2a:
  • Friday Dec 11 3:30pm in AV Williams 4185 (facing elevator).
  • Open notes
• (Dec 9a) Homework 7 and Exam 2 - version 3. Hw7 and Exam2 updated (fixes to BlackWhiteBakery program, outline of timestamp program, assertions to be proved or disproved). There shouldn't be any more updates other than typos.
• (Dec 8) Homework 7 and Exam 2 - version 2. Hw7 updated with a BlackWhiteBakery program. There may be typos.
• (Dec 6) Typos in chapter 11:
  • Figure 11-4 has "reqQ.front()[1] = i and lessReqQHts()" in two places. The "i" should be "aL".
  • > After Figure 11.4 you have "If G does not hold, the thread signals
    > condAcqRet (to wake up another waiting user) and goes back to waiting on
    > condAcqRet" I do not see any condAcqRet.signal().
    Insert a wait before the while loop and a signal before the wait in the loop.

    condAcqRet.wait;
    while not G {
       condAcqRet.signal;
       condAcqRet.wait;
    }
    

• (Dec 4) Homework 7 and Exam 2.
• (Dec 3) Scheduling MS comp exam.
  • Re the MS comp exam some time, please tell me your availability during Dec 11-15. (Dec 11 (Fri) is the last day of class. Dec 12, 13 (Sat, Sun) are study days.)
  • If we cannot settle on a time, it will be during the last class (Dec 10).
• (Nov 30) Hw 6: You can refer to existing papers. No need for an assertional proof.
• (Nov 28a) Typos in chapter 9:
  • Safety proof of section 9.3: "holds (since i would be at s5)". Delete the parenthetical note.
  • Safety proof of section 9.3: "Similarly, if acqd[i] is true, then..." should be "... acqd[j]...".
  • Figure 9.3a: In t2, choosing[mytid] should be set to false.
  • Safety proof in section 9.5, second to last paragraph: "Step i.s2 with i.p = j preserves it because nothing changes if the while test fails and the predicate holds vacuously if it succeeds". Reverse "fails" and "succeeds".
• (Nov 28a) As mentioned in class, hw 6 (bounding num values in the bakery algorithm) is also due Dec 1 in class.
• (Nov 26) Typo in hw-5: "tNs > tauNow + minNs" should be "tauNow > tNs + minNs"
• (Nov 22b) 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) 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.
  Typos in problem 9: In tx, change "y[Addr j]" to "y". In rx, change "v[Addr j]" to "y".
• (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

This course deals with the compositional design and analysis of distributed systems (in which we include concurrent, parallel, and interactive systems with real-time and non-real-time behavior). The course emphasizes correctness and compositionality. Distributed systems and their services (i.e., "specifications" in software engineering lingo) are defined separately by (distributed) programs. We learn what it means for a system program A to implement a service program A, how to establish this, and why this ensures that A can be used in any distributed system where B is used.

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.
  • Note-5: N process mutual exclusion
  • Note-6: Peterson 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

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