german_data.cub

(*

CacheState Coherence Protocol (Steve German, 2001)

ExGntd   |------|                                 |-----------|
CurCmd   |      | <-- Chan1 (excl/shared req.) -- |           |  Invalide/
CurPtr   | Home | --- Chan2 (grants or inv.) ---> | Client(i) |  Shared/
InvSet   |      | <-- Chan3 (inv. ack) ---------- |           |  Exclusive
ShrSet   |------|                                 |-----------|

Data paths from Chou, Manava and Park version

*)

type state = Invalid | Shared | Exclusive
type msg = Empty | Reqs | Reqe | Inv | Invack | Gnts | Gnte
type data

var Exgntd : bool
var Curcmd : msg
var CurClient : proc

var MemData : data
var AuxData : data
var Store_data : data

array Chan1Cmd[proc] : msg
array Chan1Data[proc] : data

array Chan2Cmd[proc] : msg
array Chan2Data[proc] : data

array Chan3Cmd[proc] : msg
array Chan3Data[proc] : data

array CacheState[proc] : state
array CacheData[proc] : data

array Invset[proc] : bool
array Shrset[proc] : bool

init (z) { 		   
     Chan1Cmd[z] = Empty &&
     Chan2Cmd[z] = Empty &&
     Chan3Cmd[z] = Empty &&
     CacheState[z] = Invalid &&
     Invset[z] = False &&
     Shrset[z] = False &&
     Curcmd = Empty &&
     Exgntd = False &&
     MemData = Store_data && (* oblige de mettre ca sinon   *)
     AuxData = Store_data    (* ca foire a cause des gardes *)
     	       		     (* universelles (approx.)      *)
     }


(* Control *)
unsafe (z1 z2) { CacheState[z1] = Exclusive && CacheState[z2] <> Invalid }


(* Data *)
unsafe () { Exgntd = False && MemData <> AuxData }
unsafe (z) { CacheState[z] <> Invalid && CacheData[z] <> AuxData }


transition send_req_shared(n)
requires { CacheState[n] = Invalid && Chan1Cmd[n] = Empty }
{
  Chan1Cmd[j] := case 
  	        | j = n : Reqs 
		| _ : Chan1Cmd[j];
}

transition send_req_exclusive_1(n)
requires { CacheState[n] = Invalid && Chan1Cmd[n] = Empty }
{ 
  Chan1Cmd[j] := case
  	       | j = n : Reqe 
	       | _ : Chan1Cmd[j] ;
}

transition send_req_exclusive_2(n)
requires { CacheState[n] = Shared && Chan1Cmd[n] = Empty }
{
  Chan1Cmd[j] := case 
   	       | j = n : Reqe 
	       | _ : Chan1Cmd[j] ;
}

transition recv_req_shared(n)
requires { Curcmd = Empty && Chan1Cmd[n] = Reqs }
{ 
  Curcmd := Reqs; 
  CurClient := n; 
  Invset[j] := case | _ : Shrset[j];
  Chan1Cmd[j] := case 
  	       | j = n: Empty 
	       | _ : Chan1Cmd[j];
}

transition recv_req_exclusive(n)
requires { Curcmd = Empty && Chan1Cmd[n] = Reqe }
{ 
  Curcmd := Reqe; 
  CurClient := n; 
  Invset[j] := case | _ : Shrset[j];
  Chan1Cmd[j] := case 
  	       | j = n : Empty 
	       | _ : Chan1Cmd[j] ;
}

transition send_inv_1(n)
requires { Chan2Cmd[n] = Empty && Invset[n] = True && Curcmd = Reqe }
{ 
  Chan2Cmd[j] := case
	       | j = n : Inv 
	       | _ : Chan2Cmd[j] ;
  Invset[j] := case
  	       | j = n : False 
	       | _ : Invset[j];
}

transition send_inv_2(n)
requires { Chan2Cmd[n] = Empty && Invset[n] = True && 
	  Curcmd = Reqs && Exgntd = True}
{ 
  Chan2Cmd[j] := case
  	       | j = n : Inv 
	       | _ : Chan2Cmd[j] ;
  Invset[j] := case 
  	       | j = n : False 
	       | _ : Invset[j] ;
}

transition send_invack_noex(n)
requires { Chan2Cmd[n] = Inv && Chan3Cmd[n] = Empty &&
	   CacheState[n] <> Exclusive }
{
  Chan2Cmd[j] := case
  	       | j = n : Empty 
	       | _ : Chan2Cmd[j] ;
  Chan3Cmd[j] := case
  	       | j = n : Invack 
	       | _ : Chan3Cmd[j] ;
  CacheState[j] := case 
  	       | j = n : Invalid 
	       | _ : CacheState[j] ;
}

transition send_invack_ex(n)
requires { Chan2Cmd[n] = Inv && Chan3Cmd[n] = Empty &&
	   CacheState[n] = Exclusive }
{
  Chan2Cmd[j] := case
  	       | j = n : Empty 
	       | _ : Chan2Cmd[j] ;
  Chan3Cmd[j] := case
  	       | j = n : Invack 
	       | _ : Chan3Cmd[j] ;
  Chan3Data[j] := case
  	       | j = n : CacheData[n] 
	       | _ : Chan3Data[j] ;
  CacheState[j] := case 
  	       | j = n : Invalid 
	       | _ : CacheState[j] ;
}

transition recv_invack_noex(n)
requires { Chan3Cmd[n] = Invack && Curcmd <> Empty && Exgntd = False }
{ 
  Chan3Cmd[j] := case 
  	       | j = n : Empty 
	       | _ : Chan3Cmd[j] ;
  Shrset[j] := case
  	        | j = n : False 
		| _ : Shrset[j] ;
}

transition recv_invack_ex(n)
requires { Chan3Cmd[n] = Invack && Curcmd <> Empty  && Exgntd = True }
{ 
  Exgntd := False;
  Chan3Cmd[j] := case 
  	       | j = n : Empty 
	       | _ : Chan3Cmd[j] ;
  Shrset[j] := case
  	        | j = n : False 
		| _ : Shrset[j] ;
  MemData := Chan3Data[n];
}

transition send_gnt_shared(n)
requires { CurClient = n && Curcmd = Reqs && 
	  Exgntd = False && Chan2Cmd[n] = Empty }
{ 	  
  Curcmd := Empty;
  Chan2Cmd[j] := case 
  	       | j = n : Gnts 
	       | _ : Chan2Cmd[j] ;
  Chan2Data[j] := case 
  	       | j = n : MemData 
	       | _ : Chan2Data[j] ;
  Shrset[j] := case 
	        | j = n : True 
		| _ : Shrset[j] ;
}

transition send_gnt_exclusive(n)
requires { CurClient = n && Curcmd = Reqe &&
	  Chan2Cmd[n] = Empty && Shrset[n] = False && 
          forall_other j. Shrset[j] = False }
{ 
  Curcmd := Empty; 
  Exgntd := True ;
  Chan2Cmd[j] := case
               | j = n : Gnte 
	       | _ : Chan2Cmd[j] ;
  Chan2Data[j] := case 
  	       | j = n : MemData 
	       | _ : Chan2Data[j] ;
  Shrset[j] := case 
	       | j = n : True 
	       | _ : Shrset[j] ;
}

transition recv_gnt_shared(n)
requires { Chan2Cmd[n] = Gnts }
{
  CacheState[j] := case 
               | j = n : Shared 
	       | _ : CacheState[j] ;
  CacheData[j] := case 
               | j = n : Chan2Data[n]
	       | _ : CacheData[j] ;
  Chan2Cmd[j] := case 
	       | j = n : Empty 
	       | _ : Chan2Cmd[j] ;
}

transition recv_gnt_exclusive(n)
requires { Chan2Cmd[n] = Gnte }
{
  CacheState[j] := case 
               | j = n : Exclusive 
	       | _ : CacheState[j] ;
  CacheData[j] := case 
               | j = n : Chan2Data[n]
	       | _ : CacheData[j] ;
  Chan2Cmd[j] := case 
	       | j = n : Empty 
	       | _ : Chan2Cmd[j] ;
}

transition store (n)
requires { CacheState[n] = Exclusive }
{
  AuxData := Store_data;
  CacheData[j] := case 
    	       	  | j = n : Store_data
	       	  | _  : CacheData[j];
  Store_data := .;
}