Compiling Distributed System Models with PGo, and Beyond

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

• Finn Hackett
• Thursday 11 July 2024, 15:00-16:00
• FW11 and https://meet.jit.si/cambridge-cl-srg-seminar.

If you have a question about this talk, please contact Ryan Gibb.

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.

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
• FW11 and https://meet.jit.si/cambridge-cl-srg-seminar
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• rp587

Note that ex-directory lists are not shown.