Note that some links may only work within the Cornell domain, so you may have to set up a VPN
Week | Day | Date | Topic | Reading | Notes | |
---|---|---|---|---|---|---|
1 | Thu | Aug 26 | Administrivia and Specifying Concurrent Systems | How to read a paper and Sections 1-3 of Specifying Concurrent Systems with TLA+ | ||
2 | Tue | Aug 31 | More on specification / intro to first programming project | Epidemic algorithms for replicated database maintenance by Alan Demers et al. | Due Aug 31, 9am | |
Thu | Sep 2 | Specification continued | A Simple Approach to Specifying Concurrent Systems (Sections 1-3, 4 optional) by Leslie Lamport | Due Sep 4 | ||
3 | Tue | Sep 7 | Instantiation and Refinement | Use of Formal Methods at Amazon Web Services | Due Sep 7, 9am | |
Thu | Sep 9 | Mutual Exclusion, Inductive Invariants, and Model Checking | Hints and Principles for Computer System Design by Butler Lampson up to and including Section 3.4 | Due Sep 9, 9am | ||
4 | Tue | Sep 14 | Consistency | Hints and Principles for Computer System Design by Butler Lampson, remainder | Due Sep 14, 9am | |
Thu | Sep 16 | Two-Phase Commit and Chain Replication | Chain Replication by Robbert van Renesse and Fred B. Schneider | Due Sep 16, 9am | ||
5 | Tue | Sep 21 | Failure Models, Consensus | no review assignment | ||
Thu | Sep 23 | Paxos | Paxos made simple by Leslie Lamport | Due Sep 23, 9am | ||
6 | Tue | Sep 28 | Byzantine failures | Making Distributed Systems Robust | Due Sep 28, 9am | |
Thu | Sep 30 | Permissionless Blockchains | Bitcoin: A Peer-to-Peer Electronic Cash System by Satoshi Nakamoto | Due Sep 30 | ||
7 | Tue | Oct 5 | Paper Presentation | The nanoPU: A Nanosecond Network Stack for Datacenters (Shubham Chaudhary) | Due Oct 4, 9am | |
Thu | Oct 7 | Paper Presentation | Ethane: taking control of the enterprise (William Ma) | Due Oct 6, 9am | ||
8 | Tue | Oct 12 | Fall Break -- no class | |||
Thu | Oct 14 | Paper Presentation | Just Say NO to Paxos Overhead (Nitika Saran) | Due Oct 13, 9am | ||
9 | Tue | Oct 19 | Paper Presentation | Viaduct: an extensible, optimizing compiler for secure distributed programs (Allen Yao) | Due Oct 18, 9am | |
Thu | Oct 21 | Paper Presentation | Komodo: Using verification to disentangle secure-enclave hardware from software (Priya Srikumar) | Due Oct 20, 9am | ||
10 | Tue | Oct 26 | Paper Presentation | Nickel: A Framework for Design and Verification of Information Flow Control Systems (Goktug Saatcioglu) | Due Oct 25, 9am | |
Thu | Oct 28 | Paper Presentation | CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels (Ariel Kellison) | Due Oct 27, 9am | ||
11 | Tue | Nov 2 | Paper Presentation | The benefits and costs of writing a POSIX kernel in a high-level language (Abhishek Kumar) | Due Nov 1, 9am | |
Thu | Nov 4 | Paper Presentation | SKQ: Event Scheduling for Optimizing Tail Latency in a Traditional OS Kernel (Yueying Li) | Due Nov 3, 9am | ||
12 | Tue | Nov 9 | Paper Presentation | A Case for Lease-Based, Utilitarian Resource Management on Mobile Devices (Sachille Atapattu) | Due Nov 8, 9am | |
Thu | Nov 11 | Paper Presentation | Dorylus: Affordable, Scalable, and Accurate GNN Training with Distributed CPU Servers and Serverless Threads (Noah Bertram) | Due Nov 10, 9am | ||
13 | Tue | Nov 16 | Paper Presentation | Heterogeneity-Aware Cluster Scheduling Policies for Deep Learning Workloads (Alicia Yang) | Due Nov 15, 9am | |
Thu | Nov 18 | Paper Presentation | A Hierarchical Model For Device Placement (Katy Blumer) | Due Nov 17, 9am | ||
14 | Tue | Nov 23 | Paper Presentation | Scalable and Probabilistic Leaderless BFT Consensus through Metastability (Rodrigo Delgado) | Due Nov 22, 9am | |
Thu | Nov 25 | Thanksgiving Break | ||||
15 | Tue | Nov 30 | Paper Presentation | Generalized Byzantine-tolerant SGD (Tao Yu); Bao: Making Learned Query Optimization Practical (Victor Giannakouris) | Due Nov 29, 9am | |
Thu | Dec 2 | Projects Presentations | 9-11am | |||
16 | Tue | Dec 7 | Projects Presentations | 9-11am |