german.ctc_finite.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 = Data1 | Data2

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 = Data1 &&
     AuxData = Data1 
     }


(* 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 store1 (n)
requires { CacheState[n] = Exclusive }
{
  AuxData := Data1;
  CacheData[j] := case 
    	       	  | j = n : Data1
	       	  | _  : CacheData[j];
}

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

transition sendReqs (i)
requires { Chan1Cmd[i] = Empty && CacheState[i] = Invalid }
{
  Chan1Cmd[i] := Reqs;
}

transition sendReqe (i)
requires { Chan1Cmd[i] = Empty && CacheState[i] <> Exclusive }
{
  Chan1Cmd[i] := Reqe;
}


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


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

transition sendInv1 (i)
requires { Chan2Cmd[i] = Empty && Invset[i] = True && Curcmd = Reqe }
{
  Chan2Cmd[i] := Inv;
  Invset[i] := False;
}

transition sendInv2 (i)
requires { Chan2Cmd[i] = Empty && Invset[i] = True && Curcmd = Reqs &&
           Exgntd = True }
{
  Chan2Cmd[i] := Inv;
  Invset[i] := False;
}


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

transition recvInvack1 (i)
requires { Chan3Cmd[i] = Invack && Curcmd <> Empty && Exgntd = False } 
{
  Chan3Cmd[i] := Empty;
  Shrset[i] := False;
}

transition recvInvack2 (i)
requires { Chan3Cmd[i] = Invack && Curcmd <> Empty && Exgntd = True } 
{
  Chan3Cmd[i] := Empty;
  Shrset[i] := False;
  Exgntd := False;
  MemData := Chan3Data[i];
}

transition sendGnts (i)
requires { Curcmd = Reqs && CurClient = i && Chan2Cmd[i] = Empty && Exgntd = False }
{
  Chan2Cmd[i] := Gnts;
  Chan2Data[i] := MemData;
  Shrset[i] := True;
  Curcmd := Empty;
}

transition sendGnte (i)
requires { Curcmd = Reqe && CurClient = i && Chan2Cmd[i] = Empty && Exgntd = False &&
           Shrset[i] = False && forall_other j. Shrset[j] = False }
{
  Chan2Cmd[i] := Gnte;
  Chan2Data[i] := MemData;
  Shrset[i] := True;
  Curcmd := Empty;
  Exgntd := True;
}

transition recvGnts (i)
requires { Chan2Cmd[i] = Gnts }
{
  CacheState[i] := Shared;
  CacheData[i] := Chan2Data[i];
  Chan2Cmd[i] := Empty;
}

transition recvGnts (i)
requires { Chan2Cmd[i] = Gnte }
{
  CacheState[i] := Exclusive;
  CacheData[i] := Chan2Data[i];
  Chan2Cmd[i] := Empty;
}