# 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.

• Relaxed Prefix project, recording:
Partial solution, proves correctness for a positive result only, the invariant is proved only for some cases.
• Parallel GCD project, recording:
Proof of partial correctness, excluding termiantion. Concurrency is limited: evaluation of conditionals takes no step, the assignments are atomic.
• Dancing Links project, recording:
Complete solution using a separation logic abstraction.

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:

• `pat ⊑ x`, i.e., it is a proper prefix (where `⊑` is defined in the library.
• There is a split `pat = pat0 + a + pat1` such that `pat0 + pat1 ⊑ x`

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

• `M` remains the same: `M' = M`
• `N` can only decrease `N' ≤ N`
• No interference when its not N's turn: `N ≤ M → N' = N`

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

• The loop satisfies the invariant and propagates the rely/guarantee condition: gcd-loop-partial. Here, a formula `[: X | rely, guar, inv, proc(; X), post)` states that procedure `proc` runs in a `rely`-compatible environment, providing `guar` and maintaining the state-invariant `inv`. If `proc` terminates, then `post` holds (no termination guarantee). Variables `X` denote the state shared with other processes.
• The parallel system computes the GCD: gcd-partial. The proof relies on a decomposition theorem from the library, applied in the proof in step 9.

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;
}
}
}``````

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

• The hash functions `h1` and `h2` return positions in the arrays: `hi(x) < Ti.length`. Other than that, nothing should be assumed about the hash values. In particular it is unspecified whether `h1(x) = h2(x)`.
• For insertion it is sufficient to prove partial correctness, since it is impossible to prove termination without further assumptions.
• Alternatively, you can add an upper bound to the number of iterations and signal an error if insertion does not succeed. You should prove that an unsuccessful insertion is not observable (i.e., the contained elements are the same).

### 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):

• The tables have a constant and equal size.
• The hash functions return values below that size.
• All items are stored at the correct position as given by the corresponding has functions, i.e., `Ti[n] = x` implies `hi[x] = n`.
• The tables contain disjoint sets of values (this was not immediately obvious).