Discussing "Checking Interference with Fractional Permissions"

(Link)

Author: John Boyland (University of Wisconsin-Milwaukee)

Reference: Boyland, J. (2003). Checking Interference with Fractional Permissions. In: Cousot, R. (eds) Static Analysis. SAS 2003. Lecture Notes in Computer Science, vol 2694. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44898-5_4

Why this paper? Cited by Mechanised Robust Safety for Virtual Machines Communicating above FF-A, and Fractional Resources in Unbounded Separation Logic, and Verification-Preserving Inlining in Automatic Separation Logic Verifiers (extended version)

Of late the citations in my Google Scholar recommendations have been very concerned with the question of whether two different parts of a program interfere with each other, or depend on each other – see here, here, and (less directly) here. This is an important question if we want to reason about the behaviour of a program – we would like to reason about a large program piece by piece, but can only do so if we are sure the pieces do not interfere with each other (or, if they do interfere, we have a precise sense of how this interference might manifest).

Separation logic à la Reynolds tells us that we can reason about parts of a program separately if they only access disjoint parts of memory. This is correct, but needlessly blunt. Two programs that read the same piece of memory do not effect each other; it is only if one of those program write to memory the other program is interested in that we have an issue. The solution proposed in this paper is to give different (parts of) programs different levels of permission to each part of the memory. Full permission, represented by the number 1, allows one to write and read, whereas a permission represented by a fraction strictly between 0 and 1 gives only read access. Where there is parallel composition or similar in the program, permissions can be divided between threads. Conversely, a program can add its permissions back together when it completes threads and hence, if full permission is reached, regain the ability to write.

The concepts of this paper and presented in the form of a type system, but it was soon realised by others that they can also be used to generalise separation logic as well; this is the context in which fractional permissions continue to appear in papers recommended to me.