// --------------------------------------------------------------------	
// This file implements a simple Mutex protocol that is controlled via	
// a boolean lock variable. Processes wait until that lock variable is	
// false, and set it afterwards while entering their critical section.	
//  Protocols like this simple protocol require to have an atomic
// test-and-set operation that is assumed to be provided by the hardware
// platform.
//				
//  References: G.R. Andrews' book, Concurrent Programming, p.103, 1991	
// --------------------------------------------------------------------	

package Communication.MutexProtocols.SpinLock;

// number of processes
macro NumProc = 3;


module SpinLockMutexProtocol
   (event ?leave_cs,		// instructs to leave the critical section
    nat{NumProc()} ?go,		// used to control interleaved execution
    bool lock,			// lock variable tells whether cs is free
    nat{4} crit_var,		// shared variable used in critic section
    [NumProc()] bool !done,	// to check successful termination
    [NumProc()] bool !spin)	// to see that process applies for CS
{
   lock = false;
   crit_var = 0;
   for(i=0 .. (NumProc()-1))
      suspend
         loop {
	    EntryProtocol(spin[i],lock);
	    CriticalSection(leave_cs,crit_var);
	    ExitProtocol(done[i],lock);
         }
      when(go!=i);
}satisfies {
   // ============================================================
   MutualExclusive:
   // ------------------------------------------------------------
   // at most one process can enter critical section
   // ------------------------------------------------------------
	assert A G (crit_var <= 1);
   // ============================================================
   EnterLemma:
   // ------------------------------------------------------------
   // a process will enter its critical section if it currently
   // is enabled by the scheduler in a stage where it applies
   // for the critical section and the critical section is free
   // note that
   // ------------------------------------------------------------
	assert A G
	   forall(i=0 .. (NumProc()-1))
                (spin[i] & !lock & (go==i) -> A X !spin[i])
           ;
   // ============================================================
   ConverseEnterLemma:
   // ------------------------------------------------------------
   // conversely, it can only leave the spin lock if the critical
   // section is free and the process is enabled for execution
   // ------------------------------------------------------------
	assert A G
	   forall(i=0 .. (NumProc()-1))
                (spin[i] & X !spin[i] -> !lock & (go==i))
           ;
   // ============================================================
   NoDeadlock:
   // ------------------------------------------------------------
   // if several processes apply for accessing the critical section
   // and the critical section is free, then one of them enters it
   // ------------------------------------------------------------
	assert A G
	  ((crit_var==0)
           ->
	   forall(i=0 .. (NumProc()-1))
                (spin[i] & (go==i) -> A X (!spin[i] & crit_var>0))
	  );
   // ============================================================
   FairnessRequiresTermination:
   // ------------------------------------------------------------
   // the protocol is fair only if all processes will eventually
   // leave their critical section
   // ------------------------------------------------------------
	assert A (
	   (G forall(i=0 .. (NumProc()-1))
		 F done[i]) 
	   ->
	   (G forall(i=0 .. (NumProc()-1))
                 F(leave_cs & (go==i)) )
	  );
   // ============================================================
   EventualEntry:
   // ------------------------------------------------------------
   // fairness is very hard to achieve: it only holds if the
   // scheduler does not always choose the same process out of
   // the processes that are applying for the critical section
   // ------------------------------------------------------------
	assert A (
	   (G forall(i=0 .. (NumProc()-1))
                 F(spin[i] & !lock & (go==i)))
	   ->
	   (G forall(i=0 .. (NumProc()-1))
		 F done[i])
	  );
   // ============================================================
}