Abstract
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.