Abstract Local Reasoning for Concurrent Libraries: Mind the Gap
Venue
Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics (MFPS’14), vol. 308, pp. 147–166
Publication Year
2014
Identifiers
Authors
- Philippa Gardner
- Azalea Raad
- Mark J. Wheelhouse
- Adam Wright
Abstract
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.