Specifying and verifying concurrent algorithms with histories and subjectivity

DOI10.1007/978-3-662-46669-8_14zbMATH Open1335.68067arXiv1410.0306OpenAlexW1533529458MaRDI QIDQ2802440FDOQ2802440

Authors: Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee 

Publication date: 26 April 2016

Published in: Programming Languages and Systems (Search for Journal in Brave)

Abstract: We present a lightweight approach to Hoare-style specifications for fine-grained concurrency, based on a notion of time-stamped histories that abstractly capture atomic changes in the program state. Our key observation is that histories form a partial commutative monoid, a structure fundamental for representation of concurrent resources. This insight provides us with a unifying mechanism that allows us to treat histories just like heaps in separation logic. For example, both are subject to the same assertion logic and inference rules (e.g., the frame rule). Moreover, the notion of ownership transfer, which usually applies to heaps, has an equivalent in histories. It can be used to formally represent helping---an important design pattern for concurrent algorithms whereby one thread can execute code on behalf of another. Specifications in terms of histories naturally abstract granularity, in the sense that sophisticated fine-grained algorithms can be given the same specifications as their simplified coarse-grained counterparts, making them equally convenient for client-side reasoning. We illustrate our approach on a number of examples and validate all of them in Coq.

Full work available at URL: https://arxiv.org/abs/1410.0306

Recommendations

• Expressive modular fine-grained concurrency specification
• Subjective auxiliary state for coarse-grained concurrency
• Communicating state transition systems for fine-grained concurrent resources
• Reasoning about optimistic concurrency using a program logic for history
• Fine-grained concurrency with separation logic

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cited In (10)

• Higher-order linearisability
• Connecting higher-order separation logic to a first-order outside world
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• A perspective on specifying and verifying concurrent modules
• Abstract specifications for concurrent maps
• Order out of chaos: proving linearizability using local views
• Reasoning about optimistic concurrency using a program logic for history
• Subjective auxiliary state for coarse-grained concurrency
• Higher-order linearisability
• Expressive modular fine-grained concurrency specification

Uses Software

• Coq

This page was built for publication: Specifying and verifying concurrent algorithms with histories and subjectivity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2802440)