Distributed Systems Verification
A distributed system is one in which the failure of a computer you didn’t even know existed can render your own computer unusable. – Leslie Lamport, 1987.
Distributed systems are the workhorses of modern day computing. Applications ranging from home automation systems to e-commerce, payment gateways, and cryptocurrencies all rely on distributed systems to meet their computational needs, and scale to millions of users across the planet. Unfortunately though, the ubiquity of distributed computing hasn’t resulted in a proportional decrease in the complexity of distributed programming; building reliable and scalable distributed systems/applications remains hard despite decades of progress in this direction. In this seminar course, we shall review the fundamental challenges inherent in building provably-correct distributed systems, discuss recent advances addressing or circumventing the challenges, and explore ways to extend the state-of-the-art in Distributed Program Verification.
As conveyed by the title, our emphasis in this course will be on the specification and verification of distributed systems and applications. Formal verification often invokes unfortunate connotations of impracticality. We shall try to avoid this pitfall by prioritizing the study of theories, techniques, and systems with strong practical implications. The course is research-oriented meaning that there will be student-led discussions on research papers and industry tech reports. It will be hands-on meaning that there will be programming assignments (most likely in TLA+ and PlusCal) and a course project (to be proposed independently by each student). To set a common ground for subsequent research discussions, I will review the fundamental concepts of Distributed Systems and Program Verification in the first few lectures. The schedule can be found here.
Essential Details
- Instructor: Gowtham Kaki.
- Where: Zoom (Email me for the passcode)
- When: T,Th 11:10 AM - 12:25 PM
- Office Hours: On Piazza or by appointment.
Grading
| Item | Due | Weightage (%) |
|---|---|---|
| Programming Assignment ( TLA+/PlusCal) | – | 25 |
| Research paper presentations | – | 30 |
| Project based on a research paper | – | 30 |
| Contributing to paper discussions | – | 15 |
Acknowledgements
The course borrows some of the materials from