Model-based reasoning: generalised concurrent counting

Verification example with `n` threads, each decrementing a shared variable. This verification problem shows that our model-based abstraction approach can be applied to applications that spawn a dynamic number of threads.

General Information

Backend: Silicon
Language: PVL
Features: Fork/join concurrency, Futures, Statically-scoped locking
Path to Example File: futures/counteradd_n.pvl
Should Verify: Yes
Date: 2017-06-19
Lines of Code: 91 (comments not included)
Lines of Specification: 26 (28.6% of total)
Computation Time: 27.9 seconds

// -*- tab-width:2 ; indent-tabs-mode:nil -*-
//:: case GeneralisedConcurrentCounting
//:: suite puptol
//:: tool silicon
//:: option --check-history

class `Future` {
	int counter;

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

// Models a concurrent system with `n` "decrease" actions.
	requires 0 <= n;
	ensures counter == \old(counter) - n;
	process pardecr(int n) = 0 < n ? (decr() || pardecr(n - 1)) : empty;
}

class Worker {
	/* ghost */ frac p;
	Program prog;

requires Value(pr.f) ** fr != none;
	ensures Value(prog) ** Value(prog.f) ** Value(p) ** p != none;
	ensures prog == pr ** p == fr;
	Worker(Program pr, frac fr) {
		this.prog = pr;
		this.p = fr;
	}

// Performs the atomic "decrease" action.
	context Value(p) ** Value(prog) ** Value(prog.f) ** p != none;
	requires Future(prog.f, p, prog.f.decr());
	ensures Future(prog.f, p, empty);
	void run() {
		lock prog;
		action(prog.f, p, empty, prog.f.decr()) {
			prog.f.counter = prog.f.counter - 1;
		}
		unlock prog;
	}
}

class Program {
	/* ghost */ int count;
	/* ghost */ int threads;
	`Future` f;

resource lock_invariant() = Value(f) ** HPerm(f.counter, 1);

requires threads > 0;
	ensures Value(f) ** Future(f, 1, f.pardecr(threads));
	ensures Value(this.count) ** Value(this.threads) ** AbstractState(f, counter == this.count - this.threads);
	ensures this.count == count ** this.threads == threads;
	Program(int count, int threads) {
		this.count = count;
		this.threads = threads;
		this.f = new `Future`();
		this.f.counter = count;
		create f, f.pardecr(threads);
	}

// Recursively forks and joins `n` concurrent threads.
	given frac p;
	requires p <= 1;
	context n >= 0 ** p != none ** Value(f);
	context Value(count) ** Value(threads) ** AbstractState(f, counter == count - threads);
	requires Future(f, p, f.pardecr(n));
	ensures Future(f, p, empty);
	void spawn(int n) {
		if (n > 0) {
			// split-off a `decr()` process.
			split f, p\2, f.decr(), p\2, f.pardecr(n - 1);

// spawn `n` concurrent threads.
			Worker t = new Worker(this, p\2);
			fork t;
			spawn(n - 1) with { p = p\2; };
			join t;

// merge the resulting process.
			merge f, p\2, empty, p\2, empty;
		}
	}
}

class Main {

requires threads > 0;
	void main(int count, int threads) {
		Program p = new Program(count, threads);
		p.spawn(threads) with { p = 1; };

lock p;
		destroy p.f;
		assert p.f.counter == count - threads;
	}
}

Language: