Verifying concurrent, crash-safe systems with Perennial

SOSP presentation

Here are the slides for the SOSP presentation.

SOSP paper

We have an SOSP 2019 paper describing Perennial's techniques, the Goose translator, and a broad evaluation of several aspects of Perennial's implementation.

Here's the abstract:

This paper introduces Perennial, a framework for verifying concurrent, crash-safe systems. Perennial extends the Iris concurrency framework with three techniques to enable crash-safety reasoning: recovery leases, recovery helping, and versioned memory. To ease development and deployment of applications, Perennial provides Goose, a subset of Go and a translator from that subset to a model in Perennial with support for reasoning about Go threads, data structures, and file-system primitives. We implemented and verified a crash-safe, concurrent mail server using Perennial and Goose that achieves speedup on multiple cores. Both Perennial and Iris use the Coq proof assistant, and the mail server and the framework's proofs are machine checked.

Perennial source code

All of Perennial is open source. The implementation is split into multiple GitHub repos:

• The framework and verified examples are at mit-pdos/perennial.
• The Goose translator, which imports Go into Coq for verification with Perennial, is at tchajed/goose. The documentation in that repo goes into more detail than the SOSP paper on exactly how the translation works.
• The mail server we verified, Mailboat, is at tchajed/mailboat.

Poster

Here is a digital copy of the poster.

Questions you might ask

Why is it called Perennial?

We extend Iris, and irises (the flowers) are perennials, but also because perennials recover in the spring.

Why is it called Goose?

Because it translates from Go to Coq, and Coq means "rooster" in french, and a goose is like a rooster.

This is cool, how do I work on it?

This work is all based on Iris, a sophisticated and extensible Coq framework for concurrency. Talk to Tej or Joe Tassarotti and we can point you to some resources.