Reto Achermann
Assistant Professor
Systopia Lab
Department of Computer Science
University of British Columbia
Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems
Authors
Travis Hance, Andrea Lattuada, Reto Achermann, Alex Conway, Ryan Stutsman, Gerd Zellweger, Chris Hawblitzel, Jon Howell and Bryan Parno
Venue
Proceedings of the 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI'23)
Links
Abstract
We present IronSync, an automated verification framework for concurrent code with shared memory. IronSync scales to complex systems by splitting system-wide proofs into isolated concerns such that each can be substantially automated. As a starting point, IronSync's ownership type system allows a developer to straightforwardly prove both data safety and the logical correctness of thread-local operations. IronSync then introduces the concept of a Localized Transition System, which connects the correctness of local actions to the correctness of the entire system. We demonstrate IronSync by verifying two state-of-the-art concurrent systems comprising thousands of lines: a library for black-box replication on NUMA architectures, and a highly concurrent page cache.
Bibtex
@inproceedings{Hance:2023:SSM,
author = {Hance, Travis and Lattuada, Andrea and Achermann, Reto and Conway, Alex and Stutsman, Ryan and Zellweger, Gerd and Hawblitzel, Chris and Howell, Jon and Parno, Bryan},
booktitle = {Proceedings of the 17th USENIX Symposium on Operating Systems Design and Implementation},
id = {Hance:2023:SSM},
isbn = {978-1-939133-34-2},
location = {Boston, MA, USA},
pages = {911--929},
publisher = {USENIX Association},
series = {OSDI'23},
title = {Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems},
url = {https://www.usenix.org/conference/osdi23/presentation/hance},
year = {2023}
}
