sense_barrier.cub

(*

 Barrier for N process.

 We assume a global variable sense initialized to false and a variable
 count initialized to N.

 Each process has a local variable local_sense (initialized to false) as
 well as a variable level (initialized to 0).
 
 L1:  local_sense := not sense;
 L2:  count := count - 1;
 L3 : if count = 0 then (count := N; goto L5);
 L4 : if local_sense <> sense then goto L4;
 L5 : level := level + 1; goto L1

 The variable count is represented by an array Count[proc] : bool.

 (Example contributed by Luc Maranget)
 
 #define DECR(x) __sync_add_and_fetch(x,-1)

 typedef struct {
   unsigned int nprocs ;
   volatile unsigned int count ;
   volatile int go ;
 } barrier_t ;

 barrier_t alloc_barrier(int nprocs) {
   barrier_t *p = malloc_check(sizeof( *p)) ;
   p->nprocs = p->count = nprocs ;
   p->go = 0 ;
   return p ;
 }

 free_barrier(barrier_t *p { free(p) ; }

 void wait_barrier(barrier_t *p) {
   int sense = p->go ;
   int rem = DECR(&p->count) ;

   if (rem == 0) {
     p->count = p->nprocs ;
     p->go = !sense ;
   } else {
     while (p->go == sense) ;
   }
 }


 void *T1(void *_p) {
  ...
  for (int k = size-1 ; k >= 0 ; k--) {
   wait(q->b,&sense) ;
   q->x[k] = 1 ;
   int r1 = q->y[k] ;
   t[k] = r1 ;
  }
  ...
 }

*)


type loc = L1 | L2 | L3 | L4 | L5

var Sense : bool
array Local_sense[proc] : bool
array Level[proc] : int
array Count[proc] : bool
array PC[proc] : loc

init (z) { Sense = False && Local_sense[z] = False &&
           Level[z] = 0 && Count[z] = True && PC[z] = L1 }

(* unsafe (z1 z2) { Level[z1] + 2 <= Level[z2] } *)
unsafe (z1 z2) { PC[z1] = L1 && PC[z2] = L1 && Level[z1] <> Level[z2] }

transition enter (i)
requires { PC[i] = L1 }
{ 
  PC[i] := L2;
  Local_sense[j] := case | i = j && Local_sense[j] = True : False 
                         | i = j && Local_sense[j] = False : True
                         | _ : Local_sense[j];
}

transition decr (i)
requires { PC[i] = L2 }
{
  PC[i] := L3;
  Count[i] := False;
}


transition test_last (i)
requires { PC[i] = L3 && Count[i] = False && forall_other j. Count[j] = False }
{ 
  PC[i] := L5;
  Count[j] := case | _ : True;
  Sense := Local_sense[i]
}

transition test_wait (i k)
requires { PC[i] = L3 && Count[k] = True }
{ 
  PC[i] := L4;
}

transition wait (i)
requires { PC[i] = L4 && Local_sense[i] <> Sense }
{ 
  PC[i] := L4;
}

transition exit (i)
requires { PC[i] = L4 && Local_sense[i] = Sense }
{ 
  PC[i] := L5;
}

transition end (i)
requires { PC[i] = L5 }
{ 
  PC[i] := L1;
  Level[i] := Level[i] + 1;
}