Ownership-Based Owicki-Gries Reasoning

Ownership-Based Owicki-Gries Reasoning

---

연구 분야: Verification

---

---

학회: SAC '23: Proceedings of the 38th ACM/SIGAPP Symposium on Applied Computing

---

초록

This paper explores the use of ownership as a key auxiliary variable within Owicki-Gries framework. We explore this idea in the context of a ring buffer, developed by Amazon, which is a partial library that only provides methods for reserving (acquiring) and releasing addresses within the buffer. A client is required to implement additional functionality (including an additional shared queue) to enable full synchronisation between a writer and a reader. We verify correctness of the Amazon ring buffer (ARB) and show that the ARB satisfies both safety and progress. Our proofs are fully mechanised within the Isabelle/HOL proof assistant.

---