Verifying a concurrent data-structure from the Dartino Framework in Iris

Abstract We specify and verify a concurrent queue data structure used in the scheduler of a real-world virtual machine, Google’s Dartino Framework. Our speci cation treats the queue operations as abstractly atomic. This means that a client can reason about them as if they take e ect at a single instant in time, and thus impose its own invariants on the queue. The speci cations also involve resource transfer: to enqueue a process, a thread transfers ownership of its descriptor to the queue. We show that an implementation of the data structure, directly translated from the Dartino Framework source, satis es our speci cation in Iris, a state-of-the-art higher-order concurrent separation logic, capable of expressing both abstract atomicity and resource transfer. Our veri cation is formalised in the Coq proof assistant. Hence, our work shows that Iris is both expressive and practical enough to formally reason about production code taken from “the wild”.