BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Compiling Distributed System Models with PGo\, and Beyond - Finn H
 ackett
DTSTART:20240711T140000Z
DTEND:20240711T150000Z
UID:TALK218707@talks.cam.ac.uk
CONTACT:Ryan Gibb
DESCRIPTION:Distributed Systems are inherently hard to build and reason ab
 out. Their \ncombination of asynchrony and partial failures leads to compl
 ex edge \ncases that are rarely repeatable under test conditions. To addre
 ss this \nproblem\, we can use formal methods to formally model and analyz
 e our \ndistributed systems\, detecting error scenarios before they reach 
 \nproduction. Taking the idea further\, we can compile our formal model \n
 into an implementation\, minimizing the chances that our formal models \na
 nd systems exhibit diverging behavior. Our compiler PGo does this\, and \n
 we have used it to develop a collection formally verified distributed \nsy
 stems. Of those\, our verified Raft-based key-value store PGo-RaftKV \nout
 performs related work that is compiled from formal models. The story \nisn
 't over\, however. Spec-compiled code is still not \nperformance-competiti
 ve with hand-written production systems like etcd\, \nand spec-compiled co
 de can still have bugs (in how the verified protocol \ninteracts with the 
 world). We describe our work so far\, as well as \nfollow-up work we have 
 begun that addresses remaining shortfalls in \ncompiling distributed syste
 m models into practical implementations.\n
LOCATION:FW11 and https://meet.jit.si/cambridge-cl-srg-seminar
END:VEVENT
END:VCALENDAR