Semaphore in Chalice, shared variable with multiple writers

Dec 13, 2011 at 9:56 AM

Hi, I'm trying to see if I can prove some properties of .net threaded code I have written. In the code I use the .net "System.Threading.ManualResetEventSlim" object. I don't know how to write its counterpart in Chalice. It is not a monitor, because threads do not acquire a lock on it. The idea that I had is to write it as a shared variable that acts like a semaphore, but multiple threads (methods) need to have write permission to the variable.

To illustrate it, I have made a small example, how I use it. It looks like a producer/consumer model, but a little bit altered for my needs. I think the code is self explaining but if anyone does not understand it ask me. Can anyone help me, to show how to do this. Or if it not possible please let me know.

Kind regards, Sybren Roede

class SemaphoreTest {
	var PauseGateWorkerA : int;
	var PauseGateWorkerB : int;

	var workitems: int
	var i: int;
	var j: int;

	method Main() {
		var cc := new SemaphoreTest{ workitems := 0, PauseGateWorkerA := 0, PauseGateWorkerB := 0, i := 0, j := 0 }
		share cc

		fork tk0 := cc.WorkerA()
		fork tk1 := cc.WorkerB()
		fork tk2 := cc.WorkerA()
		join tk0; 		join tk1; 		join tk2; 

		acquire cc; unshare cc
		assert cc.workitems == 0
		assert cc.i == 100
		assert cc.j == 100
	}

	method WorkerA()
		requires rd(mu) && waitlevel << mu
		requires acc(i) && acc(workitems) && acc(PauseGateWorkerA) && acc(PauseGateWorkerB)
		ensures rd(mu)
		ensures acc(i) && acc(workitems) && acc(PauseGateWorkerA) && acc(PauseGateWorkerB)
	{
		while (i < 100)
		{
			acquire this;
			if (workitems < 25 && i < 100)
			{
				i := i + 1;
				workitems := workitems + 1;
				PauseGateWorkerB := 0; //acts like PauseGateWorkerB.Set();
			}
			else
				PauseGateWorkerA := 1; //acts like PauseGateWorkerA.Reset();
			release this;
			while(PauseGateWorkerA == 1) //acts like PauseGateWorkerA.Wait();
			{
			}
		}
	}
	
	method WorkerB()
		requires rd(mu) && waitlevel << mu
		requires acc(j) && acc(workitems) && acc(PauseGateWorkerA) && acc(PauseGateWorkerB)
		ensures rd(mu)
		ensures acc(j) && acc(workitems) && acc(PauseGateWorkerA) && acc(PauseGateWorkerB)
	{
		while (j < 100)
		{
			acquire this;
			if (0 < workitems)
			{
				j := j + 1;
				workitems := workitems - 1;
				PauseGateWorkerA := 0; //acts like PauseGateWorkerA.Set();
			}
			else
				PauseGateWorkerB := 1; //acts like PauseGateWorkerB.Reset();
			release this;
			while(PauseGateWorkerB == 1) //acts like PauseGateWorkerB.Wait();
			{
			}
		}
	}	
}


System.Threading.ManualResetEventSlim