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\, Systopia lab and Software Practices Lab\, University of British C
 olumbia
DTSTART:20241114T150000Z
DTEND:20241114T160000Z
UID:TALK224308@talks.cam.ac.uk
CONTACT:Richard Mortier
DESCRIPTION:Distributed Systems are inherently hard to build and reason ab
 out. Their\ncombination of asynchrony and partial failures leads to comple
 x edge\ncases that are rarely repeatable under test conditions. To address
  this\nproblem\, we can use formal methods to formally model and analyze o
 ur\ndistributed systems\, detecting error scenarios before they reach\npro
 duction. Taking the idea further\, we can compile our formal model\ninto a
 n implementation\, minimizing the chances that our formal models\nand syst
 ems exhibit diverging behavior. Our compiler PGo does this\, and\nwe have 
 used it to develop a collection formally verified distributed\nsystems. Of
  those\, our verified Raft-based key-value store PGo-RaftKV\noutperforms r
 elated work that is compiled from formal models. The story\nisn't over\, h
 owever. Spec-compiled code is still not\nperformance-competitive with hand
 -written production systems like etcd\,\nand spec-compiled code can still 
 have bugs (in how the verified protocol\ninteracts with the world). We des
 cribe our work so far\, as well as\nfollow-up work we have begun that addr
 esses remaining shortfalls in\ncompiling distributed system models into pr
 actical implementations.\n\nBio:\n\nFinn is a Ph.D. student exploring prac
 tical applications of programming\nlanguage design and formal verification
 \, currently on internship with\nthe VeriDis team at Inria. As a member of
  the Systopia lab and Software\nPractices Lab at the University of British
  Columbia\, Finn aims to build\nlanguage-level tools that help developers 
 interact more confidently with\nthe complex and unintuitive design problem
 s that arise when building\npractical systems. Finn's most recent work is 
 PGo\, a TLA+-based\ndomain-specific language for developing formally verif
 ied distributed\nsystems.
LOCATION:Zoom\, https://christs-cam-ac-uk.zoom.us/j/99963336965?pwd=vW8ItP
 cOU2pRe6heGIHyk1CNanIfVr.1
END:VEVENT
END:VCALENDAR