Lecture Summaries

Not intended to be a detailed transcript of each class meeting, but rather a brief description and possibly some pointers to sources.

About homework, new deadline, a look at real-time clock snapshot paper from a 2017 conference.

Continue a little with stabilization0.pdf and then stabilization1.pdf. Also, a bit more about the current CRDT assignment/report.


Further discussion of current homework (solution to Homework 6). The link register communication model: stabilization0.pdf


Discussion of current homework. Some CRDT questions: CRDTq.pdf.


New homeworks. Wait-free atomic snapshot waitfree2.pdf.


Look at the universal construction in waitfree1.pdf. Class exercise, specify consensus object in TLA.


Finish the proof in waitfree0.pdf. Time permitting, start waitfree1.pdf.


See updates on Homework5 due in a week. First mention of the Producer-consumer problem consumer0.pdf. Begin Chapter 18 by introduction of Non-blocking algorithm and wait-freedeom waitfree0.pdf.


New homework due 14 November. Most of the class time looked at proving Kessels Algorithm correct: kessels.pdf.

Discussion of current homework. The class time was devoted to detailed reading (out loud) part of Chapter 16 of the distributed computing notes and making sense of the simulation algorithms.

New homework assigned. In-class demonstration of TLA-Toolbox (not required to do the homework). Main topic of the lecture is linearizability shared2.pdf.


Introducing shared memory objects shared1.pdf. Preview of next homework: TLA for single-writer mutual exclusion protocol.


The course moves on to shared memory distributed computing shared0.pdf. Most of the class time will be for the second exam.


Reminder - exam on Thursday! Continue with consensus consensus1.pdf. Not shown in lecture, but may be a way to understand how Raft works: http://thesecretlivesofdata.com/raft/


Sample solutions to Homework3. Continue with algorithm for Byzantine consensus consensus0.pdf (and if students would like the impossibility proof for n=3f imposs0.pdf). Then a quick look at leader election in message-passing systems.


Reminder, third homework due soon. Fairness added to logic4.pdf, also read the description of fairness in the c-manual for PlusCal. For the main topic, we begin looking at message-passing consensus problems, hopefully getting to Byzantine consensus consensus0.pdf.


Continue with graph0.pdf and introduce a couple more temporal operators in logic4.pdf.


Introducing graph algorithms in message-passing distributed systems. Lecture notes: graph0.pdf, and Distributed minimum spanning tree.


Continue with the theme of cuts, covering distributed snapshot. Notes: snapshot0.pdf. One reference is the Chandy-Lamport algorithm. Some class time also for answering questions about the homework (see added hints to the PDF description of the homework).


Begin covering the PlusCal language (C-variant). The main example is pluscal1.pdf. For in-class demonstrations, ClockMutex.tla, ClockMutex.cfg.


Coverage of Chapter 7 begins. Notes are cuts0.pdf. A related algorithm, if time permits, is Lamport's distributed mutual exclusion algorithm.


Finish Chapter 3 with impos0.pdf. Questions about current homework? Moving on next to Chapter 7 of Distributed Algorithm book.


The class meeting starts with another TLC demonstration (notes intlc2.pdf) which shows how to deal with n-process mutual exclusion (some new TLA notation is used). Then the algorithms from Chapter 3 of the Distributed Algorithm book.


Start Chapter 2 from Distributed Algorithm book, also selected topics from Chapter 4 of TLA book: logic3.pdf. Also, a quick derivation of one question's answer in the exam: dual.pdf


First Exam. Then a demonstration of TCL, transcript in tlc1.pdf


Covering Chapter 3 of the TLA book. See notes in logic2.pdf.


Continue with the notes logic0.pdf. Covered part of TLA introduction, in notes logic1.pdf.


The topic for the next several class meeting is TLA+. This Tuesday meeting begins with a review of logic, then a quick look at predicate logic and temporal logic. Here are logic0.pdf some notes.


Class meeting introduced the problem of mutual exclusion, based on these notes. Also, each student invited to email office hours preference to instructor.


Syllabus and general description of the situation in distributed computing. Some sources (textbooks, notes, papers). Mention of some topics. The course will provide background on research in an active topic, namely (theory of) distributed systems. Some topics even generate debate.

Lectures (last edited 2017-12-07 16:59:53 by Ted Herman)