CS 371D – Distributed Computing

Spring 2024

Distributed protocols are at the foundation of modern cloud computing services but are notoriously difficult to define and implement correctly. In this class, we will survey some important methods and concepts in distributed computing, including logical clocks, consistency models, fault tolerance, consensus, sharding, peer-to-peer protocols, cache coherence and distributed transactions, as well as important systems applying these ideas. The class will be divided roughly into one half theory and one half practical application.

An overview of the concepts covered in the class can be found in the introductory slides from Spring 2023.

The class will consist of lecture and a series of lab assignments. The labs are protocol design and implementation exercises that build from simple replicated stores to a scalable fault-tolerant  system using distributed consensus. The labs will be implemented in Java. We will test our systems in a simulated distributed environment and use model checking, a technique of systematic state space exploration, to help us find subtle concurrency bugs that are difficult to find by testing alone. Grading will be based on the labs. There will be no final exam. 

CS 395T: The Model Checking Paradigm

Spring 2021

Course Description

Model checking and related techniques of automatic formal verification emerged in the early 1980’s. These methods present a cost and a benefit: we must model our system and write our specification in very restricted forms, but in exchange for this we obtain proofs and counterexamples automatically. Despite early successes, this approach immediately led to difficult problems, for example, how to extend the expressiveness of the models to allow the verification of real systems, while keeping the proofs tractable. The model checking paradigm is the collection of strategies that researchers developed for resolving these problems.

The class will survey a sampling of research topics within the model checking paradigm, with a view to elucidating the high-level strategies, while disregarding algorithmic details. In this way, we will try to make some sense of the diverse and not always coherent literature in the field. The goal is for students to be able to read critically and put into context recent papers in areas such as software model checking, cyber-physical systems or neural network verification.