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.

Lectures (last edited 2017-11-16 14:17:12 by Ted Herman)