Reasoning over Permissions Regions in Concurrent Separation Logic

We propose an extension of separation logic with fractional permissions, aimed at reasoning about concurrent programs that share arbitrary regions or data structures in memory. In existing formalisms, such reasoning typically either fails or is subject to stringent side conditions on formulas (notably precision) that significantly impair automation. We suggest two formal syntactic additions that collectively remove the need for such side conditions: first, the use of both “weak” and “strong” forms of separating conjunction, and second, the use of nominal labels from hybrid logic. We contend that our suggested alterations bring formal reasoning with fractional permissions in separation logic considerably closer to common pen-and-paper intuition, while imposing only a modest bureaucratic overhead.