VerifyThis Competition 2015: KIV Solutions

This page documents the KIV solutions of the VerifyThis Competition held at ETAPS 2015 in London.

The version of KIV used can be downloaded at the Eclipse update site https://swt.informatik.uni-augsburg.de/kiv/v6/verifythis2015/site.

On-Site Solutions

The solutions submitted during the competition are archived below. The submissions were recognized with the best student team award. The screen recordings are completely unedited.

Contact: Gidon Ernst & Jörg Pfähler, {ernst,pfaehler} (at) isse.de

Challenge 1: Relaxed Prefix

Project overview relaxed-prefix, the property that was to be shown is this one. The partial proof from the competition has been completed afterwards, extending the invariant slightly and adding three additional helper-lemmas.

All definitions can be found in this specification.

The program has been modified slightly to accommodate for KIV's lack of return statement, namely by a variable break. Note that we do not increase the index i then, which unifies some cases of the loop invariant.

The relaxed prefix property is given by the predicate relaxed-prefix? by two cases. Sequence pat is a relaxed prefix of x iff one of the following holds:

The invariant (predicate inv) states that we have checked the relaxed prefix property up to the current index i. If the shift is 0, then the first i elements of pat, written as firstn(i, pat) must be a proper prefix of x. Otherwise, there is the corresponding split and we know that the intermediate element a mismatches the list x at that position. If the loop is aborted with break = true we track the second mismatch as well.

The proof is unfortunately not so straight forward. The following equivalences are exploited (omitting any size constraints here):

firstn(n + 1, x) = firstn(n, x) + x[n]
x + a ⊑ y  ↔  x ⊑ y ∧ y[# x] = a

The (technically) complicated part is showing that returning false can be justified: we have found two mismatches (rightmost part of the proof). The reason is that the invariant gives one arbitrary split, whereas the negated relaxed-prefix? gives another one. These have to be matched up properly.

Challenge 2: Parallel GCD

Project overview parallel-gcd-rg, developed after the competition. Compositional verification of partial correctness using rely guarantee reasoning.

The implementation runs procedure GCD_loop interleaved to itself symmetrically. Access is at the level of reads/writes, modeled by two local variables X and Y. Each assignment and test of conditional is a separate step. Note that the Done flag could be avoided with a do { ... } while loop (which is not supported by KIV).

GCD_loop(; N, M) {
  let Done = false, X = 0, Y = 0
  in while ¬ Done do {
    X := N;
    Y := M;
    if X = Y
    then Done := True
    else if X < Y
    then M := Y - X
  }
}

The process modifying N provides the following guarantee that is in turn the rely for the process modifying M. Such a step from N, M to N', M' satisfies

These properties are encoded in a predicate rely.

The invariant of the loop is simply that for initial values n,m of N,M the GCD is still the same, i.e.

gcd(n,m) = gcd(N,M)

Two theorems are proved

See also: G. Schellhorn, B. Tofan, G. Ernst, J. Pfähler, and W. Reif:
RGITL: A Temporal Logic Framework for Compositional Reasoning about Interleaved Programs

Project overview dancing-links, the property that was to be shown is this one. This is the exact solution from the competition.

Abstraction

Specification cell defines heap cells with pointers left and right; and data val of generic type elem. Specifications reflist cell-heap instantiate lists with references resp. heaps with this cell type defined above (i.e., just some boiler-plate).

Specification dllist defines the separation logic abstraction recursively given a list of values (third parameter), and proves some lemmas, notably to unfold the abstraction for the last or some intermediate list cell.

The abstraction is a heap-predicate

dls(head, prev, x, rx, next, tail)

where head/tail are a pointer to the first/last cell. Prev/next are the left/right pointer of the first/last cell (this can be used to express cyclic lists for example). The list x collects all the values (could be computed from rx) and the list rx collects the references to the cells between and including head and tail.

Slightly simplifying, there is one case for empty lists:

dls(head, prev, [], [], next, tail)
  = emp  ∧  head = next  ∧  tail = prev

where emp denotes an empty remaining heap part. In KIV, lifting of pure formulas p of type bool to heap assertions heap → bool is written ⌜p⌝. The recursive case unfolds one heap cell at head:

dls(head, prev, a+x, r0+rx, next, tail)
  =    r0 = head
    ∧  ∃ r.   head ↦ mkcell(prev, r, a)
            * dls(r, head, x, rx, next, tail)

In KIV, the points-to assertion ↦ is written => and the existential quantifier is written as a higher-order operator _∃ taking a λ-abstraction as parameter. Note that the actual definition destructs rx with selectors .first and .rest instead of pattern matching so that dls is specified for all cases.

Implementation

The operations remove and its converse insert ("unremove") are defined here. Since the formatting of the web-export is not so nice, we repeat the definitions here. Parameter H is the heap (after the semicolon) that is explicit in our programs. It is passed by reference, so that assignments to the variable H in the program are propagated to the caller. Note that H[r].left := ... is just an abbreviation for the assignment H := H[r, ...] where H[r, ce] denotes (algebraic) modification of the heap (you can see this in the web-export linked above).

remove(r; H) {
    let prev = H[r].left,
        next = H[r].right
    in {
        H[next].left := prev;
        H[prev].right := next;
    }
};

insert(r; H) {
    let prev = H[r].left,
        next = H[r].right
    in {
        H[next].left := r;
        H[prev].right := r;
    }
};

Verification

The two main proofs are a contract for remove and one for insert.

Removing r from a doubly linked list has as part of its precondition

dls(head, prev, x0+a+x1, rx0+r+rx1, next, tail)

i.e., there is a split such that r is in the list of references; x0 and rx0 must have same length, the prefix/postfix of the split x0 resp. x1 is assumed to be nonempty. The postcondition pulls r out of the list:

  r ↦ mkcell(rx0.last, rx1.first, a)
* dls(head, prev, x0+x1, rx0+rx1, next, tail)

In KIV, there is an additional part of the heap P: heap → bool (a higher-order variable), providing explicit framing. Whenever this lemma is used in some context, P can be instantiated to whatever (disjoint) heap assertion needs to be preserved over the call (the frame rule of separation logic is not generally valid in KIV, because the heap H is explicit and the program can do non-local actions).

We proved that reinsertion works in the main correctness theorem.

To facilitate this, we have reformulated the two contracts as follows: remove, insert.

Finally, we proved that removing two elements and reinserting these works as well.

Challenge Proposal: Cuckoo Hashing

We'd also like to share our submission during the collection of challenge proposals, namely a simple, partial implementation of Cuckoo Hashing.

Description

Cuckoo hash tables are a variant of hash tables that allow constant-time lookups. The basic idea is to have two tables, T1 and T2 and two corresponding hash functions h1 and h2. Here we consider an implementation of sets using arrays to represent the two tables.

An item x is in the data structure iff T1[h1(x)] = x ∨ T2[h2(x)] = x, i.e., x is found in table T1 or T2 using the respective hash function.

Insertion of an element x first checks if the element is already present. If not, x is inserted into T1 at position h1(x). If this slot is already occupied, i.e., T1[h1(x)] = y, this element y is moved to table T2 using the same strategy.

Elements are moved between T1 and T2 until an empty slot is found. To prevent looping forever, after a bounded number of tries the tables are resized, rehashed and insertion is restarted with the current pending element. Resizing of the table shall not be part of the challenge.

The following code is a straight forward translation from R. Pagh and F.F. Rodler: Cuckoo Hashing, J. Algorithms, 51(2):122-144, 2004. It has not been tested or compiled.

class CuckooHashSet<Elem> {
    Elem[] T1,T2;
    int size;

    CuckooHashSet(int size) {
        T1 = new Elem[size];
        T2 = new Elem[size];
        this.size = size;
    }

    int h1(x: Elem);
    int h2(x: Elem);

    boolean lookup(x: Elem) {
        return T1[h1(x)] == x || T2[h2(x)] == x;
    }

    void insert(x: Elem) {
        if(lookup(x))
            return;

        while(true) {
            Elem y;

            if(T1[h1(x)] == null) { T1[h1(x)] = x; return; }

            y = T1[h1(x)];
            T1[h1(x)] = x;
            x = y;

            if(T2[h2(x)] == null) { T2[h2(x)] = x; return; }

            y = T2[h2(x)];
            T2[h2(x)] = x;
            x = y;
        }
    }
}

Tasks

Specify and verify the partial correctness operations lookup and insert wrt. the semantics of sets. You can make the following assumptions

Variants

A recursive version is shorter and easier to verify. It passes the hash functions as parameters (in order to swap them), and assumes that the element is not already in the data structure.

void insert_rec(Elem x, Elem[] T1, Elem[] T2,
                Function<Elem,int> h1, Function<Elem, int> h2)
{
  Elem y = T1[h1(x)];
  T1[h1(x)] = x;
  if(y != null)
    insert_rec(y, T2, T1, h2, h1);
}

Solution

Project overview cuckoo. The implementation is here, the invariants and abstraction function are here Correctness proofs: lookup, insert, recursive insert. Since there is no built-in null in KIV, we define a variant slot for array elements, that can either be empty or full with a given entry.

Invariants of the hash table (we prove that they are preserved by insert):

[Imprint] [Data Privacy Statement] [E-Mail]