Verifying Concurrent Go Code in Coq with Goose
summary
A pipeline imports a practical subset of Go into Coq: a 2.5k‑line Go translator produces GooseLang programs that plug into Iris’s weakest‑precondition framework, so concurrent Go (mutexes modeled as spin‑lock locks, goroutines → fork in heapLang) is verifiable. A 150‑line concurrent mail server is fully verified; a 3,000‑line filesystem is implemented but proofs are pending. Weak‑memory racy loads/stores become undefined via split begin/commit semantics; an executable single‑threaded interpreter is used for behavioral testing. Code is open source.
AI-written summary · about
chapters (23)
- 0:00Systems verification, broadly
- 0:26Systems verification requires connecting implementation to proof
- 0:51We aim to verify realistic systems
- 1:47Goal: implement in a systems language
- 2:04Goose: write code in Go and prove with Iris
- 2:52Implementing in Go helps build the software
- 3:21Goose: import subset of Go into a Coq model
- 5:11Our systems verification research using Goose
- 5:42Go is a systems language
- 6:36Goose code
- 7:13Challenges in implementing Goose
- 7:30GooseLang, a semantic model of Go
- 10:07modeling concurrency and locking
- 11:37Challenge in modeling Go: weak memory
- 12:57Disallow racy loads and stores
- 13:31Compatibility with Iris gives us amazing verification technology
- 14:04Proofs using non-atomic memory
- 15:06GooseLang programs can make system calls
- 16:29Semantics of GooseLang
- 18:45Goose translator supports enough Go
- 19:24Making the goose translator sound
- 20:25Related work
- 22:43Conclusion
related talks
29mUsing Formal Reasoning to Build Concurrent Go Systems
26mGo is Boring... And That's Fantastic!
48mUnderstanding concurrency with behavioural types
39mIs Go A Good Language to Build Compilers?
10mGo I made all the mistakes
47mGo and Ruby
40mDebugging concurrency programs in Go
44mConcurrency in Go: from hardware to code ☠️