How would one specify a correct behaviour of an optimistic fine-grained concurrent data structure? For more than twenty five years Herlihy and Wing’s notion of linearizability served as a golden standard of such a correctness criteria for concurrent objects.

However, even though linearizability works well when checking whether all operations of an object can be seen as atomic ones, it does not answer the question what stable specifications should be given to these operations, so the clients could reason about them in the style of Hoare logic, in the presence of interference. Neither does it answer, which specifications can be thought of as canonical ones.

In my talk, I will present an ongoing work in progress, which makes a tentative attempt to provide canonical Hoare-style specifications to operations of a series of non-blocking data structures. The key idea of our approach is instantiation of the recently developed framework of Fine-Grained Concurrent Separation Logic with a novel sort of resources: subjective histories. By considering object histories as timestamp-indexed series of “atomic deltas”, we provide a simple and principled way to specify and prove granularity abstraction: sophisticated non-blocking algorithms are given the same specifications as their simplified coarse-grained counterparts, which makes the former ones as convenient as the later ones for the client-side reasoning.