зеркало из https://github.com/microsoft/ivy.git
518 строки
13 KiB
XML
518 строки
13 KiB
XML
#lang ivy1.7
|
|
|
|
type id
|
|
type cache_state = { invalid, shared, exclusive }
|
|
type wait_type = { none, get, getX }
|
|
type unitype = { nouni, uGet, uGetX, uNAK, uPut, uPutX }
|
|
type swhbtype = {noshwb,shwb,fack}
|
|
|
|
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)
|
|
}
|
|
|
|
object net(self:id) = {
|
|
var mtype : unitype
|
|
var proc : id
|
|
}
|
|
|
|
module wb_network = {
|
|
individual proc : id
|
|
relation wb
|
|
}
|
|
|
|
object shwbnet = {
|
|
var mtype : swhbtype
|
|
var proc : id
|
|
}
|
|
|
|
individual home : id
|
|
instantiate cache(X:id) : cache_line
|
|
instantiate dir : header
|
|
relation collecting
|
|
individual requester : id
|
|
relation rp_net(X:id)
|
|
individual real_owner : id
|
|
individual last_owner : id
|
|
individual fwd_get : wait_type
|
|
individual fwd_src : id
|
|
individual excl_src : id
|
|
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.mtype(S) := nouni;
|
|
shwbnet.mtype := noshwb;
|
|
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;
|
|
real_owner := home
|
|
}
|
|
|
|
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(home).mtype := uGet;
|
|
net(home).proc := dir.hptr;
|
|
fwd_get := get;
|
|
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(src).mtype := uGet;
|
|
net(src).proc := home;
|
|
src := *
|
|
}
|
|
|
|
action ni_Local_Get_nak = {
|
|
assume net(src).mtype = uGet & net(src).proc = 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(src).mtype := uNAK;
|
|
}
|
|
|
|
# action ni_Local_Get_fwd = {
|
|
# assume net(src).mtype = uGet & net(src).proc = 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(src).mtype = uGet & net(src).proc = home;
|
|
assume home ~= src;
|
|
assume ~dir.pending & ~dir.dirty & ~ rp_net(src) & ~cache(src).invmarked;
|
|
net(src).mtype := uPut;
|
|
dir.head := true;
|
|
dir.hptr := src;
|
|
dir.shlist(src) := true;
|
|
src := *
|
|
}
|
|
|
|
action ni_Local_Get_fwd = {
|
|
assume net(src).mtype = uGet & net(src).proc = home;
|
|
assume home ~= src;
|
|
assume ~dir.pending & dir.dirty & ~ rp_net(src) & ~dir.local_ & src ~= dir.hptr;
|
|
net(src).proc := dir.hptr;
|
|
fwd_get := get;
|
|
dir.pending := true;
|
|
src := *
|
|
}
|
|
|
|
action ni_Remote_Put = {
|
|
assume dst ~= home;
|
|
assume net(dst).mtype = uPut;
|
|
net(dst).mtype := nouni;
|
|
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(src).mtype := uGetX;
|
|
net(src).proc := home;
|
|
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(src).mtype = uGetX & net(src).proc = 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(src).mtype := uPutX;
|
|
dir.dirty := true;
|
|
dir.head := true;
|
|
dir.hptr := src;
|
|
dir.real(X) := X = src;
|
|
dir.shlist(X) := X = src;
|
|
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(src).mtype = uGetX & net(src).proc = home;
|
|
assume home ~= src;
|
|
assume dir.pending | dir.dirty & cache(home).state ~= exclusive | src = dir.hptr;
|
|
assume ~rp_net(src);
|
|
net(src).mtype := uNAK;
|
|
src := *
|
|
}
|
|
|
|
|
|
# Directory receives an exclusive request. This action handles the
|
|
# case when the request is pended.
|
|
|
|
action ni_Local_GetX_pend = {
|
|
assume net(src).mtype = uGetX & net(src).proc = home;
|
|
assume home ~= src;
|
|
assume ~dir.pending & dir.dirty & ~dir.local_ & src ~= dir.hptr;
|
|
assume ~rp_net(src);
|
|
dir.pending := true;
|
|
collecting := false;
|
|
net(src).proc := dir.hptr;
|
|
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(src).mtype = uGetX & net(src).proc = 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(src).mtype := uPutX;
|
|
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;
|
|
real_owner := src;
|
|
cache(home).state := invalid;
|
|
src := *;
|
|
dst := *
|
|
}
|
|
|
|
action ni_Remote_PutX = {
|
|
assume net(dst).mtype = uPutX & net(dst).proc = src;
|
|
assume dst~=home & cache(dst).wait = getX;
|
|
net(dst).mtype := nouni;
|
|
cache(dst).wait :=none;
|
|
cache(dst).invmarked := false;
|
|
cache(dst).state := exclusive;
|
|
excl_src := src;
|
|
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;
|
|
real_owner := home;
|
|
last_owner := src;
|
|
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(src) & 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 & dir.real(src);
|
|
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(src).mtype = uGetX & net(src).proc = dst;
|
|
assume dst ~=src & dst ~= home & cache(dst).state ~= exclusive;
|
|
net(src).mtype := uNAK;
|
|
fwd_get := none;
|
|
fwd_src := src;
|
|
nakc := true;
|
|
src := *;
|
|
dst := *
|
|
}
|
|
|
|
action ni_Remote_GetX_fwd = {
|
|
assume net(src).mtype = uGetX & net(src).proc = dst;
|
|
assume dst ~=src & dst ~= home & cache(dst).state = exclusive;
|
|
net(src).mtype := uPutX;
|
|
cache(dst).state := invalid;
|
|
fwd_get := none;
|
|
fwd_src := src;
|
|
real_owner := src;
|
|
last_owner := dst;
|
|
if src~=home {
|
|
shwbnet.mtype := fack;
|
|
shwbnet.proc := src
|
|
};
|
|
src := *;
|
|
dst := *
|
|
}
|
|
|
|
action ni_FAck = {
|
|
assume shwbnet.mtype = fack;
|
|
shwbnet.mtype := noshwb;
|
|
dir.pending := false;
|
|
if dir.dirty {
|
|
dir.hptr := shwbnet.proc;
|
|
dir.shlist(X) := X = shwbnet.proc;
|
|
}
|
|
}
|
|
|
|
action ni_Remote_Get_nak = {
|
|
assume net(src).mtype = uGet & net(src).proc = dst;
|
|
assume dst ~=src & dst ~= home & cache(dst).state ~= exclusive;
|
|
net(src).mtype := uNAK;
|
|
fwd_get := none;
|
|
fwd_src := src;
|
|
nakc := true;
|
|
src := *;
|
|
dst := *
|
|
}
|
|
|
|
action ni_Remote_Get_fwd = {
|
|
assume net(src).mtype = uGet & net(src).proc = dst;
|
|
assume dst ~=src & dst ~= home & cache(dst).state = exclusive;
|
|
net(src).mtype := uPut;
|
|
# assume ~cache(src).invmarked; TODO: ???
|
|
cache(dst).state := shared;
|
|
fwd_get := none;
|
|
fwd_src := src;
|
|
last_owner := dst;
|
|
real_owner := home;
|
|
if src~=home {
|
|
shwbnet.mtype := shwb;
|
|
shwbnet.proc := src;
|
|
};
|
|
# shwb_src := dst;
|
|
src := *;
|
|
dst := *
|
|
}
|
|
|
|
action ni_ShWB = {
|
|
assume shwbnet.mtype = shwb;
|
|
shwbnet.mtype := noshwb;
|
|
dir.pending := false;
|
|
dir.dirty := false;
|
|
dir.shlist(shwbnet.proc) := true;
|
|
dir.real(X) := dir.shlist(X);
|
|
# last_WB := shwb_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
|
|
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 [coherent]
|
|
cache(X).state = exclusive -> X = real_owner
|
|
proof let H = home, Y = excl_src
|
|
|
|
invariant [coherent2]
|
|
cache(X).state = shared & ~cache.invmarked(X) & ~dir.pending -> real_owner = home & cache.state(home) ~= exclusive
|
|
proof let H = home, Y = last_owner
|
|
|
|
invariant [nodups]
|
|
cache(X).state = exclusive -> dir.dirty & ~wbnet.wb & shwbnet.mtype ~= shwb
|
|
proof let H = home
|
|
|
|
# invariant [nonint1]
|
|
# net.shwb(X,home) -> dir.pending & dir.dirty & X = dir.hptr
|
|
# proof let H = home
|
|
|
|
|
|
|
|
# invariant [l4]
|
|
# cache(dst).state = exclusive ->
|
|
# dir.dirty & ~wbnet.wb & ~net.shwb(X,home)
|
|
# & ~net.put(X,home)
|
|
# & ((cache(X).state = exclusive | net.putX(Y,X)) -> dst = X)
|
|
# proof let H = home, Y = dst
|
|
|
|
invariant [l5]
|
|
net.proc(X) ~= home -> (net.mtype(X) = uGet -> fwd_get = get) & (net.mtype(X) = uGetX -> fwd_get = getX)
|
|
proof let H = home, Y = fwd_src
|
|
|
|
invariant [l6]
|
|
invack(X) & dir.real(X) -> dir.pending & collecting
|
|
proof let H = home
|
|
|
|
include mc_schemata
|
|
|
|
attribute method = mc
|