Model-based reasoning: locking protocol

Verification example where model-based reasoning is used to verify that the program adheres to a certain locking protocol.

General Information

Backend: Silicon
Language: PVL
Features: Atomics, Futures
Path to Example File: futures/locking.pvl
Should Verify: Yes
Date: 2017-06-19
Lines of Code: 80 (comments not included)
Lines of Specification: 36 (45.0% of total)
Computation Time: 25.6 seconds

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

class `Future` {
	boolean flag;
	
	modifies flag;
	requires !flag;
	ensures flag;
	process acquire(); 
	
	modifies flag;
	ensures !flag;
	process release();

process Locked() = release() * Unlocked();
	process Unlocked() = acquire() * Locked();
}

class Lock {
	`Future` m;
	
	resource lock_invariant() = Value(m) ** HPerm(m.flag, write);
	
	/** constructs a new lock (with associated model `m`). */
	requires HPerm(m.flag, write);
	Lock(`Future` m) {
		this.m = m;
	} 
	
	/** atomically updates `m.flag` by `newval` when it holds the value `oldval`. */
	given frac p;
	given process P;
	context Value(m) ** p != none;
	requires Future(m, p, P);
	ensures  (\result && !oldval && newval && P == m.Unlocked()) ==> Future(m, p, m.Locked());
	ensures !(\result && !oldval && newval && P == m.Unlocked()) ==> Future(m, p, P);
	boolean atomic_cas(boolean oldval, boolean newval);
	
	/** atomically writes `val` to `m.flag`. */
	given frac p;
	given process P;
	context Value(m) ** p != none;
	requires Future(m, p, P);
	ensures  (!val && P == m.Locked()) ==> Future(m, p, m.Unlocked());
	ensures !(!val && P == m.Locked()) ==> Future(m, p, P);
	void atomic_set(boolean val);
	
	/** acquires the lock */
	given frac p;
	context Value(m) ** p != none;
	requires Future(m, p, m.Unlocked());
	ensures Future(m, p, m.Locked());
	void acquire() {
		boolean b = false;
		loop_invariant Value(m);
		loop_invariant !b ==> Future(m, p, m.Unlocked());
		loop_invariant b ==> Future(m, p, m.Locked());
		while (!b) {
			b = atomic_cas(false, true) with { 
				P = m.Unlocked();
				p = p; 
			};
		}
	}
	
	/** releases the lock */
	given frac p;
	context Value(m) ** p != none;
	requires Future(m, p, m.Locked());
	ensures Future(m, p, m.Unlocked());
	void release() {
		atomic_set(false) with { 
			P = m.Locked();
			p = p;
		};
	}
}

Language: