Compiling Distributed System Models with PGo, and Beyond

Add to your list(s) Download to your calendar using vCal

• Finn Hackett, Systopia lab and Software Practices Lab, University of British Columbia
• Thursday 14 November 2024, 15:00-16:00
• Zoom, https://christs-cam-ac-uk.zoom.us/j/99963336965?pwd=vW8ItPcOU2pRe6heGIHyk1CNanIfVr.1.

If you have a question about this talk, please contact Richard Mortier.

Distributed Systems are inherently hard to build and reason about. Their combination of asynchrony and partial failures leads to complex edge cases that are rarely repeatable under test conditions. To address this problem, we can use formal methods to formally model and analyze our distributed systems, detecting error scenarios before they reach production. Taking the idea further, we can compile our formal model into an implementation, minimizing the chances that our formal models and systems exhibit diverging behavior. Our compiler PGo does this, and we have used it to develop a collection formally verified distributed systems. Of those, our verified Raft-based key-value store PGo-RaftKV outperforms related work that is compiled from formal models. The story isn’t over, however. Spec-compiled code is still not performance-competitive with hand-written production systems like etcd, and spec-compiled code can still have bugs (in how the verified protocol interacts with the world). We describe our work so far, as well as follow-up work we have begun that addresses remaining shortfalls in compiling distributed system models into practical implementations.

Bio:

Finn is a Ph.D. student exploring practical applications of programming language design and formal verification, currently on internship with the VeriDis team at Inria. As a member of the Systopia lab and Software Practices Lab at the University of British Columbia, Finn aims to build language-level tools that help developers interact more confidently with the complex and unintuitive design problems that arise when building practical systems. Finn’s most recent work is PGo, a TLA +-based domain-specific language for developing formally verified distributed systems.

This talk is part of the Computer Laboratory Systems Research Group Seminar series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• CL's SRG seminar
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Computer Laboratory Systems Research Group Seminar
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• Zoom, https://christs-cam-ac-uk.zoom.us/j/99963336965?pwd=vW8ItPcOU2pRe6heGIHyk1CNanIfVr.1
• bld31
• ndk22's list
• ob366-ai4er
• rp587

Note that ex-directory lists are not shown.