Verifying crash-safe, concurrent code with sequential proofs. The goal is to connect goose-nfsd's verified journal with sequential verification in Dafny: the idea is that the journal should make reasoning sequential, in which case we can prove applications correct using only sequential reasoning in a productive proof system like Dafny while carrying out the complicated concurrency and crash-safety reasoning in Perennial.
Spec for journal interface, assuming 2PL
Run make verify to verify everything and make compile to compile
the file-system and bank examples to Go (the generated code goes into
dafnygen/).
You'll need Dafny 3:
- On Arch Linux you can get
dafny-binfrom the AUR - On macOS use
brew install dafny - For other systems the easiest solution is to download a binary release from https://github.com/dafny-lang/dafny/releases, extract it, and add it to your $PATH (this is what we have to do in CI, which runs on Ubuntu 20.04).
Compilation additionally depends on goimports to remove unused imports:
go get golang.org/x/tools/cmd/goimportsThen you can run some sanity tests over the bank and file-system examples.
These are ordinary Go tests that import the code generated from Dafny and
run it, linking with goose-nfsd,
specifically with its twophase package. To run these tests,
after compiling with make compile, run:
go test -v ./testsYou'll need some basic utilities: the rpcbind service to tell the server what
port to run on, and the NFS client utilities to mount the file system. On Arch
Linux these are available using pacman -S rpcbind nfs-utils and on Ubuntu you
can use apt-get install rpcbind nfs-common.
You might need to start the rpcbind service with systemctl start rpcbind. The
rpcinfo -p command is useful for verifying that an rpcbind service is
running on port 111.
Now run go run ./cmd/dafny-nfsd to start the server and sudo mount localhost:/ /mnt/x to mount it using the Linux NFS client.
On macOS you already have rpcbind and the NFS client utilities, but you'll
need to start a couple services with:
sudo launchctl start com.apple.rpcbind
sudo launchctl start com.apple.lockd
We provide a library at dafny_go that exports some external APIs that are
axiomatized using {:extern} modules, classes, and methods in Dafny. Some of
these are core primitives, like []byte and little-endian encoding, while the
big one is the jrnl package which interfaces between Dafny and
github.com/mit-pdos/goose-nfsd/txn.
The support library is trusted and hence its agreement with the Dafny spec is important.
You can run tests for this support library with go test:
go test ./dafny_go/...