szymanski_boleslaw_bool_at.cub

(*
From: B. K. Szymanski. A Simple Solution to Lamport's Concurrent Programming
      Problem with Linear Wait. In Proceedings of the International Conference
      on Supercomputing Systems (ICS), 1988.

========================== ATOMIC VERSION ===========================

specific boolean intent, door_in, door_out = false;
local integer j in O..n-1;

P10: intent[i]:=true;
P11: wait until forall j: !intent[j] | !door_in[j];
P20: door_in[i]:=true;
P21: if exists j: intent[j] & !door_in[j] then begin intent[i]:=false;
P22:                                           wait until exists j: door_out[j];
                                               intent[i]:=true; end;
P30: door_out[i] := true;
E0 : wait until forall j>i: !door_in[j] | door_out[j];
P31: wait until forall j<i: !door_in[j];

CS : Critical Section

E1: intent[i]=false; door_in[i]=false; door_out[i]=false;

*)


type location = P10 | P11 | P20 | P21 | P22 | P30 | P31 | CS | E0 | E1
type flag = F0 | F1 | F2 | F3 | F4

array PC[proc] : location
array Intent[proc] : bool
array Door_in[proc] : bool
array Door_out[proc] : bool

init (x) { PC[x] = P10 && Intent[x] = False && Door_in[x] = False && Door_out[x] = False }


unsafe (z1 z2) { PC[z1] = CS && PC[z2] = CS }


transition p10 (i)
requires { PC[i] = P10 }
{
  Intent[i] := True;
  PC[i] := P11;
}

transition p11 (i)
requires { PC[i] = P11 &&
           forall_other j. (Intent[j] = False || Door_in[j] = False) }
{
  PC[i] := P20;
}

transition p20 (i)
requires { PC[i] = P20 }
{
  Door_in[i] := True;
  PC[i] := P21;
}

transition p21_then (i j)
requires { PC[i] = P21 && Intent[j] = True && Door_in[j] = False }
{
  Intent[i] := False;
  PC[i] := P22;
}

transition p21_else (i)
requires { PC[i] = P21 && forall_other j. (Intent[j] = False ||  Door_in[j] = True) }
{
  PC[i] := P30;
}

transition p22 (i j)
requires { PC[i] = P22 && Door_out[j] = True }
{
  Intent[i] := True;
  PC[i] := P30;
}

transition p30 (i)
requires { PC[i] = P30 }
{
  Door_out[i] := True;
  PC[i] := E0;
}

transition e0 (i)
requires { PC[i] = E0 &&
           forall_other j. (j < i || Door_in[j] = False || Door_out[j] = True) }
{
  PC[i] := P31;
}

transition p31 (i)
requires { PC[i] = P31 &&
           forall_other j. (i < j || Door_in[j] = False) }
{
  PC[i] := CS;
}

transition cs_exit (i)
requires { PC[i] = CS }
{
  PC[i] := E1;
}


transition e1 (i)
requires { PC[i] = E1 }
{
  Intent[i] := False;
  Door_in[i] := False;
  Door_out[i] := False;  
  PC[i] := P10;
}