Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Modular Reasoning about Separation for Concurrent Data Structures

Kasper Svendsen, Lars Birkedal, and Matthew Parkinson

Abstract

In a concurrent setting, the usage protocol of standard separation logic specifications are not refinable by clients, because standard specifications abstract all information about potential interleavings. This breaks modularity, as libraries cannot be verified in isolation, since the appropriate specification depends on how clients intend to use the library.

In this paper we propose a new logic and a new style of specification for thread-safe concurrent data structures. Our specifications allow clients to refine usage protocols and associate ownership of additional resources with instances of these data structures.

Details

Publication typeInproceedings
Published inProceedings of ESOP
> Publications > Modular Reasoning about Separation for Concurrent Data Structures