Software Specification: Dynamic Frames and Separation Logic

Software Specification, MEIC @ IST, 2019/20

João F. Ferreira

 jff
### At the end of this session, you should be able to: - Describe and implement the standard idiom for using dynamic frames in Dafny - Describe some challenges involved in verifying heap-manipulating programs - Describe the main concepts involved in separation logic
## A brief review of last session...

Classes in Dafny

class Cell {
    var data: int;

    constructor ()
        ensures data == 0
    { data := 0; this.data := 0; }

    method setValue(v: int)
        ensures data == v
        modifies this
    { data := v; }

    method Main() {
        var c1 := new Cell(); c1.setValue(5);
    }
}

Familiar, but...

The ability to write predicates and assertions is new and increases confidence in our code.

Class invariants

  • Class invariants are properties that must hold at the entry and exit point of every method, for every instance of a class
  • They often express properties about the consistency of the internal representation of an object
  • They are typically transparent to clients of an object
  • They are sometimes also called object invariants or instance invariants.

Example: An Odd Stack

Let us implement a stack that can only contain odd integers.

The Problem with Class Invariants

In the previous example, the invariant was defined directly on the internal representation.

However, in Dafny, it's very common to define class invariants in terms of so-called ghost variables.

Ghost variables are declared with the modifier ghost, and are used only at verification time; they are not compiled into variables that are allocated and updated when the program is run, so we do not need to worry about the impact on performance that manipulating these variables would otherwise have.

Example: A Simple Counter

Let us look at the simple counter in Counter.dfy, where the invariant also uses a ghost variable.

Framing

To reason modularly about a method invocation, one should not rely on the callee's implementation, but only on its specification. 

class Cell {
    int x;

    Cell()
        ensures this.x == 0
    { this.x := 0 }

    void setX(int v)
        ensures this.x == v
    { this.x := v; }
}


Cell c1 := new Cell();
c1.setX(5);

Cell c2 := new Cell();
c2.setX(10);

assert c1.x == 5;

Q: Is the assertion valid?

Framing

  • The given contracts are too weak to prove the assertion. The implementation of setX is allowed to change the state arbitrarily, as long as it ensures that this.x equals v on exit. In particular, the contract does not prevent c2.setX(10) from modifying c1.x
  • To prove the assertion, we must strengthen Cell's method contracts. The contracts should additionally specify an upper bound on the set of memory locations modifiable by the corresponding method. This problem is called the frame problem.

The Dynamic Frames Approach

  • Solution used in Dafny: Dynamic Frames
    • each object maintains a ghost field for its own representation frame
    • frames of different objects are kept separate by adding appropriate disjointness constraints
    • yields compositional verification approach
    • The idea behind Dynamic Frames is the introduction in the abstract vocabulary of the footprints of methods and functions.

Example

Let's revisit the binary trees example.

Autocontracts

  • AutoContracts is an experimental feature that will fill much of the dynamic-frames boilerplate into a class.
  • From the user’s perspective, what needs to be done is simply:
    • mark the class with {:autocontracts}
    • declare a function (or predicate) called Valid()
  • AutoContracts will then declare all the boilerplate code.

Autocontracts

  • Declares: ghost var Repr: set<object>
  • For function/predicate Valid(), inserts: reads this, Repr
  • Into body of Valid(), inserts (at the beginning of the body): this in Repr && null !in Repr
  • For every field F of a class type T where T has a field called Repr, also inserts:
    (F != null ==> F in Repr && F.Repr <= Repr && this !in Repr)
  • Except, if F is declared with {:autocontracts false}, then the implication will not be added.
  • For every constructor, add:
    modifies this
    ensures Valid() && fresh(Repr - {this})
  • Etc... (see Reference Manual for more details)

Frame Rule

The so-called frame rule $$\ione{Frame}{\ht{F \wedge P}{C}{F \wedge Q}}{\ht{P}{C}{Q}}$$ is known to fail in standard Hoare Logic. Example: $$\ione{Frame}{\ht{y=0 \wedge x=0}{x := 2}{y=0 \wedge x=2}}{\ht{x=0}{x:=2}{x=2}}$$ Not valid because $y$ could alias $x$ (i.e. point to the same memory cell)

Dynamic memory

  • Reasoning about programs that manipulate dynamic memory is challenging
  • There have been several formalisms proposed
  • A very successful proposal is separation logic, an extension of Hoare Logic

Separation Logic

  • Separation logic is an extension of Hoare logic, which employs novel logical operators, most importantly the separating conjunction $\ast$ (pronounced "and separately") when writing assertions.
  • It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang drawing upon early work by Rod Burstall.

Frame Rule

The so-called frame rule $$\ione{Frame}{\ht{F \ast P}{C}{F \ast Q}}{\ht{P}{C}{Q}}$$ is valid in Separation Logic, provided that C does not modify variables mentioned in the "frame" F. $$\ione{Frame}{\ht{y{\mapsto}0 \ast x{\mapsto}0}{[x] := 2}{y{\mapsto}0 \ast x{\mapsto}2}}{\ht{x{\mapsto}0}{[x] := 2}{x{\mapsto}2}}$$ Valid because $y$ cannot alias $x$ (i.e. they point to different memory cells)

Frame Rule

The frame rule is the key to the principle of local reasoning in separation logic: reasoning and specifications should concentrate on the resources that a program accesses (the footprint), without mentioning what doesn’t change.

Separation Logic

Learning material:

FreeRTOS: Scheduling Tasks

FreeRTOS: Scheduling Tasks

The verification system used was HIP/Sleek, which supports sets, bags, etc.

FreeRTOS: Scheduling Tasks

For small case studies such as FreeRTOS, it is possible to annotate the code with contracts. However, manual annotation is not scalable!

Scalable verification

  • One of the main obstacles blocking application of verification tools to programs in the millions of LOC is the need for the human to supply annotations.
  • Bi-abduction is a technique that can be used to infer pre- and postconditions
  • Bi-abduction: given A and B, find $\text{?frame}$ and $\text{?anti-frame}$ such that $$A \ast \text{?anti-frame} \vdash B * \text{?frame}$$ where $\vdash$ is read 'entails' or 'implies.'
  • See Peter O'Hearn's Lecture 4 for more details.

Monoidics founded in 2009 and acquired in 2013 by Facebook

FB Infer

In deployment at Facebook where it catches thousands of bugs per month before code reaches production in products used daily by over one billion people.

FB Infer

  • The compositional nature of Infer turned out to be a remarkable fit for Facebook's software development process: a codebase with millions of lines is altered thousands of times per day in "code diffs" submitted by the programmers.
  • Instead of doing a whole-program analysis for each diff, Infer analyzes changes (the diffs) compositionally, and reports regressions as a bot participating in the internal code review process.
  • Using bi-abduction, the frame rule picks off (an approximation of) just enough state to analyze a diff, instead of considering the entire global program state.

Separation Logic: Key Insights

  • Separation logic supports in-place updating of facts as we reason, in a way that mirrors in-place update of memory during execution, and this leads to logical proofs about imperative programs that match computational intuition
  • Separation logic supports scalable reasoning by using an inference rule (the frame rule) that allows a proof to be localized to the resources that a program component accesses (its footprint).
  • Concurrent separation logic shows that modular reasoning about threads that share storage and other resources is possible
### After this session, you should now be able to: - Describe and implement the standard idiom for using dynamic frames in Dafny - Describe some challenges involved in verifying heap-manipulating programs - Describe the main concepts involved in separation logic

Credits

  • These slides use the framework reveal.js and were produced using vim and Ubuntu.
  • Some slides and examples are based on material available online by Peter O'Hearn.