## Lecture Summaries

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

- 16Nov
**New homeworks.**Wait-free atomic snapshot waitfree2.pdf.- 14Nov
Look at the universal construction in waitfree1.pdf. Class exercise, specify consensus object in TLA.

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

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

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

- 31Oct
- 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.
- 26Oct
New homework assigned. In-class demonstration of TLA-Toolbox (not required to do the homework). Main topic of the lecture is linearizability shared2.pdf.

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

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

- 17Oct
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/

- 12Oct
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.

- 10Oct
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.

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

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

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

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

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

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

- 14Sep
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.

- 12Sep
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

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

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

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

- 29Aug
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.

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

- 22Aug
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.