Abstract Local Reasoning for Concurrent Libraries: Mind the Gap
File(s)Gardner_abstract local_MFPS.pdf (461.25 KB)
Published version
Author(s)
Gardner, P
Raad, A
Wheelhouse, M
Wright, A
Type
Conference Paper
Abstract
© 2014 The Authors.We study abstract local reasoning for concurrent libraries. There are two main approaches: provide a specification of a library by abstracting from concrete reasoning about an implementation; or provide a direct abstract library specification, justified by refining to an implementation. Both approaches have a significant gap in their reasoning, due to a mismatch between the abstract connectivity of the abstract data structures and the concrete connectivity of the concrete heap representations. We demonstrate this gap using structural separation logic (SSL) for specifying a concurrent tree library and concurrent abstract predicates (CAP) for reasoning about a concrete tree implementation. The gap between the abstract and concrete connectivity emerges as a mismatch between the SSL tree predicates and CAP heap predicates. This gap is closed by an interface function I which links the abstract and concrete connectivity. In the accompanying technical report, we generalise our SSL reasoning and results to arbitrary concurrent data libraries.
Date Issued
2014-06
Citation
2014
ISSN
1571-0661
Publisher
Elsevier B.V.
Journal / Book Title
Electronic Notes in Theoretical Computer Science
Volume
308
Copyright Statement
© 2014 The Authors. Published by Elsevier B.V. This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/3.0/).
License URL
Description
16.06.15 KB. Ok to add published verison, OA paper
Source
Mathematical Foundations of Programming Semantics Thirtieth Conference, MFPS 2014
Start Date
2014-06-12
Finish Date
2014-06-15
Coverage Spatial
Ithaca, New York, USA