зеркало из https://github.com/microsoft/ivy.git
refactoring tilelink spec
This commit is contained in:
Ken McMillan
Родитель
ec70b1b5db
Коммит
8fb2863d18
|
|
@ -327,7 +327,7 @@ module server_top(ref,me,net) = {
|
|||
|
||||
# Delegated shards have correct data
|
||||
|
||||
conjecture net.delegated(X,S) & shard_lo(S) <= K & K <= shard_hi(S) -> shard_value(S,K) = ref.hash(K)
|
||||
# conjecture net.delegated(X,S) & shard_lo(S) <= K & K <= shard_hi(S) -> shard_value(S,K) = ref.hash(K)
|
||||
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -29,13 +29,13 @@ module total_order(carrier) = {
|
|||
# could add <= as derived relation here
|
||||
}
|
||||
|
||||
########################################
|
||||
# type of global time
|
||||
type time
|
||||
instantiate total_order(time)
|
||||
|
||||
########################################
|
||||
# type of local time
|
||||
#
|
||||
# Every memory operation is assigned a unique local time
|
||||
#
|
||||
|
||||
type ltime
|
||||
instantiate total_order(ltime)
|
||||
|
||||
|
|
@ -47,10 +47,6 @@ type data
|
|||
# type of memory addresses
|
||||
type addr
|
||||
|
||||
########################################
|
||||
# type of message types
|
||||
type mtype = { grant_t, release_t, request_t, response_t}
|
||||
|
||||
########################################
|
||||
# type of ownership state
|
||||
type ownership = { none, shrd, excl }
|
||||
|
|
@ -61,7 +57,7 @@ type side = {client,manager}
|
|||
|
||||
########################################
|
||||
# type of memory ops
|
||||
type otype = {read, write, cas}
|
||||
type otype = {read, write, amo}
|
||||
|
||||
########################################
|
||||
# id's of protocol agents
|
||||
|
|
@ -69,17 +65,20 @@ type id
|
|||
|
||||
########################################
|
||||
# structure of memory events to serialize
|
||||
#
|
||||
# A memory event has operation, address, data and an id indicating
|
||||
# which CPU produced the event. It also has flags indicating whether
|
||||
# the even thas been serialized or fused. Initially, all events are
|
||||
# unserialized.
|
||||
########################################
|
||||
|
||||
module memev = {
|
||||
individual type_ : otype
|
||||
individual addr_ : addr
|
||||
individual data_ : data # data for write and cas
|
||||
relation result(D:data) # value for read and cas
|
||||
individual id_ : id # process id of op
|
||||
relation serialized
|
||||
relation fused
|
||||
individual time_ :time # serialized time if any
|
||||
|
||||
axiom result(T) & result(U) -> T = U
|
||||
individual data_ : data # data for write and amo
|
||||
individual id_ : id # process id of op
|
||||
individual serialized : bool # has this event been serialized?
|
||||
relation fused : bool # has this event been fused?
|
||||
|
||||
init ~serialized & ~fused
|
||||
}
|
||||
|
|
@ -88,12 +87,12 @@ module memev = {
|
|||
#
|
||||
# Reference specification
|
||||
#
|
||||
# This module describes a set of memory events ordered by local
|
||||
# time. It provides actions that assign global time to events in
|
||||
# increasing order. The pre-conditions of these actions enforce the
|
||||
# consistency model (that is, what orderings in local time must be
|
||||
# preserved in global time). This ordering condition is determined by
|
||||
# the relation "prevents" (see below).
|
||||
# This module defines the memory semantics. It contains a map from local time
|
||||
# to memory events produced by the CPU's. The action "serialize" is used to
|
||||
# serialize a memory event at the current physical time. This operation will
|
||||
# fail if the happens-before relation prevents the operation being serialized
|
||||
# at the current time.
|
||||
#
|
||||
#
|
||||
################################################################################
|
||||
|
||||
|
|
@ -101,54 +100,51 @@ module reference = {
|
|||
|
||||
########################################
|
||||
# memory events by local time
|
||||
# TODO: can we export this read-only?
|
||||
|
||||
instantiate evs(T:ltime) : memev
|
||||
|
||||
########################################
|
||||
# current global time
|
||||
|
||||
individual gt : time
|
||||
|
||||
########################################
|
||||
# global memory state
|
||||
# obeys partial function axiom
|
||||
|
||||
individual mem(A:addr) : data
|
||||
|
||||
########################################
|
||||
# event T1 prevents T2 if it must come before T2 according to the
|
||||
# ordering conditions but is not yet serialized. The definition
|
||||
# here is strong enough to imply release consistency (reads and
|
||||
# writes to different addresses commute, but nothing commutes with
|
||||
# cas)
|
||||
|
||||
derived prevents(T1,T2) =
|
||||
~evs(T1).serialized
|
||||
& T1 < T2
|
||||
& evs(T1).id_ = evs(T2).id_
|
||||
& (evs(T1).addr_ = evs(T2).addr_ | evs(T1).type_ = cas | evs(T2).type_ = cas)
|
||||
|
||||
########################################
|
||||
# serialize an event lt at current global time. The "id"
|
||||
# parameter tells us what process is serializing the event.
|
||||
#
|
||||
# This represents the state of memory after all the serialized events
|
||||
|
||||
action perform(lt:ltime, id_:id) = {
|
||||
function mem(A:addr) : data
|
||||
|
||||
# serialization must be appropriately ordered
|
||||
# assert ~prevents(T1,A1,lt,A2)
|
||||
########################################
|
||||
# Event T1 happens before T2 if it must come before T2 according to the
|
||||
# ordering constraints. This definition says that T1 happens before T2
|
||||
# if both are operations of the same CPU and if T1's locally happens before T2,
|
||||
# and if either they have the same address, or one of the two is
|
||||
# an atomic operation. The actual happens-before relation is the transitive
|
||||
# closure of happens_before.
|
||||
|
||||
# serialize at current global time
|
||||
derived happens_before(T1,T2) =
|
||||
T1 < T2
|
||||
& evs(T1).id_ = evs(T2).id_
|
||||
& (evs(T1).addr_ = evs(T2).addr_ | evs(T1).type_ = amo | evs(T2).type_ = amo)
|
||||
|
||||
# An event T1 prevents T2 if T1 happens before T2 and is not yet serialized
|
||||
|
||||
derived prevents(T1,T2) =
|
||||
~evs(T1).serialized & happens_before(T1,T2)
|
||||
|
||||
########################################
|
||||
# serialize an event lt at current global time. The "id" parameter
|
||||
# tells us what component is serializing the event. Note the
|
||||
# serializing component is not usually the originating component
|
||||
# of the event.
|
||||
|
||||
action serialize(lt:ltime, id_:id) = {
|
||||
|
||||
# Serialization must be appropriately ordered
|
||||
# That is, every event the happens before the
|
||||
# specified event lt must already be serialized
|
||||
|
||||
assert happens_before(T1,lt) -> evs(T1).serialized
|
||||
|
||||
# serialize at current physical time
|
||||
evs(lt).serialized := true;
|
||||
evs(lt).time_ := gt;
|
||||
|
||||
# advance global time
|
||||
local ngt : time {
|
||||
ngt := *;
|
||||
assume gt < ngt; # TODO: without "assume?"
|
||||
gt := ngt
|
||||
};
|
||||
|
||||
# update the global memory state
|
||||
local a : addr, d : data {
|
||||
|
|
@ -161,19 +157,27 @@ module reference = {
|
|||
if evs(lt).type_ = write {
|
||||
mem(a) := d
|
||||
}
|
||||
else { # cas operation
|
||||
else { # AMO
|
||||
# TODO: we need a specification of AMO's
|
||||
# Probably this should be a ghost module
|
||||
# The following is just a stand-in for the actual spec
|
||||
evs(lt).data_ := mem(a);
|
||||
mem(a) := d
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
delegate perform
|
||||
delegate serialize
|
||||
|
||||
########################################
|
||||
# this serializes an event by combining it with another event at
|
||||
# the same location into an atomic event. For now, we assume first
|
||||
# event is a write and second event a read.
|
||||
#
|
||||
# The fuse action would be useful, for example, to a store buffer
|
||||
# that forwards read data fron buffered writes. The read a re
|
||||
# write can be fused into an atomic operation, so we guarantee the
|
||||
# are serialized consecutively.
|
||||
|
||||
action fuse(e1:ltime, e2:ltime, s:id) = {
|
||||
|
||||
|
|
@ -194,7 +198,7 @@ module reference = {
|
|||
# This says there are no unfused events that must be ordered between e1 and e2
|
||||
|
||||
assert ~(e1 < T & T < e2 & evs(T).id_ = eid &
|
||||
(evs(T).addr_ = a | evs(T).type_ = cas) & ~evs(T).fused);
|
||||
(evs(T).addr_ = a | evs(T).type_ = amo) & ~evs(T).fused);
|
||||
|
||||
# event must not already be serialized
|
||||
|
||||
|
|
@ -301,7 +305,7 @@ module interface(ref,clnt,mngr,side) = {
|
|||
assert ref.evs(lt).data_ = d;
|
||||
assert mo = ref.evs(lt).type_;
|
||||
assert ~excl_p(a) & ~shrd_p(a); # TODO: shouldn't matter
|
||||
assert ~(ref.prevents(T1,lt) & ~to_ser(T1));
|
||||
assert ~(ref.happens_before(T1,lt) & ~ref.evs(T1).serialized & ~to_ser(T1));
|
||||
to_ser(lt) := true
|
||||
}
|
||||
}
|
||||
|
|
@ -332,7 +336,7 @@ module interface(ref,clnt,mngr,side) = {
|
|||
mixin response before clnt.response
|
||||
|
||||
########################################
|
||||
# Guarantees made on "perform" actions.
|
||||
# Guarantees made on "serialize" actions.
|
||||
#
|
||||
# We split this specification into two parts: a guarantee by
|
||||
# the client side and a guarantee by the manager side. This
|
||||
|
|
@ -342,7 +346,7 @@ module interface(ref,clnt,mngr,side) = {
|
|||
# The client side promises to serialize only events for which it
|
||||
# has the appropriate ownership state.
|
||||
|
||||
action perform_client(lt:ltime, sid:id) = {
|
||||
action serialize_client(lt:ltime, sid:id) = {
|
||||
if side(sid) = client {
|
||||
|
||||
|
||||
|
|
@ -363,8 +367,8 @@ module interface(ref,clnt,mngr,side) = {
|
|||
|
||||
assert mo = read -> excl_p(a) | shrd_p(a);
|
||||
assert mo = write -> excl_p(a);
|
||||
assert mo = cas -> excl_p(a);
|
||||
assert ~ref.prevents(T1,lt);
|
||||
assert mo = amo -> excl_p(a);
|
||||
assert ~(ref.happens_before(T1,lt) & ~ref.evs(T1).serialized);
|
||||
if mo ~= read {
|
||||
dirt_p(a) := true # if modified, mark as dirty
|
||||
}
|
||||
|
|
@ -372,12 +376,12 @@ module interface(ref,clnt,mngr,side) = {
|
|||
}
|
||||
}
|
||||
|
||||
mixin perform_client before ref.perform
|
||||
mixin serialize_client before ref.serialize
|
||||
|
||||
# The manager side promises to serialize
|
||||
# only events that have been passed by "request".
|
||||
|
||||
action perform_manager(lt:ltime, sid:id) = {
|
||||
action serialize_manager(lt:ltime, sid:id) = {
|
||||
if side(sid) = manager {
|
||||
local a:addr,d:data,mo:otype,eid:id {
|
||||
a := ref.evs(lt).addr_;
|
||||
|
|
@ -393,7 +397,7 @@ module interface(ref,clnt,mngr,side) = {
|
|||
# promises to serialize only requested events in order
|
||||
|
||||
assert to_ser(lt);
|
||||
assert ~(to_ser(T1) & ref.prevents(T1,lt))
|
||||
assert ~(to_ser(T1) & ref.happens_before(T1,lt) & ~ref.evs(T1).serialized)
|
||||
}
|
||||
|
||||
########################################
|
||||
|
|
@ -404,13 +408,13 @@ module interface(ref,clnt,mngr,side) = {
|
|||
else {
|
||||
assert mo = read -> ~excl_p(a);
|
||||
assert mo = write -> ~excl_p(a) & ~shrd_p(a);
|
||||
assert mo = cas -> ~excl_p(a) & ~shrd_p(a);
|
||||
assert ~ref.prevents(T1,lt)
|
||||
assert mo = amo -> ~excl_p(a) & ~shrd_p(a);
|
||||
assert ~(ref.happens_before(T1,lt) & ~evs(T1).serialized)
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
mixin perform_manager before ref.perform
|
||||
mixin serialize_manager before ref.serialize
|
||||
|
||||
########################################
|
||||
# Guarantees made on "fuse" actions.
|
||||
|
|
@ -446,7 +450,7 @@ module interface(ref,clnt,mngr,side) = {
|
|||
|
||||
# nothing to_ser if prevented by event not to_ser
|
||||
|
||||
conjecture ~(ref.prevents(T1,T2) & ~to_ser(T1) & to_ser(T2))
|
||||
conjecture ~(ref.happens_before(T1,T2) & ~ref.evs(T1).serialized & ~to_ser(T1) & to_ser(T2))
|
||||
|
||||
# only client side events are to_ser
|
||||
|
||||
|
|
@ -456,7 +460,7 @@ module interface(ref,clnt,mngr,side) = {
|
|||
|
||||
################################################################################
|
||||
#
|
||||
# Generic model of a client. This performs arbitrary client actions, except
|
||||
# Generic model of a client. This serializes arbitrary client actions, except
|
||||
# the it guarantees to use only ID's from the "client" side of the interface
|
||||
# as defined by its parameter "side".
|
||||
#
|
||||
|
|
@ -477,7 +481,7 @@ module generic_client(mngr,ref,side) = {
|
|||
} else if * {
|
||||
call mngr.request(a, d, mo, lt)
|
||||
} else if * {
|
||||
call ref.perform(lt,sid)
|
||||
call ref.serialize(lt,sid)
|
||||
} else {
|
||||
call ref.fuse(lt,lt1,sid)
|
||||
}
|
||||
|
|
@ -487,7 +491,7 @@ module generic_client(mngr,ref,side) = {
|
|||
|
||||
################################################################################
|
||||
#
|
||||
# Generic model of a manager. This performs arbitrary manager actions, except
|
||||
# Generic model of a manager. This serializes arbitrary manager actions, except
|
||||
# the it guarantees to use only ID's from the "manager" side of the interface
|
||||
# as defined by its parameter "side".
|
||||
#
|
||||
|
|
@ -508,7 +512,7 @@ module generic_manager(clnt,ref,side) = {
|
|||
} else if * {
|
||||
call clnt.response(a, d, mo, lt)
|
||||
} else if * {
|
||||
call ref.perform(lt,sid)
|
||||
call ref.serialize(lt,sid)
|
||||
} else {
|
||||
call ref.fuse(lt,lt1,sid)
|
||||
}
|
||||
|
|
|
|||
|
|
@ -153,7 +153,7 @@ int main(int argc, const char **argv){
|
|||
ext__c__acquire_gen cag;
|
||||
ext__c__finish_gen cfg;
|
||||
ext__c__release_gen crg;
|
||||
ext__c__perform_gen cpg;
|
||||
ext__c__serialize_gen cpg;
|
||||
ext__m__grant_gen mgg;
|
||||
ext__m__probe_gen mpg;
|
||||
|
||||
|
|
@ -171,8 +171,6 @@ int main(int argc, const char **argv){
|
|||
|
||||
int ccl = dut.cached_clients();
|
||||
for (int cl = 0; cl < 2; cl++){
|
||||
for (int a = 0; a < 4; a++)
|
||||
tb.front__cached[cl][a] = 1 ? (cl < ccl) : 0;
|
||||
for (int a = 0; a < 2; a++)
|
||||
tb.front__cached_hi[cl][a] = 1 ? (cl < ccl) : 0;
|
||||
}
|
||||
|
|
@ -379,10 +377,10 @@ int main(int argc, const char **argv){
|
|||
if (acq_send & acq_ready){
|
||||
std::cout << "output: " << acq_c << std::endl;
|
||||
if (acq_c.own == 0 && !acq_c.block){
|
||||
// TEMPORARY: treat non-block memory ops as uncached and perform them
|
||||
// TEMPORARY: treat non-block memory ops as uncached and serialize them
|
||||
// on behalf of the DUT (in principle, DUT should do this). We need a better
|
||||
// way to distinguish ops from uncached clients.
|
||||
tb.ref__perform(acq_c.ltime_,tb.buf_id);
|
||||
tb.ref__serialize(acq_c.ltime_,tb.buf_id);
|
||||
}
|
||||
tb.ext__b__acquire(acq_c.cid,acq_c.id_,acq_c.addr_hi,acq_c.word,acq_c.own,acq_c.op,acq_c.data_,acq_c.block,acq_c.ltime_);
|
||||
}
|
||||
|
|
@ -400,12 +398,12 @@ int main(int argc, const char **argv){
|
|||
// TEMPORARY: we don't know when the DUT actually
|
||||
// serializes an operation. If we get a grant for the
|
||||
// operation and it isn't serialized yet, we assume
|
||||
// the DUT has performed it internally, and serialize
|
||||
// the DUT has serializeed it internally, and serialize
|
||||
// it now. This could fail (giving us a bogus
|
||||
// assertion failure) if the DUT returns grants out of
|
||||
// order.
|
||||
tb.ref__perform(gnt_m.ltime_,tb.buf_id);
|
||||
std::cout << "performed: " << gnt_m.ltime_ << std::endl;
|
||||
tb.ref__serialize(gnt_m.ltime_,tb.buf_id);
|
||||
std::cout << "serialized: " << gnt_m.ltime_ << std::endl;
|
||||
}
|
||||
tb.ext__b__grant(gnt_m.cid,gnt_m.clnt_txid,gnt_m.mngr_txid,gnt_m.word,gnt_m.own,gnt_m.relack,gnt_m.data_,gnt_m.addr_hi,gnt_m.ltime_);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,12 +1,10 @@
|
|||
#lang ivy1.3
|
||||
#lang ivy1.5
|
||||
|
||||
################################################################################
|
||||
#
|
||||
# This is the abstract specification of the tilelink protocol. It defines
|
||||
# the consistency reference model (reference) and abstract interface protocol
|
||||
# (interface). It includes generic client and manager models for building
|
||||
# test benches.
|
||||
#
|
||||
# (interface).
|
||||
################################################################################
|
||||
|
||||
|
||||
|
|
@ -29,10 +27,6 @@ module total_order(carrier) = {
|
|||
# could add <= as derived relation here
|
||||
}
|
||||
|
||||
########################################
|
||||
# type of global time
|
||||
type time
|
||||
instantiate total_order(time)
|
||||
|
||||
########################################
|
||||
# type of local time
|
||||
|
|
@ -47,12 +41,12 @@ type data
|
|||
# type of memory addresses
|
||||
type addr
|
||||
|
||||
########################################
|
||||
# type of message types
|
||||
type mtype = { grant_t, release_t, request_t, response_t}
|
||||
|
||||
########################################
|
||||
# type of ownership state
|
||||
#
|
||||
# Note, this is the abstract ownership state associated with the
|
||||
# interface and is not necessarily the same as the cache protocol
|
||||
# state.
|
||||
type ownership = { none, shrd, excl }
|
||||
|
||||
########################################
|
||||
|
|
@ -61,14 +55,21 @@ type side = {client,manager}
|
|||
|
||||
########################################
|
||||
# type of memory ops
|
||||
type otype = {read, write, cas}
|
||||
#
|
||||
# This just gives the general class of the operation for the purposes
|
||||
# of determining the happens-before relation.
|
||||
|
||||
type otype = {read, write, amo}
|
||||
|
||||
########################################
|
||||
# id's of protocol agents
|
||||
# Global ID's of protocol components
|
||||
type id
|
||||
|
||||
########################################
|
||||
# type of client id
|
||||
#
|
||||
# ID of a client on a particular tilelink
|
||||
# interface. This is not the global id.
|
||||
type client_id
|
||||
|
||||
|
||||
|
|
@ -77,29 +78,26 @@ type client_id
|
|||
module memev = {
|
||||
individual type_ : otype
|
||||
individual addr_ : addr
|
||||
individual data_ : data # data for write and cas
|
||||
relation result(D:data) # value for read and cas
|
||||
individual data_ : data # data for write and amo
|
||||
individual id_ : id # process id of op
|
||||
relation serialized
|
||||
relation fused
|
||||
individual time_ :time # serialized time if any
|
||||
|
||||
axiom result(T) & result(U) -> T = U
|
||||
|
||||
# TEMPORARY: no atomic ops!
|
||||
init ~serialized & ~fused & type_ ~= cas
|
||||
# This is because atomic ops haven't been defined yet.
|
||||
init ~serialized & ~fused & type_ ~= amo
|
||||
}
|
||||
|
||||
################################################################################
|
||||
#
|
||||
# Reference specification
|
||||
#
|
||||
# This module describes a set of memory events ordered by local
|
||||
# time. It provides actions that assign global time to events in
|
||||
# increasing order. The pre-conditions of these actions enforce the
|
||||
# consistency model (that is, what orderings in local time must be
|
||||
# preserved in global time). This ordering condition is determined by
|
||||
# the relation "prevents" (see below).
|
||||
# This module defines the memory semantics. It contains a map from
|
||||
# local time to memory events produced by the CPU's. The action
|
||||
# "serialize" is used to serialize a memory event at the current
|
||||
# physical time. This operation will fail if the happens-before
|
||||
# relation prevents the operation being serialized at the current
|
||||
# time.
|
||||
#
|
||||
################################################################################
|
||||
|
||||
|
|
@ -111,50 +109,45 @@ module reference = {
|
|||
|
||||
instantiate evs(T:ltime) : memev
|
||||
|
||||
########################################
|
||||
# current global time
|
||||
|
||||
individual gt : time
|
||||
|
||||
########################################
|
||||
# global memory state
|
||||
# obeys partial function axiom
|
||||
|
||||
individual mem(A:addr) : data
|
||||
function mem(A:addr) : data
|
||||
|
||||
########################################
|
||||
# event T1 prevents T2 if it must come before T2 according to the
|
||||
# ordering conditions but is not yet serialized. The definition
|
||||
# here is strong enough to imply release consistency (reads and
|
||||
# writes to different addresses commute, but nothing commutes with
|
||||
# cas)
|
||||
# Event T1 happens before T2 if it must come before T2 according
|
||||
# to the ordering constraints. This definition says that T1
|
||||
# happens before T2 if both are operations of the same CPU and if
|
||||
# T1's locally happens before T2, and if either they have the same
|
||||
# address, or one of the two is an atomic operation. The actual
|
||||
# happens-before relation is the transitive closure of
|
||||
# happens_before.
|
||||
|
||||
derived prevents(T1,T2) =
|
||||
~evs(T1).serialized
|
||||
& T1 < T2
|
||||
derived happens_before(T1,T2) =
|
||||
T1 < T2
|
||||
& evs(T1).id_ = evs(T2).id_
|
||||
& (evs(T1).addr_ = evs(T2).addr_ | evs(T1).type_ = cas | evs(T2).type_ = cas)
|
||||
& (evs(T1).addr_ = evs(T2).addr_ | evs(T1).type_ = amo | evs(T2).type_ = amo)
|
||||
|
||||
# An event T1 prevents T2 if T1 happens before T2 and is not yet
|
||||
# serialized
|
||||
|
||||
derived prevents(T1,T2) =
|
||||
~evs(T1).serialized & happens_before(T1,T2)
|
||||
|
||||
|
||||
########################################
|
||||
# serialize an event lt at current global time. The "id"
|
||||
# parameter tells us what process is serializing the event.
|
||||
#
|
||||
|
||||
action perform(lt:ltime, id_:id) = {
|
||||
action serialize(lt:ltime, id_:id) = {
|
||||
|
||||
# serialization must be appropriately ordered
|
||||
# assert ~prevents(T1,A1,lt,A2)
|
||||
assert ~prevents(T1,lt);
|
||||
|
||||
# serialize at current global time
|
||||
evs(lt).serialized := true;
|
||||
# evs(lt).time_ := gt;
|
||||
|
||||
# advance global time
|
||||
# local ngt : time {
|
||||
# ngt := *;
|
||||
# assume gt < ngt; # TODO: without "assume?"
|
||||
# gt := ngt
|
||||
# };
|
||||
|
||||
# update the global memory state
|
||||
local a : addr, d : data {
|
||||
|
|
@ -167,14 +160,14 @@ module reference = {
|
|||
if evs(lt).type_ = write {
|
||||
mem(a) := d
|
||||
}
|
||||
else { # cas operation
|
||||
else { # amo operation
|
||||
evs(lt).data_ := mem(a);
|
||||
mem(a) := d
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
delegate perform
|
||||
delegate serialize # this says caller is responsible for assertions
|
||||
|
||||
########################################
|
||||
# this serializes an event by combining it with another event at
|
||||
|
|
@ -200,7 +193,7 @@ module reference = {
|
|||
# This says there are no unfused events that must be ordered between e1 and e2
|
||||
|
||||
assert ~(e1 < T & T < e2 & evs(T).id_ = eid &
|
||||
(evs(T).addr_ = a | evs(T).type_ = cas) & ~evs(T).fused);
|
||||
(evs(T).addr_ = a | evs(T).type_ = amo) & ~evs(T).fused);
|
||||
|
||||
# event must not already be serialized
|
||||
|
||||
|
|
@ -213,292 +206,7 @@ module reference = {
|
|||
evs(e2).fused := true;
|
||||
evs(e2).data_ := evs(e1).data_ # copy the data from write to read
|
||||
}
|
||||
delegate fuse
|
||||
delegate fuse # this says caller is responsible for assertions
|
||||
}
|
||||
|
||||
################################################################################
|
||||
#
|
||||
# TileLink interface specification
|
||||
#
|
||||
# This describes the semantics of the interface in relation to the reference
|
||||
# specification. The function "side" tells us whether a given process id is on
|
||||
# the client or the manager side of this interface.
|
||||
#
|
||||
################################################################################
|
||||
|
||||
module interface(ref,clnt,mngr,side,cmap) = {
|
||||
|
||||
########################################
|
||||
# client side ownership state of address
|
||||
|
||||
relation excl_p(C:client_id, A:addr) # client as exclusive priv
|
||||
relation shrd_p(C:client_id, A:addr) # client as shared priv
|
||||
relation dirt_p(C:client_id, A:addr) # client has modified data
|
||||
|
||||
########################################
|
||||
# client side events to serialize on manager side
|
||||
|
||||
relation to_ser(T:ltime)
|
||||
|
||||
########################################
|
||||
# set of cached addresses at this interface.
|
||||
# for each client
|
||||
|
||||
relation cached(C:client_id, A:addr)
|
||||
|
||||
########################################
|
||||
# initial state of interface. nothing owned, nothing to serialize
|
||||
|
||||
init ~excl_p(C,A) & ~shrd_p(C,A) & ~dirt_p(C,A) & ~to_ser(T)
|
||||
|
||||
|
||||
########################################
|
||||
# specification of release messages
|
||||
|
||||
action release(c:client_id, a:addr, d:data, o:ownership) = {
|
||||
assert cached(c,a);
|
||||
assert o ~= none;
|
||||
# cannot release priviledges you don't have
|
||||
assert o = shrd -> shrd_p(c,a);
|
||||
assert o = excl -> excl_p(c,a);
|
||||
# assert o = excl -> ref.mem(a) = d; # excl release transfers correct data
|
||||
assert ref.mem(a) = d; # all releases transfer correct data
|
||||
if o = excl {
|
||||
excl_p(c,a) := false;
|
||||
dirt_p(c,a) := false # after release the line is clean
|
||||
} else {
|
||||
shrd_p(c,a) := false
|
||||
}
|
||||
}
|
||||
mixin release before mngr.release
|
||||
|
||||
########################################
|
||||
# specification of grant messages
|
||||
|
||||
action grant(c:client_id, a:addr, d:data, o:ownership) = {
|
||||
assert cached(c,a);
|
||||
assert o ~= none;
|
||||
assert ~dirt_p(c,a) -> ref.mem(a) = d; # grant has correct data if not dirty already
|
||||
if o = excl {
|
||||
# assert ~excl_p(c,a);
|
||||
excl_p(c,a) := true
|
||||
} else {
|
||||
# assert ~shrd_p(c,a);
|
||||
shrd_p(c,a) := true
|
||||
}
|
||||
}
|
||||
mixin grant before clnt.grant
|
||||
|
||||
########################################
|
||||
# specification of request messages
|
||||
#
|
||||
# these model acquire/op. note they have ghost parameter "lt"
|
||||
# representing the local time of the event. a request has the
|
||||
# effect of marking an event to serialize on the manager side.
|
||||
# note the last assert says we must order the events on the
|
||||
# interface.
|
||||
|
||||
action request(c:client_id, a:addr, d:data, mo:otype, lt:ltime) = {
|
||||
local rid:id {
|
||||
rid := ref.evs(lt).id_;
|
||||
assert ~cached(c,a);
|
||||
assert ~ref.evs(lt).serialized & ~to_ser(lt);
|
||||
assert side(rid) = client;
|
||||
assert ref.evs(lt).addr_ = a;
|
||||
assert ref.evs(lt).data_ = d;
|
||||
assert mo = ref.evs(lt).type_;
|
||||
assert ~excl_p(c,a) & ~shrd_p(c,a); # TODO: shouldn't matter
|
||||
assert ~(ref.prevents(T1,lt) & ~to_ser(T1));
|
||||
to_ser(lt) := true
|
||||
}
|
||||
}
|
||||
mixin request before mngr.request
|
||||
|
||||
########################################
|
||||
# specification of request messages
|
||||
#
|
||||
# these model grants that respond to acquire/op. they also have
|
||||
# ghost parameter "lt" representing the local time of the event. a
|
||||
# response indicates the given event has been serialized and returns
|
||||
# the result of the operation if any.
|
||||
|
||||
action response(c:client_id, a:addr, d:data, mo:otype, lt:ltime) = {
|
||||
local rid:id {
|
||||
rid := ref.evs(lt).id_;
|
||||
|
||||
assert ~cached(c,a);
|
||||
assert side(rid) = client;
|
||||
assert ref.evs(lt).addr_ = a;
|
||||
assert ref.evs(lt).data_ = d;
|
||||
assert mo = ref.evs(lt).type_;
|
||||
assert ~excl_p(c,a) & ~shrd_p(c,a); # TODO: shouldn't matter
|
||||
assert to_ser(lt);
|
||||
assert ref.evs(lt).serialized
|
||||
}
|
||||
}
|
||||
mixin response before clnt.response
|
||||
|
||||
########################################
|
||||
# Guarantees made on "perform" actions.
|
||||
#
|
||||
# The client side promises to serialize only events for which it
|
||||
# has the appropriate ownership state. The manager side promises to serialize
|
||||
# only events that have been passed by "request".
|
||||
|
||||
action perform(lt:ltime, sid:id) = {
|
||||
local a:addr,d:data,mo:otype,eid:id {
|
||||
a := ref.evs(lt).addr_;
|
||||
d := ref.evs(lt).data_;
|
||||
mo := ref.evs(lt).type_;
|
||||
eid := ref.evs(lt).id_;
|
||||
|
||||
assert ~ref.evs(lt).serialized;
|
||||
if side(eid) = client {
|
||||
|
||||
########################################
|
||||
# client event serialized on client side. client
|
||||
# promises to serialize only with appropriate ownership
|
||||
# and in order
|
||||
|
||||
if side(sid) = client {
|
||||
assert mo = read -> excl_p(cmap(sid),a) | shrd_p(cmap(sid),a);
|
||||
assert mo = write -> excl_p(cmap(sid),a);
|
||||
assert mo = cas -> excl_p(cmap(sid),a);
|
||||
assert ~ref.prevents(T1,lt);
|
||||
if mo ~= read {
|
||||
dirt_p(cmap(sid),a) := true # if modified, mark as dirty
|
||||
}
|
||||
}
|
||||
|
||||
########################################
|
||||
# client event serialized on manager side. manager
|
||||
# promises to serialize only requested events in order
|
||||
|
||||
else {
|
||||
assert to_ser(lt);
|
||||
assert ~(to_ser(T1) & ref.prevents(T1,lt))
|
||||
}
|
||||
}
|
||||
|
||||
########################################
|
||||
# manager event serialized on manager side. manager
|
||||
# promises to serialize only events for which client does
|
||||
# not have conflicting ownership (and in order)
|
||||
|
||||
else {
|
||||
assert side(sid) = manager; # can't serialize a manager side event on client side
|
||||
assert mo = read -> ~excl_p(cmap(sid),a);
|
||||
assert mo = write -> ~excl_p(cmap(sid),a) & ~shrd_p(cmap(sid),a);
|
||||
assert mo = cas -> ~excl_p(cmap(sid),a) & ~shrd_p(cmap(sid),a);
|
||||
assert ~ref.prevents(T1,lt)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
mixin perform before ref.perform
|
||||
|
||||
########################################
|
||||
# Guarantees made on "fuse" actions.
|
||||
#
|
||||
# Fusing of a client side message is done on manager side iff
|
||||
# the read has been requested.
|
||||
|
||||
action fuse(e1:ltime, e2:ltime, sid:id) = {
|
||||
local eid : id {
|
||||
eid := ref.evs(e2).id_;
|
||||
assert side(sid) = manager <-> (to_ser(e2) | side(eid) = manager)
|
||||
}
|
||||
}
|
||||
mixin fuse before ref.fuse
|
||||
|
||||
################################################################################
|
||||
#
|
||||
# Conjectured invariants of interface state
|
||||
#
|
||||
################################################################################
|
||||
|
||||
# can only be dirty if exclusive
|
||||
|
||||
conjecture dirt_p(C,A) -> excl_p(C,A)
|
||||
|
||||
# can only have privs if cached
|
||||
|
||||
conjecture (excl_p(C,A) | shrd_p(C,A)) -> cached(C,A)
|
||||
|
||||
# to_ser only if uncached
|
||||
|
||||
# TODO: not true anymore
|
||||
# conjecture ~(to_ser(T) & cached(ref.evs(T).addr_))
|
||||
|
||||
# nothing to_ser if prevented by event not to_ser
|
||||
|
||||
conjecture ~(ref.prevents(T1,T2) & ~to_ser(T1) & to_ser(T2))
|
||||
|
||||
# only client side events are to_ser
|
||||
|
||||
conjecture to_ser(T) -> side(ref.evs(T).id_) = client
|
||||
|
||||
}
|
||||
|
||||
################################################################################
|
||||
#
|
||||
# Generic model of a client. This performs arbitrary client actions, except
|
||||
# the it guarantees to use only ID's from the "client" side of the interface
|
||||
# as defined by its parameter "side".
|
||||
#
|
||||
# TODO: should be able to generate this
|
||||
#
|
||||
################################################################################
|
||||
|
||||
module generic_client(mngr,ref,side) = {
|
||||
action response(c:client_id, a:addr, d:data, mo:otype, lt:ltime) = {
|
||||
}
|
||||
action grant(c:client_id, a:addr, d:data, o:ownership) = {
|
||||
}
|
||||
action step = {
|
||||
local c:client_id, a:addr, d:data, mo:otype, lt:ltime, o:ownership, sid:id, lt1:ltime {
|
||||
assume side(sid) = client;
|
||||
if * {
|
||||
call mngr.release(c, a, d, o)
|
||||
} else if * {
|
||||
call mngr.request(c, a, d, mo, lt)
|
||||
} else if * {
|
||||
call ref.perform(lt,sid)
|
||||
} else {
|
||||
call ref.fuse(lt,lt1,sid)
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
################################################################################
|
||||
#
|
||||
# Generic model of a manager. This performs arbitrary manager actions, except
|
||||
# the it guarantees to use only ID's from the "manager" side of the interface
|
||||
# as defined by its parameter "side".
|
||||
#
|
||||
# TODO: should be able to generate this
|
||||
#
|
||||
################################################################################
|
||||
|
||||
module generic_manager(clnt,ref,side) = {
|
||||
action request(c:client_id, a:addr, d:data, mo:otype, lt:ltime) = {
|
||||
}
|
||||
action release(c:client_id, a:addr, d:data, o:ownership) = {
|
||||
}
|
||||
action step = {
|
||||
local c:client_id, a:addr, d:data, mo:otype, lt:ltime, o:ownership, sid:id, lt1:ltime {
|
||||
assume side(sid) = manager;
|
||||
if * {
|
||||
call clnt.grant(c, a, d, o)
|
||||
} else if * {
|
||||
call clnt.response(c, a, d, mo, lt)
|
||||
} else if * {
|
||||
call ref.perform(lt,sid)
|
||||
} else {
|
||||
call ref.fuse(lt,lt1,sid)
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
#lang ivy1.3
|
||||
#lang ivy1.5
|
||||
|
||||
################################################################################
|
||||
#
|
||||
|
|
@ -98,9 +98,9 @@ module tl_generic_client_gen(mngr,ref,side) = {
|
|||
|
||||
instantiate generic_client_intf(mngr)
|
||||
|
||||
action perform(lt:ltime, sid:id) = {
|
||||
action serialize(lt:ltime, sid:id) = {
|
||||
assume side(sid) = client;
|
||||
call ref.perform(lt,sid)
|
||||
call ref.serialize(lt,sid)
|
||||
}
|
||||
|
||||
action fuse(lt:ltime, lt1:ltime, sid:id) = {
|
||||
|
|
@ -174,9 +174,9 @@ module tl_generic_manager_gen(clnt,ref,side) = {
|
|||
|
||||
instantiate generic_manager_intf(clnt)
|
||||
|
||||
action perform(lt:ltime, sid:id) = {
|
||||
action serialize(lt:ltime, sid:id) = {
|
||||
assume side(sid) = manager;
|
||||
call ref.perform(lt,sid)
|
||||
call ref.serialize(lt,sid)
|
||||
}
|
||||
|
||||
action fuse(lt:ltime, lt1:ltime, sid:id) = {
|
||||
|
|
@ -209,7 +209,7 @@ instantiate m : tl_generic_manager_gen(b,ref,bside)
|
|||
export c.acquire
|
||||
export c.finish
|
||||
export c.release
|
||||
export c.perform
|
||||
export c.serialize
|
||||
export m.grant
|
||||
export m.probe
|
||||
export b.acquire
|
||||
|
|
@ -335,7 +335,6 @@ rely front_prb_rdy_io
|
|||
#
|
||||
################################################################################
|
||||
|
||||
interpret time -> bv[2]
|
||||
interpret ltime -> bv[2]
|
||||
interpret data -> {0..1}
|
||||
interpret addr -> {0..3}
|
||||
|
|
|
|||
|
|
@ -1,13 +1,10 @@
|
|||
#lang ivy1.3
|
||||
#lang ivy1.5
|
||||
|
||||
################################################################################
|
||||
#
|
||||
# This is a (more) concrete specification of the tilelink protocol. It specifies
|
||||
# the low-level messages with reference to the abstract spec.
|
||||
#
|
||||
# The concrete model introduces Acquire and Finish messages, requester ID's,
|
||||
# and other fields that indicate the address range to operate on, and so on.
|
||||
#
|
||||
################################################################################
|
||||
|
||||
|
||||
|
|
@ -155,35 +152,45 @@ module prb = {
|
|||
type prb_id
|
||||
instantiate prbs(X:prb_id) : prb
|
||||
|
||||
########################################
|
||||
# Stub actions for mixins
|
||||
|
||||
module interface_stubs = {
|
||||
action release(c:client_id, a:addr, d:data, o:ownership) = {}
|
||||
action grant(c:client_id, a:addr, d:data, o:ownership) = {}
|
||||
action request(c:client_id, a:addr, d:data, mo:otype, lt:ltime) = {}
|
||||
action response(c:client_id, a:addr, d:data, mo:otype, lt:ltime) = {}
|
||||
}
|
||||
|
||||
|
||||
################################################################################
|
||||
#
|
||||
# This module describes the TileLink interface. It uses mixins to specify the
|
||||
# interaction between a client (clnt) a manager (mngr) and a reference model (ref).
|
||||
# The funciton "side" tells us, for each component ID, which side of the interface
|
||||
# The function "side" tells us, for each component ID, which side of the interface
|
||||
# the component is on ("client" or "manager").
|
||||
#
|
||||
################################################################################
|
||||
|
||||
module tl_interface(ref,clnt,mngr,side,cmap) = {
|
||||
|
||||
########################################
|
||||
# client side ownership state of address
|
||||
#
|
||||
# Ownership status is by address, not by cache line. This is
|
||||
# because we need to be able to serialize an operation on the
|
||||
# critical word when it arrives, and not wait for the whole cache
|
||||
# line to be granted.
|
||||
|
||||
relation excl_p(C:client_id, A:addr) # client as exclusive priv
|
||||
relation shrd_p(C:client_id, A:addr) # client as shared priv
|
||||
relation dirt_p(C:client_id, A:addr) # client has modified data
|
||||
|
||||
########################################
|
||||
# client side events to serialize on manager side
|
||||
#
|
||||
# An event is added to "to_ser" when the corresponding
|
||||
# non-cached acquire occurs.
|
||||
|
||||
relation to_ser(T:ltime)
|
||||
|
||||
########################################
|
||||
# whether a line is cached by given client
|
||||
|
||||
relation cached_hi(C:client_id,X:tl_addrhi)
|
||||
|
||||
########################################
|
||||
# if true, this interface does not allowed reordering of messages
|
||||
# if true, this interface does not allow reordering of messages
|
||||
|
||||
relation ordered
|
||||
|
||||
|
|
@ -199,7 +206,7 @@ module tl_interface(ref,clnt,mngr,side,cmap) = {
|
|||
# of the three phases, for each type: exclusive, shared and uncached.
|
||||
#
|
||||
# Note, this is cache protcol dependent. We might want to parameterize
|
||||
# this on an arbitraru set of possible cache line priviledges.
|
||||
# this on an arbitrary set of possible cache line priviledges.
|
||||
|
||||
relation excl_r(C:client_id,A:tl_addrhi) # there is a requested excl acquire for line
|
||||
relation shrd_r(C:client_id,A:tl_addrhi) # there is a requested shrd acquire for line
|
||||
|
|
@ -277,6 +284,11 @@ module tl_interface(ref,clnt,mngr,side,cmap) = {
|
|||
########################################
|
||||
# Initial condition of interface
|
||||
#
|
||||
|
||||
# Nothing is owned, nothing to serialize
|
||||
|
||||
init ~excl_p(C,A) & ~shrd_p(C,A) & ~dirt_p(C,A) & ~to_ser(T)
|
||||
|
||||
# Nothing is requested, accepted, finished or granted.
|
||||
|
||||
init ~excl_r(C,H) & ~shrd_r(C,H) & ~unc_r(C,H,W)
|
||||
|
|
@ -328,7 +340,7 @@ module tl_interface(ref,clnt,mngr,side,cmap) = {
|
|||
# which would be violated by reordering lock operations.
|
||||
|
||||
assert ~(to_ser(E) & ~granted(E) &
|
||||
(ref.evs(E).type_ = cas | ref.evs(lt).type_ = cas)
|
||||
(ref.evs(E).type_ = amo | ref.evs(lt).type_ = amo)
|
||||
& ref.evs(E).id_ = ref.evs(lt).id_);
|
||||
|
||||
# (5) No two operations request or accepted on same address for the same
|
||||
|
|
@ -358,7 +370,7 @@ module tl_interface(ref,clnt,mngr,side,cmap) = {
|
|||
|
||||
# TODO: HACK: some components do not support PutAtomic
|
||||
|
||||
assert o = cas -> supports_uncached_atomic;
|
||||
assert o = amo -> supports_uncached_atomic;
|
||||
|
||||
########################################
|
||||
# mark the acquire as requested
|
||||
|
|
@ -374,7 +386,18 @@ module tl_interface(ref,clnt,mngr,side,cmap) = {
|
|||
# Perform abstract operation
|
||||
#
|
||||
|
||||
call abs.request(c,addr_cons(hi,lo),d,o,lt)
|
||||
local rid:id, a:addr {
|
||||
rid := ref.evs(lt).id_;
|
||||
a := addr_cons(hi,lo);
|
||||
assert ~ref.evs(lt).serialized & ~to_ser(lt);
|
||||
assert side(rid) = client;
|
||||
assert ref.evs(lt).addr_ = a;
|
||||
assert ref.evs(lt).data_ = d;
|
||||
assert o = ref.evs(lt).type_;
|
||||
assert ~excl_p(c,a) & ~shrd_p(c,a); # TODO: shouldn't matter
|
||||
assert ~(ref.prevents(T1,lt) & ~to_ser(T1));
|
||||
to_ser(lt) := true
|
||||
}
|
||||
}
|
||||
|
||||
else {
|
||||
|
|
@ -443,7 +466,7 @@ module tl_interface(ref,clnt,mngr,side,cmap) = {
|
|||
# specification of Grant message
|
||||
|
||||
action tl_Grant(msg:gnt_id) = {
|
||||
local c:client_id, hi:tl_addrhi, lo:tl_addrlo, c_txid: id, m_txid: id, reqt:time, maddr:addr, ow:ownership, lt:ltime {
|
||||
local c:client_id, hi:tl_addrhi, lo:tl_addrlo, c_txid: id, m_txid: id, maddr:addr, ow:ownership, lt:ltime {
|
||||
|
||||
c := gnts(msg).cid;
|
||||
hi := gnts(msg).addr_hi; # this field is aux
|
||||
|
|
@ -588,8 +611,14 @@ module tl_interface(ref,clnt,mngr,side,cmap) = {
|
|||
########################################
|
||||
# Abstract semantics of grant
|
||||
|
||||
if ow ~= none { # cached: perform an abstract grant
|
||||
call abs.grant(c,maddr,gnts(msg).data_,ow);
|
||||
if ow ~= none { # cached: perform an abstract grant
|
||||
# grant has correct data if not dirty already
|
||||
assert ~dirt_p(c,maddr) -> ref.mem(maddr) = gnts(msg).data_;
|
||||
if ow = excl {
|
||||
excl_p(c,maddr) := true
|
||||
} else {
|
||||
shrd_p(c,maddr) := true
|
||||
};
|
||||
|
||||
g_beats(lo) := false; # mark the beat completed
|
||||
|
||||
|
|
@ -607,7 +636,15 @@ module tl_interface(ref,clnt,mngr,side,cmap) = {
|
|||
}
|
||||
|
||||
else { # uncached: perform an abstract response
|
||||
call abs.response(c,maddr,gnts(msg).data_,ref.evs(lt).type_,lt);
|
||||
local rid:id {
|
||||
rid := ref.evs(lt).id_;
|
||||
assert side(rid) = client;
|
||||
assert ref.evs(lt).addr_ = maddr;
|
||||
assert ref.evs(lt).data_ = gnts(msg).data_;
|
||||
assert ~excl_p(c,maddr) & ~shrd_p(c,maddr); # TODO: shouldn't matter
|
||||
assert to_ser(lt);
|
||||
assert ref.evs(lt).serialized
|
||||
};
|
||||
granted(gnts(msg).ltime_) := true
|
||||
}
|
||||
}
|
||||
|
|
@ -791,18 +828,19 @@ module tl_interface(ref,clnt,mngr,side,cmap) = {
|
|||
|
||||
if rlss(msg).dirty {
|
||||
if excl_p(c,a) {
|
||||
call abs.release(c,a,d,excl)
|
||||
assert ref.mem(a) = d; # correct data
|
||||
excl_p(c,a) := false;
|
||||
dirt_p(c,a) := false # clean after relase
|
||||
};
|
||||
if shrd_p(c,a) {
|
||||
call abs.release(c,a,d,shrd)
|
||||
}
|
||||
assert ref.mem(a) = d; # correct data
|
||||
shrd_p(c,a) := false
|
||||
}
|
||||
}
|
||||
else {
|
||||
# TRICKY: to invalidate the entire block we go outside of EPR
|
||||
# We need inverse functions for addr_cons, but Ivy doesn't
|
||||
# support this yet. Also, we don't call the abstract spec here
|
||||
# because it doesn't support releasing a set of addresses (yet).
|
||||
|
||||
# support this yet.
|
||||
excl_p(c,A) := excl_p(c,A) & ~exists W:tl_addrlo. (A = addr_cons(hi,W));
|
||||
shrd_p(c,A) := shrd_p(c,A) & ~exists W:tl_addrlo. (A = addr_cons(hi,W))
|
||||
}
|
||||
|
|
@ -845,23 +883,81 @@ module tl_interface(ref,clnt,mngr,side,cmap) = {
|
|||
}
|
||||
mixin tl_Probe before clnt.tl_Probe
|
||||
|
||||
|
||||
########################################
|
||||
#
|
||||
# Instantiate the abstract interface specification
|
||||
# Guarantees made on "serialize" actions.
|
||||
#
|
||||
########################################
|
||||
# The client side promises to serialize only events for which it
|
||||
# has the appropriate ownership state. The manager side promises to serialize
|
||||
# only events that have been passed by "request".
|
||||
|
||||
action serialize(lt:ltime, sid:id) = {
|
||||
local a:addr,d:data,mo:otype,eid:id {
|
||||
a := ref.evs(lt).addr_;
|
||||
d := ref.evs(lt).data_;
|
||||
mo := ref.evs(lt).type_;
|
||||
eid := ref.evs(lt).id_;
|
||||
|
||||
instantiate abs : interface_stubs
|
||||
instantiate interface(ref,abs,abs,side,cmap)
|
||||
assert ~ref.evs(lt).serialized;
|
||||
if side(eid) = client {
|
||||
|
||||
########################################
|
||||
# client event serialized on client side. client
|
||||
# promises to serialize only with appropriate ownership
|
||||
# and in order
|
||||
|
||||
if side(sid) = client {
|
||||
assert mo = read -> excl_p(cmap(sid),a) | shrd_p(cmap(sid),a);
|
||||
assert mo = write -> excl_p(cmap(sid),a);
|
||||
assert mo = amo -> excl_p(cmap(sid),a);
|
||||
assert ~ref.prevents(T1,lt);
|
||||
if mo ~= read {
|
||||
dirt_p(cmap(sid),a) := true # if modified, mark as dirty
|
||||
}
|
||||
}
|
||||
|
||||
########################################
|
||||
# client event serialized on manager side. manager
|
||||
# promises to serialize only requested events in order
|
||||
|
||||
else {
|
||||
assert to_ser(lt);
|
||||
assert ~(to_ser(T1) & ref.prevents(T1,lt))
|
||||
}
|
||||
}
|
||||
|
||||
########################################
|
||||
# manager event serialized on manager side. manager
|
||||
# promises to serialize only events for which client does
|
||||
# not have conflicting ownership (and in order)
|
||||
|
||||
else {
|
||||
assert side(sid) = manager; # can't serialize a manager side event on client side
|
||||
assert mo = read -> ~excl_p(cmap(sid),a);
|
||||
assert mo = write -> ~excl_p(cmap(sid),a) & ~shrd_p(cmap(sid),a);
|
||||
assert mo = amo -> ~excl_p(cmap(sid),a) & ~shrd_p(cmap(sid),a);
|
||||
assert ~ref.prevents(T1,lt)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
mixin serialize before ref.serialize
|
||||
|
||||
########################################
|
||||
#
|
||||
# All or none of a line is cached
|
||||
# Guarantees made on "fuse" actions.
|
||||
#
|
||||
########################################
|
||||
# Fusing of a client side message is done on manager side iff
|
||||
# the read has been requested.
|
||||
|
||||
action fuse(e1:ltime, e2:ltime, sid:id) = {
|
||||
local eid : id {
|
||||
eid := ref.evs(e2).id_;
|
||||
assert side(sid) = manager <-> (to_ser(e2) | side(eid) = manager)
|
||||
}
|
||||
}
|
||||
mixin fuse before ref.fuse
|
||||
|
||||
|
||||
axiom cached(C,addr_cons(H,L)) <-> cached_hi(C,H)
|
||||
|
||||
|
||||
################################################################################
|
||||
|
|
@ -870,6 +966,22 @@ module tl_interface(ref,clnt,mngr,side,cmap) = {
|
|||
#
|
||||
################################################################################
|
||||
|
||||
# can only be dirty if exclusive
|
||||
|
||||
conjecture dirt_p(C,A) -> excl_p(C,A)
|
||||
|
||||
# can only have privs if cached
|
||||
|
||||
conjecture (excl_p(C,A) | shrd_p(C,A)) & A = addr_cons(H,L) -> cached_hi(C,H)
|
||||
|
||||
# nothing to_ser if prevented by event not to_ser
|
||||
|
||||
conjecture ~(ref.prevents(T1,T2) & ~to_ser(T1) & to_ser(T2))
|
||||
|
||||
# only client side events are to_ser
|
||||
|
||||
conjecture to_ser(T) -> side(ref.evs(T).id_) = client
|
||||
|
||||
# A cached acquire must be in cached space, uncached in uncached space
|
||||
|
||||
conjecture (excl_r(C,H) | excl_a(C,H) | excl_f(C,H) |
|
||||
|
|
@ -942,7 +1054,7 @@ module tl_interface(ref,clnt,mngr,side,cmap) = {
|
|||
|
||||
conjecture ~(to_ser(E1) & to_ser(E2) & ~granted(E1) & ~granted(E2) & E1 ~= E2 &
|
||||
ref.evs(E1).id_ = ref.evs(E2).id_
|
||||
& (ref.evs(E1).type_ = cas | ref.evs(E1).type_ = cas))
|
||||
& (ref.evs(E1).type_ = amo | ref.evs(E1).type_ = amo))
|
||||
|
||||
# (5) No two operations pending on same address for the same
|
||||
# client. This is required for release consistency,
|
||||
|
|
@ -1012,9 +1124,9 @@ module tl_generic_client(mngr,ref,side) = {
|
|||
action release(f:rls_id) = {
|
||||
call mngr.tl_Release(f)
|
||||
}
|
||||
action perform(lt:ltime, sid:id) = {
|
||||
action serialize(lt:ltime, sid:id) = {
|
||||
assume side(sid) = client;
|
||||
call ref.perform(lt,sid)
|
||||
call ref.serialize(lt,sid)
|
||||
}
|
||||
|
||||
action fuse(lt:ltime, lt1:ltime, sid:id) = {
|
||||
|
|
@ -1033,7 +1145,7 @@ module tl_generic_client(mngr,ref,side) = {
|
|||
} else if * {
|
||||
call release(r)
|
||||
} else if * {
|
||||
call perform(lt,sid)
|
||||
call serialize(lt,sid)
|
||||
} else {
|
||||
call fuse(lt,lt1,sid)
|
||||
}
|
||||
|
|
@ -1067,9 +1179,9 @@ module tl_generic_manager(clnt,ref,side) = {
|
|||
call clnt.tl_Probe(g)
|
||||
}
|
||||
|
||||
action perform(lt:ltime, sid:id) = {
|
||||
action serialize(lt:ltime, sid:id) = {
|
||||
assume side(sid) = manager;
|
||||
call ref.perform(lt,sid)
|
||||
call ref.serialize(lt,sid)
|
||||
}
|
||||
|
||||
action fuse(lt:ltime, lt1:ltime, sid:id) = {
|
||||
|
|
@ -1084,7 +1196,7 @@ module tl_generic_manager(clnt,ref,side) = {
|
|||
} else if * {
|
||||
call probe(p)
|
||||
} else if * {
|
||||
call perform(lt,sid)
|
||||
call serialize(lt,sid)
|
||||
} else {
|
||||
call fuse(lt,lt1,sid)
|
||||
}
|
||||
|
|
@ -1239,7 +1351,7 @@ module tl_mm_interface(ref,clnt,mngr,side) = {
|
|||
# specification of Grant message
|
||||
|
||||
action tl_Grant(msg:gnt_id) = {
|
||||
local hi:tl_addrhi, lo:tl_addrlo, c_txid: id, m_txid: id, reqt:time, maddr:addr, ow:ownership, lt:ltime {
|
||||
local hi:tl_addrhi, lo:tl_addrlo, c_txid: id, m_txid: id, maddr:addr, ow:ownership, lt:ltime {
|
||||
|
||||
hi := gnts(msg).addr_hi; # this field is aux
|
||||
lo := gnts(msg).word;
|
||||
|
|
@ -1357,9 +1469,9 @@ module tl_mm_interface(ref,clnt,mngr,side) = {
|
|||
mixin tl_Probe before clnt.tl_Probe
|
||||
|
||||
########################################
|
||||
# specification of perform (serialization)
|
||||
# specification of serialize (serialization)
|
||||
|
||||
action perform(lt:ltime, sid:id) = {
|
||||
action serialize(lt:ltime, sid:id) = {
|
||||
|
||||
# nothing can be serialized on the manager (main memory) side
|
||||
# serializing write or atomic dirties the address
|
||||
|
|
@ -1376,5 +1488,5 @@ module tl_mm_interface(ref,clnt,mngr,side) = {
|
|||
}
|
||||
}
|
||||
}
|
||||
mixin perform before ref.perform
|
||||
mixin serialize before ref.serialize
|
||||
}
|
||||
|
|
|
|||
Загрузка…
Ссылка в новой задаче