2025-2026 Sem I

This course will deep dive into distributed storage systems.

In the first one-third of the course, we will familiarize ourselves with Temporal Logic of Actions (TLA+). Then in almost every lecture, we will discuss a research paper. The discussion will be led by a student presenter. Each student is expected to submit a paper review for every paper on their own.

Prerequisites

COL331 or equivalent.

Tentative evaluation criteria

  • Paper presentation: 25%
    • This includes presenting a paper, creating a quiz for the class, and evaluating the quiz.
    • Presentation schedule
  • Quiz: 10%
    • Every discussed paper will have a quiz. This will be taken before the class. Other classes, such as on TLA+, may also have a quiz. All quizzes will be pre-announced (no surprise quizzes).
  • Paper reviews: 30%
    • This includes writing a summary of the paper and your commentary on what could be improved. Submit it on Gradescope before class begins.
  • Project: 35%
    • You can either model a system from scratch in TLA+ to argue about its correctness and show interesting edge cases/optimization that were not obvious in the paper.
    • Or you can implement a system from scratch and evaluate its performance.

Ethics

Paper reviews: You are encouraged to discuss papers with your peers. But each review must be written independently. If two student reviews are found to be copied, both reviews will be penalized. It is encouraged to note in the header: “Paper discussed with student XYZ”. You can use LLMs to help you understand the paper. But the paper review must be written by you.

Quizzes: Please do not share your quiz with your peers.

Paper presentation: You are allowed to reuse slides from other presentations. But this has to be acknowledged at the start of presentation.

Tentative schedule

Date Topic
25 Jul.
Friday.		 1. Introduction to distributed storage systems. CAP theorem. Linearizability.
27 Jul.
Sunday.		 2. Leslie’s lectures 1-4.
29 Jul.
Tuesday.		 3. Read/write some TLA+ specs. Two phase commits for distributed transactions.
1 Aug.
Friday.		 4. Leslie’s lectures 5-6.
3 Aug.
Sunday.		 5. Add restarts to two-phase commit specification. CR, CRAQ.
5 Aug.
Tuesday.		 6. Leslie’s lecture 8(a, b).
8 Aug.
Friday.		 7. Prove that two phase commits implements transaction commits. Prove that CR is linearizable.
10 Aug.
Sunday.		 8. Leslie’s lecture 9(a, b).
12 Aug.
Tuesday.		 9.
14 Aug.
Thursday		 10.
15 Aug.
Friday.		 Independence Day
19 Aug.
Tuesday.		 11.
22 Aug.
Friday.		 12.
26 Aug.
Tuesday.		 13.
29 Aug.
Friday.		 14.
2 Sep.
Tuesday.		 15.
5 Sep.
Friday.		 Milad-un-nabi
9 Sep.
Tuesday.		 16.
12 Sep.
Friday.		 Exam week
16 Sep.
Tuesday.		 Exam week
19 Sep.
Friday.		 Likely no class
23 Sep.
Tuesday.		 Likely no class
26 Sep.
Friday.		 Likely no class
30 Sep.
Tuesday.		 Semester break
3 Oct.
Friday.		 Semester break
7 Oct.
Tuesday.		 17.
10 Oct.
Friday.		 18.
14 Oct.
Tuesday.		 19.
17 Oct.
Friday.		 20.
21 Oct.
Tuesday.		 21.
24 Oct.
Friday.		 22.
28 Oct.
Tuesday.		 23.
31 Oct.
Friday.		 24.
4 Nov.
Tuesday.		 25.
7 Nov.
Friday.		 26. Project presentation
11 Nov.
Tuesday.		 27. Project presentation
14 Nov.
Friday.		 28. Course wrap up