Lectures

10 Dec

The last four Student Presentations, and time for Course Evaluation.

8 Dec

Quiz due. Six more Student Presentations.

3 Dec

Student Presentations on Mutual Exclusion algorithms in message-passing systems.

1 Dec
Byzantine consensus.
19 Nov
Discussion of Homework Five. Presentation on the Renaming Problem. Introducing Self-Stabilization.
17 Nov

Update on Homework, finishing Shared-Memory Snapshots, plan for rest of semester discussed.

12 Nov

Shared-Memory Snapshots and questions about current Homework.

10 Nov

Looking at memory-to-memory move operation to solve consensus. After that, beginning the new Readings assignment, snapshot objects.

5 Nov

Lecture on the consensus hierarchy, following the assigned reading. Key terminology in the lecture: univalent, bivalent, x-valent, y-valent, decided. Announcing Homework 4, see Homework page.

3 Nov

Lecture devoted to the universal construction, ACM Transactions on Programming Languages and Systems, Volume 11, Number 1, pages 143-146 (only those four pages of the article). The lecture outlines the proof, by showing a simulation, that using wait-free consensus objects and some atomic register arrays, that any object with methods can be concurrently accessed by n processes in a wait-free and linearizable way.

29 Oct

Quiz covering linearizability, sequential consistency, mutual exclusion and related topics from lectures and reading assignments. Start of next Readings topic on shared-object consensus. Introducing Wait-Free Consensus.

27 Oct

CC vs DSM and Exclusion for Multiple Resources; new assigned Readings for 29 Oct.

22 Oct

N-Process Mutual Exclusion is the main topic; discussion of Homework also.

20 Oct

Covering basic mutual exclusion algorithms from the assigned reading. TestAndSet Mutex in TLA, RMW Mutex in TLA, Peterson's Algorithm.

15 Oct

Questions about the homework? Students might take time to ask questions about the current homework. Start covering chapter on mutual exclusion: Sequential Control and Hardware for Shared Memory Concurrency.

13 Oct

Finishing the simulations between shared-memory and message-passing models; announcement of next Homework and new Readings assigned. See Shared Memory and Messages for background. Document camera notes.

8 Oct

Some coverage of Chapter 16 from the assigned reading; also discussion of PlusCal, which will be used in an upcoming homework.

6 Oct

Coverage of Chapter 15 from the assigned reading: Shared Object Linearizability.

1 Oct

Quiz covering causality, Lamport clock, vector clocks, snapshots, consistent cuts. Start of shared object communication, beginning with Shared Memory Consistency.

29 Sep

Brief mention of Homework Two solutions. Finish distributed snapshots (see new reading assignment, Chapters 15-16 on the Readings page). See Distributed Snapshot for lecture notes.

24 Sep

On vector clocks, introduction to distributed snapshots. See the Transforms page for some notes on this lecture.

22 Sep

First, explanation of TLA Simulation, then a discussion of Homework One solutions submitted by students (not everyone understands how synchronous and asynchronous computations are expressed in TLA).

17 Sep

Initial coverage of Causal consistency, Logical clock, Lamport timestamps, and Vector clock. How time in an asynchronous system can be partially ordered, unlike real time which is totally ordered.

15 Sep

A lecture on invariants. Notes: Invariants.pdf. New reading assignment: Chapter 12 in the course notes, on Logical Clocks. Second homework (on invariants) due 22 September.

10 Sep

This lecture can finish some issues in Chapters 1, 2, and 4, but also more carefully look at TLA tools, since these will be needed for some homeworks. Much of the lecture goes over TLA Simplified in enough detail to do the first Homework, due next Tuesday.

8 Sep

Part of the lecture covers Chapter 4 of the course notes, on Flooding (Broadcast) and the inverse operation of Convergecast. The lecture will also cover some previous material not discussed, on Chapters 1 and 2, so that models of distributed computing are made more clear. Handouts: AlgorithmsChap4.pdf and IntroInvariant.pdf.

3 Sep

Using TLA tools, a first lecture/demonstration. The current TLA Home Page is a starting point for an abstract view of TLA concepts (see also the Wikipedia Page on TLA as another starting point). But to dig into the application of TLA, start with the TLA Proof System Page, which has instructions on downloading and installing the software. During the lecture, some examples of TLA were shown and briefly explained. A TLA Example shows the beginnings of a specification of a distributed algorithm and a proof; there is also a more familiar language, PlusCal, which can be converted to TLA. At the end of the lecture, TLA on AWS was briefly demonstrated.

1 Sep

Models in Distributed Computing and Coordinated Attack Problem. Notes: Chap1Notes.pdf, Chap2Notes.pdf, Chap3Notes.pdf.

27 Aug

Lecture accompanies Chapter 1 and Chapter 2 of Lamport's TLA book (pdf file on ICON). Handout: temporal-logic.pdf.

25 Aug

Introduction Day, including Syllabus and a distributed computing puzzle, as a gentle introduction to the course. Handout: stadium.pdf.

Lectures (last edited 2015-12-08 16:09:59 by Ted Herman)