2025-2026 Sem I

This course will deep dive into distributed storage systems.

In the first part of the course, we will familiarize ourselves with Temporal Logic of Actions (TLA+). In the second part, we will discuss a research paper in every class. The paper discussion will be led by student presenters. Each student is expected to submit a paper review for every paper on their own.

Logistics

  • Prerequisites: COL331 or equivalent.
  • Timings: Tuesdays and Fridays. 2-3:30pm. AC Slot.
  • Place: LH421
  • Emails may not be answered in a timely manner. Instead, please post here.
  • Class material can be found here.

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).
    • There will be no makeup quizzes. Best N-1 out of N will be considered.
  • 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.
    • There will be no makeup paper reviews. Best N-1 out of N will be considered.
  • Project: 35%
    • You can model a (non-trivial) system from scratch in TLA+ to argue about its correctness and show interesting edge cases/optimization that were not obvious in the paper.
    • And/Or you can implement a (non-trivial) system from scratch and evaluate its performance.

Audit criteria: 30% or more marks. Present a paper.

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. Safety and Liveness. Linearizability.
Recommended reading: How Amazon web services uses formal methods
27 Jul.
Sunday.		 2. Leslie’s lectures 1-4.
29 Jul.
Tuesday.		 3. Read/write some TLA+ specs.
1 Aug.
Friday.		 4. Distributed transactions. Serializability. Concurrency control for isolation. Two-phase commits for atomicity.
3 Aug.
Sunday.		 5. Leslie’s lectures 5-6.
5 Aug.
Tuesday.		 6. Read TLA+ specs for transaction commit and two-phase commit. Restarts in two-phase commits.
8 Aug.
Friday.		 7. Chain Replication. Replicated state machines. Write TLA+ specs for single server key-value store and a chain replicated key-value store. Take home Quiz 1.
10 Aug.
Sunday.		 8. Leslie’s lectures 8(a,b).
12 Aug.
Tuesday.		 9. Prove that two-phase commit implements transaction commit.
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.
30 Aug.
Saturday.		 15.
2 Sep.
Tuesday.		 16.
5 Sep.
Friday.		 Milad-un-nabi
9 Sep.
Tuesday.		 17.
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.		 18.
10 Oct.
Friday.		 19.
14 Oct.
Tuesday.		 20.
17 Oct.
Friday.		 21.
21 Oct.
Tuesday.		 22.
24 Oct.
Friday.		 23.
28 Oct.
Tuesday.		 24.
31 Oct.
Friday.		 25.
4 Nov.
Tuesday.		 26.
7 Nov.
Friday.		 27. Project presentation
11 Nov.
Tuesday.		 28. Project presentation
14 Nov.
Friday.		 29. Course wrap up