A Restricted Definition of the Magic Wand to Soundly Combine Fractions of a Wand

Thibault Dardinier 🌐

May 30, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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. The concept has been generalized to fractional assertions. $A^p$ (where $A$ is a separation logic assertion and $p$ a fraction between $0$ and $1$) represents a fraction $p$ of $A$. $A^p$ holds in a state $\sigma$ iff there exists a state $\sigma_A$ in which $A$ holds and $\sigma$ is obtained from $\sigma_A$ by multiplying all permission amounts held by $p$. While $A^{p + q}$ can always be split into $A^p * A^q$, recombining $A^p * A^q$ into $A^{p+q}$ is not always sound. We say that $A$ is combinable iff the entailment $A^p * A^q \models A^{p+q}$ holds for any two positive fractions $p$ and $q$ such that $p + q \le 1$. Combinable assertions are particularly useful to reason about concurrent programs, for instance, to combine the postconditions of parallel branches when they terminate. Unfortunately, the magic wand assertion $A \mathbin{-\!\!*} B$, commonly used to specify properties of partial data structures, is typically not combinable. In this entry, we formalize a novel, restricted definition of the magic wand, described in a paper at CAV 22, which we call the combinable wand. We prove some key properties of the combinable wand; in particular, a combinable wand is combinable if its right-hand side is combinable.
BSD License

Topics

Theories of Combinable_Wands

Depends On