2014/10/01 by Ilya Sergey, Sergey, Ilya, Aleksandar Nanevski +3 · 1 voice
Computer Science · #Logic, programming, and type systems #Formal Methods in Verification #Parallel Computing and Optimization Techniques
paper · pdf · doi:10.48550/arxiv.1410.0306
We present a lightweight approach to Hoare-style specifications for\nfine-grained concurrency, based on a notion of time-stamped histories that\nabstractly capture atomic changes in the program state. Our key observation is\nthat histories form a partial commutative monoid, a structure fundamental for\nrepresentation of concurrent resources. This insight provides us with a\nunifying mechanism that allows us to treat histories just like heaps in\nseparation logic. For example, both are subject to the same assertion logic and\ninference rules (e.g., the frame rule). Moreover, the notion of ownership\ntransfer, which usually applies to heaps, has an equivalent in histories. It\ncan be used to formally represent helping---an important design pattern for\nconcurrent algorithms whereby one thread can execute code on behalf of another.\nSpecifications in terms of histories naturally abstract granularity, in the\nsense that sophisticated fine-grained algorithms can be given the same\nspecifications as their simplified coarse-grained counterparts, making them\nequally convenient for client-side reasoning. We illustrate our approach on a\nnumber of examples and validate all of them in Coq.\n