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. © 2013 Springer-Verlag.
CITATION STYLE
Svendsen, K., Birkedal, L., & Parkinson, M. (2013). Modular reasoning about separation of concurrent data structures. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7792 LNCS, pp. 169–188). https://doi.org/10.1007/978-3-642-37036-6_11
Mendeley helps you to discover research relevant for your work.