Model-based reasoning: concurrent counting

An example verification program with concurrent counting: two threads that concurrently decrement a shared counter. The verification uses model-based abstraction/reasoning.

General Information

Backend: Silicon
Language: PVL
Features: Futures, Statically-scoped locking, Statically-scoped parallelism
Path to Example File: futures/counteradd_2.pvl
Should Verify: Yes
Date: 2017-06-19
Lines of Code: 46 (comments not included)
Lines of Specification: 13 (28.3% of total)
Computation Time: 27.9 seconds

// -*- tab-width:2 ; indent-tabs-mode:nil -*-
//:: case ConcurrentCounting
//:: verdict Pass
//:: tool silicon
//:: option --check-history

class `Future` {
    int step;
	int counter;

// Models a single atomic "decrease" operation.
	accessible step;
	modifies counter;
	ensures counter == \old(counter) - step;
	process decr();

// Models a concurrent system with two "decrease" actions.
	accessible step;
	modifies counter;
	ensures counter == \old(counter) - 2 * step;
	process pardecr() = decr() || decr();
}

class Program {

ensures \result == count - 4;
	int decrease(int count) {

`Future` f = new `Future`();
		f.counter = count;
		f.step = 2;
		create f, f.pardecr();
		split f, 1\2, f.decr(), 1\2, f.decr();

invariant lockinv(HPerm(f.counter, write) ** HPerm(f.step, 1\2)) {
			par T0()
				requires Future(f, 1\2, f.decr());
				ensures Future(f, 1\2, empty);
			{
				atomic(lockinv) {
					action(f, 1\2, empty, f.decr()) { f.counter = f.counter - f.step; }
				}
			}
			and T1()
				requires Future(f, 1\2, f.decr());
				ensures Future(f, 1\2, empty);
			{
				atomic(lockinv) {
					action(f, 1\2, empty, f.decr()) { f.counter = f.counter - f.step; }
				}
			}
		}

merge f, 1\2, empty, 1\2, empty;
		destroy f;

return f.counter;
	}
}

Language: