Introduction to concurrency reasoning in the Iris framework, using a bank as an example program.
Iris is a powerful framework for doing concurrency reasoning. In the PDOS group we've been using it to verify concurrent storage systems, including reasoning about code implemented in Go. Iris stands out among concurrency frameworks in my mind for two reasons: it is extremely modular, allowing us to adapt it to a setting quite different from its original purposes; and it is extremely well-engineered, allowing us to work with it as a library rather than re-implement it. Iris stands out, especially among Coq frameworks, for how usable it is.
Iris is also, unfortunately, a beast to learn. It can be hard to tell where to start, hard to figure out what Iris even is, and hard to appreciate why Iris is such a good framework. In this post we'll work through a sort of "hello, world" example of concurrency verification, proving it correct in Iris. My goal is to convince you that the underlying ideas are approachable and get you excited about Iris; if I succeed then you'll walk away appreciating Iris a bit more and maybe be curious enough to dive deeper into other material.