Model-based reasoning: unequal counting

A variant on the verification example of concurrent counting: two threads that concurrently decrement a shared value, but with unequal amounts.

General Information

Backend: Silicon
Language: PVL
Features: Fork/join concurrency, Statically-scoped locking, Statically-scoped parallelism
Path to Example File: futures/unequalcounting.pvl
Should Verify: Yes
Date: 2017-06-19
Lines of Code: 52 (comments not included)
Lines of Specification: 19 (36.5% of total)
Computation Time: 19.9 seconds

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

class `Future` {
	int counter;
	
	modifies counter;
	ensures counter == \old(counter) + n;
	process plus(int n);
	
	modifies counter;
	ensures counter == \old(counter) * n;
	process mult(int n);
	
	requires counter > 0 && n > 0;
	ensures (counter == (\old(counter) + n) * n) || (counter == (\old(counter) * n) + n);
	process parcount(int n) = plus(n) || mult(n);
}

class Program {

requires c > 0 && n > 0;
	ensures \result == (c + n) * n || \result == (c * n) + n;
	int count(int c, int n) {
		`Future` f = new `Future`();
		f.counter = c;
		create f, f.parcount(n);
		split f, 1\2, f.plus(n), 1\2, f.mult(n);
		
		invariant lockinv(HPerm(f.counter, write)) {
			par T0() 
				requires Future(f, 1\2, f.plus(n));
				ensures Future(f, 1\2, empty); 
			{
				atomic(lockinv) {
					action(f, 1\2, empty, f.plus(n)) { f.counter = f.counter + n; }
				}
			}
			and T1() 
				requires Future(f, 1\2, f.mult(n));
				ensures Future(f, 1\2, empty);
			{
				atomic(lockinv) {
					action(f, 1\2, empty, f.mult(n)) { f.counter = f.counter * n; }
				}
			}
		}
		
		merge f, 1\2, empty, 1\2, empty;
		destroy f;
		
		return f.counter;
	}
}

Language: