<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
/* Wim H. Hesselink, 11 October 2004
   Making a queuing semaphore 
see [Concurrent Programming], section 4.2. 
We use the buffered channel p as the queue of the semaphore.
Additionally, we need synchronous channels v and out.
Here we illustrate its use with a mutual exclusion program. 
Phys Memory: 128, Estimated Size: 500, Max Search Depth 1000000
Compiler Option -DNOREDUCE; use partial order reduction.
Safety: assertions and invalid end-states 
Liveness: []<> !p, where #define p toggle
*/

#define Nproc 4 
chan v = [0] of {bit} ;      // contents are ignored
chan p = [Nproc] of {byte} ; // Nproc is maximal depth of queue
chan out = [0] of {byte} ;
byte crit ;
bit toggle ;

proctype semaphore (byte n) {
   byte waiter ;
   do 
   :: n > 0 ->    // be prepared for both v! and p!
      if
      :: atomic { v?_ ; n ++ }
      :: atomic { p?waiter ; n -- ; out!waiter } 
      fi
   :: n == 0 ->   // p! is disabled, be prepared for v!
      atomic { v?_ ; n ++ }
   od
}

proctype member (byte self) {
   do 
   :: atomic {
        p!self ;
        toggle = (self == 0  -> 1: toggle) // to verify progress
      }
      atomic {
        out?self ;
        crit ++ ;
        assert crit == 1 ;   // to verify mutual exclusion
        toggle = (self == 0 -> 0 : toggle)
      }
      atomic {
        crit -- ;
        v!0 
      }
   :: self != 0 -> break
   od
}

init {
   byte proc ;
   atomic {
     run semaphore(1) ;      // use (2) to see violation
     do
     :: proc < Nproc ->
        run member (proc) ;
        proc ++ 
     :: else -> break
     od
   }
}