IRUS Total

Abstract Local Reasoning for Concurrent Libraries: Mind the Gap

File Description SizeFormat 
Gardner_abstract local_MFPS.pdfPublished version461.25 kBAdobe PDFView/Open
Title: Abstract Local Reasoning for Concurrent Libraries: Mind the Gap
Authors: Gardner, P
Raad, A
Wheelhouse, M
Wright, A
Item 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.
Issue Date: 1-Jan-2014
URI: http://hdl.handle.net/10044/1/23831
DOI: http://dx.doi.org/10.1016/j.entcs.2014.10.009
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/).
Conference Name: Mathematical Foundations of Programming Semantics Thirtieth Conference, MFPS 2014
Start Date: 2014-06-12
Finish Date: 2014-06-15
Conference Place: Ithaca, New York, USA
Appears in Collections:Computing
Faculty of Engineering

This item is licensed under a Creative Commons License Creative Commons