ivy/test/flash2.ivy

#lang ivy1.7

# This is a model of the FLASH cache coherenec protocol.  The network
# is modeled in a relation way that is convenient for decidable
# invariant checking.

# In this version we prove coherence: an exclusive copy implies no other copies.


type id
type cache_state = { invalid, shared, exclusive }
type wait_type = { none, get, getX }

module cache_line = {
   individual wait : wait_type
   relation invmarked
   individual state : cache_state
}

module header = {
  relation pending
  relation local_
  relation dirty
  relation head
  individual hptr : id
  relation list
  relation real(X:id)
  relation upgrade
  relation shlist(X:id)
}

module network = {
  relation get(S:id,D:id)
  relation put(S:id,D:id)
  relation getX(S:id,D:id)
  relation putX(S:id,D:id)
  relation nak(S:id,D:id)
  relation fack(S:id,D:id)
  relation shwb(S:id,D:id)
}

module wb_network = {
  individual proc : id
  relation wb
}

individual home : id
instantiate cache(X:id) : cache_line
instantiate dir : header
relation collecting
individual requester : id
instantiate net : network
relation rp_net(X:id)
individual real_owner : id
individual fwd_get : wait_type
instantiate wbnet : wb_network
individual last_WB : id
relation nakc
relation invnet(X:id)
relation invack(X:id)

# locals used in actions

individual src : id
individual dst : id

after init {
    cache(X).state := invalid;
    cache(X).wait := none;
    cache(X).invmarked := false;
    dir.pending := false;
    dir.dirty := false;
    collecting := false;
    net.get(X,Y) := false;
    net.put(X,Y) := false;
    net.getX(X,Y) := false;
    net.putX(X,Y) := false;
    net.fack(X,Y) := false;
    net.shwb(X,Y) := false;
    net.nak(X,Y) := false;
    dir.list := false;
    dir.head := false;
    dir.shlist(X) := false;
    rp_net(X) := false;
    fwd_get := none;
    wbnet.wb := false;
    real_owner := home;
    invnet(X) := false;
    invack(X) := false;
    nakc := false;
    dir.local_ := false
}

action pi_Local_Get_dirty = {
    assume cache(home).state = invalid;
    assume cache(home).wait = none;
    assume ~dir.pending;
    assume dir.dirty;
    dir.pending := true;
    collecting := false;
    cache(home).wait := get;
    net.get(home,dir.hptr) := true;
    requester := home
}

action pi_Local_Get = {
    assume cache(home).state = invalid;
    assume cache(home).wait = none;
    assume ~dir.pending;
    assume ~dir.dirty;
    assume ~cache(home).invmarked;
    dir.local_ := true;
    cache(home).state := shared
}

# TODO: can this ever happen?

action pi_Local_Get_im = {
    assume cache(home).state = invalid;
    assume cache(home).wait = none;
    assume ~dir.pending;
    assume ~dir.dirty;
    assume cache(home).invmarked;
    cache(home).invmarked := false
}

action pi_Remote_Get = {
    assume src ~= home;
    assume cache(src).state = invalid;
    assume cache(src).wait = none;
    cache(src).wait := get;
    net.get(src,home) := true;
    src := *
}

action ni_Local_Get_nak = {
    assume net.get(src,home);
    assume home ~= src;
    assume ~rp_net(src);
    assume dir.pending | (dir.dirty & dir.local_ & cache(home).state~=exclusive) | (dir.dirty & ~dir.local_ & src = dir.hptr);
    net.get(src,home) := false;
    net.nak(home,src) := true
}

# action ni_Local_Get = {
#     assume net.get(src,home);
#     assume home ~= src;
#     assume ~dir.pending & ~dir.dirty & ~ rp_net(src) & ~cache(src).invmarked;
#     net.get(src,home) := false;
#     net.put(home,src) := true;
#     if (dir.head) {
#         dir.list := true;
# 	dir.shlist(src) := true;
# 	dir.real := dir.shlist # what is this?
#     }
#     else { 
# 	dir.head := true;
# 	dir.hptr := src
#     }
# }

action ni_Local_Get = {
    assume net.get(src,home);
    assume home ~= src;
    assume ~dir.pending & ~dir.dirty & ~ rp_net(src) & ~cache(src).invmarked;
    net.get(src,home) := false;
    net.put(home,src) := true;
    dir.head := true;
    dir.hptr := src;
    dir.shlist(src) := true;
    src := *
}

action ni_Local_Get_fwd = {
    assume net.get(src,home);
    assume home ~= src;
    assume ~dir.pending & dir.dirty & ~ rp_net(src) & ~dir.local_ & src ~= dir.hptr;
    net.get(src,home) := false;
    dir.pending := true;
    net.get(src,dir.hptr) := true;
    src := *
}

action ni_Remote_Put = {
    assume dst ~= home;
    assume net.put(src,dst);
    net.put(src,dst) := false;
    cache(dst).wait := none;
    cache(dst).state := shared;
    src := *;
    dst := *
}

# Non-deterministically drop a shared line from the cache. Send an rp message.
# informing the directory.

action pi_Remote_Replace = {
    assume cache(src).state=shared & cache(src).wait=none & src ~= home;
    cache(src).state := invalid;
    rp_net(src) := true;
    src := *
}

# Directory receives a replace message, removes sender from sharing list, assuming it is not head.

action ni_Replace_list = {
    assume rp_net(src);
    assume dir.hptr ~= src;
    rp_net(src) := false;
    dir.shlist(src) := false;
#    dir.real(src) := false;
    src := *
}

# Remote is invalid and wants an exclusive copy

action pi_Remote_GetX = {
    assume cache(src).state=invalid & cache(src).wait=none & src ~= home;
    cache(src).wait := getX;
    net.getX(src,home) := true;
    src := *
}

# Directory receives an exclusive request. This action handles the
# case when no invalidation is needed, that is, there is no exclusive
# copy and either the sharing list is empty or it contains only the
# source.

action ni_Local_GetX = {
    assume net.getX(src,home);
    assume home ~= src;
    assume ~dir.pending & ~dir.dirty;
    assume ~dir.head | src = dir.hptr;
    assume ~dir.head | ~dir.shlist(X) | X = src;
    assume ~rp_net(src);
    net.getX(src,home) := false;
    dir.dirty := true;
    dir.head := true;
    dir.hptr := src;
    dir.real(X) := X = src;
    dir.shlist(X) := X = src;
    net.putX(home,src) := true;
    real_owner := src; # ghost
    cache(home).state := invalid;
    cache(home).invmarked := (cache(home).wait = get & dir.local_) | cache(home).invmarked;
    dir.local_ := false;
    src := *
}

# Directory receives an exclusive request. This action handles the
# case when the request is nak'd

action ni_Local_GetX_nak = {
    assume net.getX(src,home);
    assume home ~= src;
    assume dir.pending | dir.dirty & cache(home).state ~= exclusive | src = dir.hptr; 
    assume ~rp_net(src);
    net.getX(src,home) := false;
    net.nak(home,src) := true;
    src := *
}


# Directory receives an exclusive request. This action handles the
# case when the request is pended.

action ni_Local_GetX_pend = {
    assume net.getX(src,home);
    assume home ~= src;
    assume ~dir.pending & dir.dirty & ~dir.local_ & src ~= dir.hptr; 
    assume ~rp_net(src);
    net.getX(src,home) := false;
    dir.pending :=  true;
    collecting := false;
    net.getX(src,dir.hptr) := true;
    fwd_get := getX;
    requester := src;
    src := *
}

# Directory receives an exclusive request. This action handles the
# case when invalidations are sent out.
 
action ni_localGetX_inv = {
    assume net.getX(src,home);
    assume home ~= src;
    assume ~dir.pending & ~dir.dirty & ~dir.local_; 
    assume dir.head;
    assume src ~= dir.hptr | (dir.shlist(dst) & dst~=src);
    assume ~rp_net(src);
    net.getX(src,home) := false;
    invnet(X) := X ~= home & X ~= src & dir.shlist(X);
    collecting := true;
    #   m1 := m;
    #   last_other_invack := (dir.hptr ~= src) ? dir.hptr . {i  . i in Proc, dir.shlist(i) & i~=src}; 
    cache(home).invmarked := (cache(home).wait = get & dir.local_) | cache(home).invmarked;
    dir.local_ := false;
    dir.dirty := true;
    dir.head := true; 
    dir.hptr := src;
    dir.pending := true;
    dir.real(X) := X ~= home & X ~= src & dir.shlist(X);
    dir.shlist(X) := X = src;
    net.putX(home,src) := true;
    real_owner := src;
    cache(home).state := invalid;
    src := *;
    dst := *
}

action ni_Remote_PutX = {
    assume net.putX(src,dst);
    assume dst~=home & cache(dst).wait = getX;
    net.putX(src,dst) := false;
    cache(dst).wait :=none;
    cache(dst).invmarked := false;
    cache(dst).state :=exclusive;
    src := *;
    dst := *
}

action pi_Remote_PutX = {
    assume cache(src).state = exclusive & src ~= home; # cache(src).wait=none ???
    cache(src).state := invalid;
    wbnet.proc := src;
    wbnet.wb := true;
    src := *
}

action ni_Inv = {
    assume invnet(dst) & dst~=home;
    invnet(dst) := false;
    invack(dst) := true;
    cache(dst).invmarked := (cache(dst).wait = get) | cache(dst).invmarked;
    cache(dst).state := invalid;
    dst := *
}

action ni_InvAck = {
      assume dir.pending & invack(src) & src~=home;
      assume dir.real(dst) & dst ~= src;
      invack(src) := false;
      dir.real(src) := false;
      # last_invack := src;
      # last_other_invack := {i : i in Proc, dir.real(i) & i ~= src};
      src := *;
      dst := *
}

action ni_InvAck_last = {
    assume dir.pending & invack(src) & src~=home;
    assume ~dir.real(X) | X = src;
    dir.pending := false;
    collecting := false;
    #	m1 := undefined; ???
    invack(src) := false;
    dir.real(src) := false;
    #	last_invack := src;
    if ( dir.local_ & ~ dir.dirty)  {
       dir.local_ := false
    }
}


action ni_WB = {
    assume wbnet.wb;
    wbnet.wb := false;
    dir.dirty := false;
    dir.head := false;
    dir.shlist(X) := false; 
    last_WB := wbnet.proc
}

action ni_Remote_GetX_nak = {
  assume net.getX(src,dst);
  assume dst ~=src & dst ~= home & cache(dst).state ~= exclusive;
  net.getX(src,dst) := false;
  fwd_get := none;
#  fwd_src := src;
  nakc := true;
  net.nak(dst,src) := true;
  src := *;
  dst := *
}

action ni_Remote_GetX_fwd = {
  assume net.getX(src,dst);
  assume dst ~=src & dst ~= home & cache(dst).state = exclusive;
  net.getX(src,dst) := false;
  cache(dst).state := invalid;
  fwd_get := none;
#  fwd_src := src;
  net.putX(dst,src) := true;
  real_owner := src;
  if src~=home {
    net.fack(src,home) := true
  };
  src := *;
  dst := *
}

action ni_FAck = {
  assume net.fack(src,home);
  net.fack(src,home) := false;
  dir.pending := false;
  if dir.dirty {
    dir.hptr := src;
    dir.shlist(X) := X = src
 };
 src := *
}

action ni_Remote_Get_nak = {
  assume net.get(src,dst);
  assume dst ~=src & dst ~= home & cache(dst).state ~= exclusive;
  net.get(src,dst) := false;
  fwd_get := none;
#  fwd_src := src;
  nakc := true;
  net.nak(dst,src) := true;
  src := *;
  dst := *
}

action ni_Remote_Get_fwd = {
  assume net.get(src,dst);
  assume dst ~=src & dst ~= home & cache(dst).state = exclusive;
  net.get(src,dst) := false;
#  assume ~cache(src).invmarked; TODO: ???
  cache(dst).state := shared;
  fwd_get := none;
#  fwd_src := src;
  net.put(dst,src) := true;
  if src~=home {
    real_owner := home;
    net.shwb(src,home) := true
  };
# shwb_src := dst;
  src := *;
  dst := *
}

action ni_ShWB = {
  assume net.shwb(src,home);
  net.shwb(src,home) := false;
  dir.pending := false;
  dir.dirty := false;
  dir.shlist(src) := true;
  dir.real(X) := dir.shlist(X);
# last_WB := shwb_src;
  src := *
}

action ni_NAK_Clear = {
  assume nakc;
  dir.pending := false;
  nakc := false
}

export pi_Local_Get_dirty
export pi_Local_Get
export pi_Local_Get_im
export pi_Remote_Get
export ni_Local_Get_nak
export ni_Local_Get
export ni_Local_Get_fwd
export ni_Remote_Put
export pi_Remote_Replace
export ni_Replace_list
export pi_Remote_GetX
export ni_Local_GetX
export ni_Local_GetX_nak
export ni_Local_GetX_pend
export ni_localGetX_inv
export ni_Remote_PutX
export pi_Remote_PutX
export ni_Inv
export ni_InvAck
export ni_InvAck_last
export ni_WB
export ni_Remote_GetX_nak
export ni_Remote_GetX_fwd
export ni_FAck
export ni_Remote_Get_nak
export ni_Remote_Get_fwd
export ni_ShWB
export ni_NAK_Clear

invariant [coherent1]
  cache(X).state = exclusive -> X = real_owner

invariant [coherent2]
  cache(X).state = exclusive & ~cache.invmarked(Y) & ~dir.pending -> cache(Y).state ~= shared

invariant [nodups]
  cache(X).state = exclusive -> dir.dirty & ~wbnet.wb & ~net.shwb(Y,home)

invariant net.putX(X,Y) -> Y = real_owner & dir.dirty & ~wbnet.wb & ~net.shwb(Z,home) & cache(Z).state ~= exclusive 

invariant net.shwb(Z,home) -> dir.dirty & dir.pending & ~collecting & ~wbnet.wb & ~net.putX(X,Y) & cache(X).state ~= exclusive  & ~net.fack(X,home) & ~nakc & ~net.put(X,home)

invariant wbnet.wb -> dir.dirty & ~net.putX(X,Y) & ~net.shwb(Z,home) & cache(X).state ~= exclusive

invariant net.putX(X,Y) & net.putX(Z,Y) -> X = Z

invariant net.shwb(X,home) & net.shwb(Z,home) -> X = Z

invariant net.get(X,Y) -> ~net.putX(Z,X) & ~net.getX(X,Z)

invariant net.put(X,Y) & net.put(Z,Y) -> X = Z

invariant net.get(X,Y) & net.get(X,Z) -> Y = Z

invariant net.put(X,Y) -> ~net.get(Y,Z) & ~net.getX(Y,Z) & ~net.putX(Z,Y)

invariant (net.put(X,Y) | cache.state(Y) = shared) & ~cache.invmarked(Y) 
       -> ~(dir.dirty & ~dir.pending)
          & (dir.pending & ~collecting & dir.head & (net.shwb(Y,home) | Y = home & ~cache.state(Y) = shared) | dir.pending & collecting & dir.real(Y) & invnet(Y) & Y ~= home | dir.head & dir.shlist(Y) & Y ~= home | dir.local_ & Y = home)
          & (dir.pending & collecting -> dir.real(Y))
          & ~net.fack(Q,home) & ~nakc
          & ((net.putX(Q,R) | cache(R).state = exclusive | wbnet.wb) -> dir.pending & collecting  & dir.real(Y) & invnet(Y) & Y ~= home)

invariant net.fack(X,home) -> dir.pending & ~collecting  & real_owner = X & ~nakc &  ~net.shwb(Y,home)

invariant net.fack(X,home) & net.fack(Y,home) -> X = Y

invariant invnet(X) -> collecting & ~invack(X) & dir.real(X)

invariant invack(X) -> collecting & ~invnet(X) & dir.real(X) & 
    (cache.state(X) = invalid & ~net.put(Y,X) | cache.invmarked(X))

invariant collecting & cache.state(X) = shared & ~cache.invmarked(X) -> dir.real(X)

invariant collecting -> dir.pending

invariant nakc -> dir.pending & ~collecting & ~net.fack(Q,home)

invariant (net.getX(X,Y) | net.get(X,Y)) & Y ~= home ->
         (dir.dirty -> dir.head) & dir.pending & ~collecting & ~net.fack(Q,home)
         & ~nakc & Y = real_owner & real_owner = dir.hptr
         & ~((net.put(Q,R) | cache.state(R) = shared) & ~cache.invmarked(R))
         & ~net.shwb(Q,home) & ~net.put(Q,home)

invariant ~((net.getX(X,Y) | net.get(X,Y)) & (net.getX(Z,Y) | net.get(Z,Y)) & X ~= Z & Y ~= home)

invariant dir.dirty & ~(dir.pending & ~collecting) -> real_owner = dir.hptr

invariant nakc -> real_owner = dir.hptr

invariant (net.get(X,Y) | net.put(Y,X)) -> cache.wait(X) = get

invariant (net.getX(X,Y) | net.putX(Y,X)) -> cache.wait(X) = getX

invariant cache.wait(X) ~= none -> cache.state(X) = invalid

invariant dir.dirty -> dir.head | dir.local_

invariant dir.pending & collecting -> ~dir.real(real_owner)

invariant net.getX(X,Y) -> ~net.putX(Z,X)

invariant net.getX(X,Y) & net.getX(X,Z) -> Y = Z

invariant rp_net(X) -> cache.state(X) = invalid & ~net.put(Y,X) & ~(net.get(X,Z) & Z ~= home)
    & ~net.putX(Y,X) & ~(net.getX(X,Z) & Z ~= home) & X ~= home

invariant dir.head -> dir.shlist(dir.hptr)

invariant net.put(X,home) -> dir.pending & ~collecting & ~net.fack(Y,home) & ~nakc & ~wbnet.wb & ~net.shwb(Y,home) & cache.state(Y) ~= exclusive & ~net.putX(Z,Y)

invariant cache.state(home) = shared -> ~dir.pending & ~dir.dirty

invariant cache.state(home) = invalid -> ~dir.local_

invariant cache.state(home) = exclusive -> dir.local_ & dir.dirty