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.

Discussing 'Nominal logic, a first order theory of names and binding'

(Link).

Author: Andrew M. Pitts (University of Cambridge)

Reference: Information and Computation vol. 186(2), pp. 165–193 (2003).

Why this paper? Cited by 5 (of a possible 29) of the papers in my Google Scholar Updates recommendations.

Comments: Two weeks ago I discussed "A New Approach...", the paper that introduced nominal techniques. In that discussion I specifically mentioned (the conference version of) this week's paper as the one that introduced nominal as the term of the art for these techniques. So this is very much a sequel paper, and as such this is very much a sequel discussion - please do read my earlier discussion before this one.

As I discussed, the innovation of "A New Approach" was the mathematical shift to a non-standard set theory. Such a move is beautiful and clever, but does run the risk of being profoundly alienating to working computer scientists who simply want to solve problems involving names and binding! This paper, without abandoning the central insights gleaned from the Fraenkel-Mostowski setting, shows how much can be accomplished without straying beyond first-order logic, a completely standard logical setting that no one could object to. Along with this, Pitts makes a notion called nominal sets the semantical heart of his developments. Nominal sets appear in "A New Approach" as a preliminary construction on the road to the set-theoretic semantics, but they are far simpler than the full non-standard set theory. Although they are less expressive, this paper makes the case that they are expressive enough for most applications, a view which has been vindicated by the hundreds of papers that have since used the nominal sets framework.

While both logic and semantics have proved very useful, there is an acknowledged mismatch in this paper between them, via an incompleteness result - first-order logic is not really powerful enough to fully describe the properties of nominal sets, even 'cut down' as they are from the full set theory. For the notion of the 'set of free names' of a term (in nominal sets jargon, the support of an element) to be specified we would need the more powerful second-order logic. However the assertion that a name is not in the set of free names of (in the jargon, is fresh for) a term can be expressed in first-order logic, and turns out to be all that is needed for most applications. James Cheney resolved this mismatch in a 2006 paper, which provided a semantics that was complete for this paper's nominal logic, although I'm not aware of any applications of this very interesting theoretical work. After all incompleteness is often unavoidable, so is not necessarily a barrier to getting some work done!