Matthew Parkinson verifies Java. Very brief and inaccurate version.

Here are some slides. (His last slide in the first set is ``do David's exercises.'' Obviously, you'll need to know what those were in order to solve them. David's exercises were ``do John's exercises.'' Happy solving!). Here's a summary of the lectures:

• Q: How to model abstraction? A: Use uninterpreted functions.
• Q: How to use separation logic to verify Java programs? A: Use intuitionistic separation logic because it plays well with garbage collection.
• Q: How to deal with inheritance? A: Attach to each method a static spec and a dynamic spec.
• Q: How to reason about concurrency? A: Use a mix of separation logic and rely/guarantee reasoning; we'll call it deny/guarantee.

Do you want more? OK, here's one example. The Visitor pattern is used often by people who write compilers. When you write a.f(b, c) you call function f with three parameters. The first one, a is special in two ways: (1) it will be known by the special name this in the body in of the function and its dynamic type is used to decide which of the functions named f will be called; in general, more than one function f may be called by the same statement depending on the value of a. The Visitor pattern is a work-around not having multiple dynamic dispatch aka multimethods. Or, depending where you come from, you might see it as a work-around not having pattern matching. The main tool used by this pattern is (single) dynamic dispatch, so it will also illustrate how to annotate programs that use this feature of Java.

interface Ast { Ast accept(Visitor v); }
class Constant implements Ast {
  int value;
  @Override Ast accept(Visitor v) { return v.visit(this); }
}
class Plus implements Ast {
  Ast left, right;
  @Override Ast accept(Visitor v) { return v.visit(this); }
}

interface Visitor {
  Ast visit(Constant n);
  Ast visit(Plus n);
}

Given this boilerplate we can do something `useful' to the AST.

class ZeroRemover implements Visitor {
  @Override Ast visit(Constant n) { return n.value == 0? null : n; }
  @Override Ast visit(Plus n) {
    n.left = n.left.accept(this);
    n.right = n.right.accept(this);
    if (n.left != null && n.right != null) return n;
    return n.left != null? n.left : n.right;
  }
}

If you are unfamiliar with the Visitor pattern you can spend a few minutes starring at the code above. Or you could continue reading and notice how sprinkling annotations actually helps to understand the code. So, how do we annotate the accept method? If the visitor and the AST node are OK (for some definition of OK depending on the visitor and on the node, respectively), then some value will be returned (for some definition of some, depending on the particular visitor. OK, so we'll just say what we just said.

interface Ast {
  Ast accept(Visitor v)
    requires this.OK(t) ** v.OK(o)
    ensures v.Result(result, this, t, o);
}

``Whooooaa, stop! What's the funny **, and what are t and o? You said you'll write exactly what you said!'' Uhm, the stars are just the separating conjunction; we use two because one is taken by multiplication. The t and o is just stuff, uninterpreted for now if you want. We're just saying that the Result may depend on the state of the node and on the state of the visitor. Feel better? Yes? OK, then let's move on, it's late. I'll skip some specs so we can move quickly to the next interesting bit. How do we say what ZeroRemover is supposed to do? We just provide a definition for the Result predicate, which was uninterpreted (or `abstract') until now.

class ZeroRemover implements Visitor {
  spec
    Result(r, a, t, o) = r == rz(t);
    plus(Constant(0), x) = x;
    plus(x, Constant(0)) = x;
    plus(x, y) = Plus(x, y);
    rz(Plus(x, y)) = plus(rz(x), rz(y));
    rz(x) = x;

  @Override Ast visit(Constant n) { return n.value == 0? null : n; }
  @Override Ast visit(Plus n) {
    n.left = n.left.accept(this);
    n.right = n.right.accept(this);
    if (n.left != null && n.right != null) return n;
    return n.left != null? n.left : n.right;
  }
}

Let's recap: In the specs you write a Haskell program that does the same thing but is shorter and (perhaps) slower and also some bridges between Haskell (aka math) and your program. As a result you can run a tool to tell you if your efficient(?) Java program does the same thing as the Haskell one.

Now, can you fill in the specs that I skipped? If not, then please do ask in the comments what information you feel you are missing.

Separation logic

A good way to learn separation logic is to read Reynold’s introductory lecture notes. This is a little bit like saying that a good way to learn programming is to read Knuth’s books. If you are the type of person that likes using iPhones and searching with Google you might need a bit more to wet your appetite.

Separation logic was designed to allow local reasoning. ‘Local’ is a generalization of ‘modular’. You can say ‘local’ when you have some sort of distance and you can say “a is close to b but far from c.” We reason locally when all the stuff that we need to keep in our head at one time is ‘close’. ‘Modular’ is simply ‘local’ specialized with program text distance. The typical distance people have in mind when they talk separation logic is “the number of pointer indirections I need to do to get from location x to location y.” When you think about a linked list you tend to ignore other linked lists that are at distance ∞. Good, so the central concept of separation logic is locality; or separation, depending on how you look at it.

A logic is a very simple language with very precise semantics. To describe the logic (that is, the one most people know) you need to introduce operators and describe what they mean (for example, p ∧ q evaluates to ⊤ when both p and q evaluate to ⊤); in other words, you introduce a piece of syntax and then you give its semantics. Thinking in terms of semantics is not always efficient. Sometimes you need to get in the symbol crunching mood. That’s why you’d typically present rules for manipulating symbols that are sound (for example, p ∧ (q ∨ r) can be replaced by (p ∧ q) ∨ (p ∧ r)).

There are three pieces of syntax that are new in separation logic: the separating conjunction p ⋆ q, the points-to operator x → v, the separating implication aka the magic wand p −⋆ q, and emp. The semantics are described in terms of a somewhat more complicated model. Now we have not only booleans plus some abstract domain. Still, the model will be familiar to any programmer. We have addresses, values, a stack (inappropriately named ‘store’ by the old-timer Reynolds), and a heap. (BTW, there’s nothing wrong with ‘store’ per se. It’s just that most programmers prefer the ambiguous terms ‘stack’ and ‘heap’.) So,

• p ⋆ q holds in a heap that can be split in a part where p holds and a part where q holds,
• x → v holds in a heap that has exactly one cell whose address is x and whose content is v,
• p −⋆ q holds in a heap that can be extended with a heap where p holds to get a heap where q holds,
• emp holds when the heap is empty.

Once we introduce these new operators we also get new laws, such as:

• p₁ ⇒ p₂ and q₁ ⇒ q₂ can be replaced by p₁ ⋆ q₁ ⇒ p₂ ⋆ q₂
• p₁ ⋆ p₂ ⇒ p₃ can be replaced by p₁ ⇒ (p₂ −⋆ p₃)

In fact there are classes of assertions for which extra rules can be used.

• pure assertions are those that don’t say anything about the heap so they can be pulled out of the new operators; for example (p ∧ q) ⋆ r can be replaced by p ∧ (q ⋆ r) if p is pure,
• strictly exact assertions are those that uniquely identify the heap,
• precise assertions are those that identify a unique subheap
• intuitionistic assertions are those that hold for any extended heap
• supported assertions are those for which there is a least subheap on which they hold

Now we can annotate programs with descriptions of the state at various intermediate points. If we also have rules on how the state is changed by simple commands we can then derive formal proofs of programs, meaning that the annotations can be shown to agree with the program by pure ‘symbol crunching’, something even a computer should be able to do. People who write such programs have a knack for funny names: Space Invader and Smallfoot. Well, perhaps not all people who write such tools. There is also the Unnamed and Unreleased tool from Matthew Parkinson that handles Java code. Edit: Matthew pointed out that the tool has a name: jStar. (Please write a comment if another tool should be mentioned here.)

The interesting algorithms proved correct (in the sense explained above) using separation logic are Schorr–Waite and Michael’s stack. (Please write a comment if another algorithm should be mentioned here.)

Let me briefly present these two algorithms.

The Schorr –Waite algorithm is used to reduce memory usage during garbage collection. For our purposes ‘garbage collection’ simply means that we want to mark all reachable nodes from a given root. The simple solution is to do a DFS. A simple implementation would use a stack of pointers that may grow in the worst case to be linear in the number of nodes in the graph. The trick Schorr and Waite use is to use the link fields in the graph to store the backpointers.

Michael’s stack is lock-free and works in the presence of memory reclamation. You want to implement push(stack, node) and pop(stack), where stack is a pointer identifying the stack. These functions will be used from multiple threads and the only synchronization primitive you are allowed to use is the compare-and-swap statement. To push a node you would probably try to read stack->next, set node->next := stack->next, if stack->next == what I read then set stack->next := node. The last operation is the compare-and-swap: “If the first element of the stack is still what it was when we looked the first time then make node the new first element.” The problem with this is that “the same first element” doesn’t necessarily mean “the next pointer of the first element is the same.” No one is supposed to change the next pointer apart from push and pop, but it may very well be that the node is freed, a ‘new’ allocated node happens to be the same area in memory and then there is nothing holding back the change of the next field. That is, unless you use an array of stuff that shouldn’t be touched, as in the solution given by Michael.

That’s it for now. Oh, and sorry if you were under the impression that I’m trying to ‘wet your appetite’. I was merely trying to draw a child’s sketch of separation logic.

FIRST Fall School

At the end of last month I attended (as a student) the FIRST fall school on the logics and semantics of state. John Reynolds told us about separation logic. David Nauman and Matthew Parkinson showed us various approaches to verifying object-oriented programs. Zhong Shao outlined a project whose vision is to verify a simple operating system. Finally, Lars Birkedal and Hongseok Yang talked about some really abstract math.

Reynold's lectures were thorough and clear. Parkinson's were fun and accessible. My lack of knowledge made it difficult for me to follow closely the other lectures so I hesitate to attach adjectives to them. But I do recommend you miss no opportunity of having Reynolds or Parkinson as a speaker in your university (or company).

I'll follow up with a few posts to outline what I learned.