Email Gateway (Sep 14 2022 at 08:34): Email Gateway (Sep 14 2022 at 08:34):From: Tobias Nipkow <nipkow@in.tum.de>
Unbounded Separation Logic
Thibault Dardinier
Many separation logics support fractional permissions to distinguish between
read and write access to a heap location, for instance, to allow concurrent
reads while enforcing exclusive writes. Fractional permissions extend to
composite assertions such as (co)inductive predicates and magic wands by
allowing those to be multiplied by a fraction. Typical separation logic proofs
require that this multiplication has three key properties: it needs to
distribute over assertions, it should permit fractions to be factored out from
assertions, and two fractions of the same assertion should be combinable into
one larger fraction. Existing formal semantics incorporating fractional
assertions into a separation logic define multiplication semantically (via
models), resulting in a semantics in which distributivity and combinability do
not hold for key resource assertions such as magic wands, and fractions cannot
be factored out from a separating conjunction. By contrast, existing automatic
separation logic verifiers define multiplication syntactically, resulting in a
different semantics for which it is unknown whether distributivity and
combinability hold for all assertions. In this entry (which accompanies an
OOPSLA'22 paper), we present and formalize an unbounded version of separation
logic, a novel semantics for separation logic assertions that allows states to
hold more than a full permission to a heap location during the evaluation of an
assertion. By reimposing upper bounds on the permissions held per location at
statement boundaries, we retain key properties of separation logic, in
particular, we prove that the frame rule still holds. We also prove that our
assertion semantics unifies semantic and syntactic multiplication and thereby
reconciles the discrepancy between separation logic theory and tools and enjoys
distributivity, factorisability, and combinability.
https://www.isa-afp.org/entries/Separation_Logic_Unbounded.html
Enjoy!
smime.p7s
Last updated: Apr 20 2024 at 08:16 UTC