In this talk, we will present an ongoing effort towards employing a concurrent Separation-style logic (FCSL) for reasoning about fine-grained concurrent data-structures, whose verification traditionally requires a dedicated meta-theory of speculations or, equivalently, prophecy variables. We introduce re-sortable histories as a novel abstraction that can be implemented in FCSL off-the-shelf, without changes to the underlying logical framework, and makes it possible to capture the notion of speculative linearization points in a mechanized concurrency verification framework.

We will illustrate our approach by presenting the first formal specification and proof of Jayanti’s wait-free concurrent snapshot construction. Furthermore, we will comment on a few interesting details about its mechanization in the Coq proof assistant and discuss pitfalls and the challenges ahead.