szymanski_boleslaw_bool_na.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.

======================== NON ATOMIC VERSION =========================

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

P10: intent[i]:=true;
P11: while (j<n) if (intent[j] & door_in[j]) then j=0 else 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
array Cpt[proc, proc] : bool

init (x y) { PC[x] = P10 &&
             Intent[x] = False && Door_in[x] = False && Door_out[x] = False &&
             Cpt[x,y] = 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 p11_while_then (i j) *)
(* requires { PC[i] = P11 && *)
(*            Cpt[i,j] = False && (\* forall_other k. (j < k || Cpt[i,k] = True) && *\) *)
(*            Intent[j] = True && Door_in[j] = True } *)
(* { *)
(*   (\* Reset counter *\) *)
(*   Cpt[x,y] := case | x = i : False | _ : Cpt[x,y]; *)
(* } *)

(* transition p11_while_incr1 (i j) *)
(* requires { PC[i] = P11 && *)
(*            Cpt[i,j] = False && (\* forall_other k. (j < k || Cpt[i,k] = True) && *\) *)
(*            Intent[j] = False } *)
(* { *)
(*   Cpt[i,j] := True; (\* j++ *\) *)
(* } *)

(* transition p11_while_incr2 (i j) *)
(* requires { PC[i] = P11 && *)
(*            Cpt[i,j] = False && (\* forall_other k. (j < k || Cpt[i,k] = True) && *\) *)
(*            Door_in[j] = False } *)
(* { *)
(*   Cpt[i,j] := True; (\* j++ *\) *)
(* } *)

(* transition p11_while_exit (i) *)
(* requires { PC[i] = P11 && forall_other j. Cpt[i,j] = True } *)
(* { *)
(*   PC[i] := P20; *)
(*   (\* Reset counter *\) *)
(*   Cpt[x,y] := case | x = i : False | _ : Cpt[x,y]; *)
(* } *)


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 p21_abort_while (i j)
requires { PC[i] = P21 && Cpt[i,j] = False &&
           Intent[j] = True && Door_in[j] = False }
{
  Intent[i] := False;
  PC[i] := P22;
  (* Reset counter *)
  Cpt[x,y] := case | x = i : False | _ : Cpt[x,y];
}


transition p21_incr1 (i j)
requires { PC[i] = P21 && Cpt[i,j] = False &&
           Intent[j] = False }
{
  Cpt[i,j] := True;
}

transition p21_incr2 (i j)
requires { PC[i] = P21 && Cpt[i,j] = False &&
           Door_in[j] = True }
{
  Cpt[i,j] := True;
}


transition p21_exit_while (i)
requires { PC[i] = P21 && forall_other j. Cpt[i,j] = True }
{
  (* Reset counter *)
  Cpt[x,y] := case | x = i : False | _ : Cpt[x,y];
  PC[i] := P30;
}


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

transition p22_abort_while (i j)
requires { PC[i] = P22 &&  Cpt[i,j] = False &&
           Door_out[j] = True }
{
  Intent[i] := True;
  Door_out[i] := True;
  PC[i] := E0;
  (* Reset counter *)
  Cpt[x,y] := case | x = i : False | _ : Cpt[x,y];  
}

transition p22_incr (i j)
requires { PC[i] = P22 &&  Cpt[i,j] = False &&
           Door_out[j] = False }
{
  Cpt[i,j] := True;
}

transition p22_restart_while (i)
requires { PC[i] = P22 && forall_other j. Cpt[i,j] = True }
{
  (* Reset counter *)
  Cpt[x,y] := case | x = i : False | _ : Cpt[x,y];  
}



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 e0_incr1 (i j)
requires { PC[i] = E0 && Cpt[i,j] = False &&
           Door_in[j] = False }
{
  Cpt[i,j] := True;  
}

transition e0_incr2 (i j)
requires { PC[i] = E0 && i < j && Cpt[i,j] = False &&
           Door_out[j] = True }
{
  Cpt[i,j] := True;  
}

(* transition e0_incr3 (i j) *)
(* requires { PC[i] = E0 && j < i && Cpt[i,j] = False && *)
(*            Door_in[j] = False } *)
(* { *)
(*   Cpt[i,j] := True;   *)
(* } *)

transition e0_exit (i)
requires { PC[i] = E0 &&
           forall_other j. (Cpt[i,j] = True) }
{
  PC[i] := CS;
  (* not reseting counter *)
  (* Reset counter *)
  Cpt[x,y] := case | x = i : False | _ : Cpt[x,y];
}

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

(* transition p31_incr (i j) *)
(* requires { PC[i] = P31 && j < i && Cpt[i,j] = False && *)
(*            Door_in[j] = False } *)
(* { *)
(*   Cpt[i,j] := True;   *)
(* } *)

(* transition p31_exit (i j) *)
(* requires { PC[i] = P31 &&  *)
(*            forall_other j. (i < j || Cpt[i,j] = True) } *)
(* { *)
(*   PC[i] := CS; *)
(*   (\* Reset counter *\) *)
(*   Cpt[x,y] := case | x = i : False | _ : Cpt[x,y];  *)
(* } *)


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;
}