Teaching rigorous distributed systems with efficient model checking

Download: PDF, slides (PDF), slides (Keynote).

“Teaching rigorous distributed systems with efficient model checking” by Ellis Michael, Doug Woos, Thomas Anderson, Michael D. Ernst, and Zachary Tatlock. In EuroSys, (Dresden, Germany), Mar. 2019, pp. 1-15.

Abstract

Writing correct distributed systems code is difficult, especially for novice programmers. The inherent asynchrony and need for fault-tolerance make errors almost inevitable. Industrial-strength testing and model checking have been shown to be effective at uncovering bugs, but they come at a cost — in both time and effort — that is far beyond what students can afford. To address this, we have developed an efficient model checking framework and visual debugger for distributed systems, with the goal of helping students find and fix bugs in near real-time. We identify two novel techniques for reducing the search state space to more efficiently find bugs in student implementations. We report our experiences using these tools to help over two hundred students build a correct, linearizable, fault-tolerant, dynamically-sharded key-value store.

Download: PDF, slides (PDF), slides (Keynote).

BibTeX entry:

@inproceedings{MichaelWAET2019,
   author = {Ellis Michael and Doug Woos and Thomas Anderson and Michael
	D. Ernst and Zachary Tatlock},
   title = {Teaching rigorous distributed systems with efficient model
	checking},
   booktitle = {EuroSys},
   pages = {1-15},
   address = {Dresden, Germany},
   month = mar,
   year = {2019}
}

(This webpage was created with bibtex2web.)

Back to Michael Ernst's publications.