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.

Oustanding issues:

Managers must include an up-to-date copy of the data in Grants responding to Acquires upgrading permissions unless they are certain that client has not been Probed since the Aquire was issued.

Todo

currently the spec requires all Grants to have data, even in the upgrade case.

Todo

We do not allow the same txid to be used for simultaneous transactions even if they differe in type (for example, cached and uncached). This can be relaxed if needed.

Todo

We allow a probe to be handled in the middle of a voluntary release, so that some beats are voluntary ans some involuntary. This could be made mode strict.

Todo

BroadcastHub does not support PutAtomic

include tilelink_abstract_spec

address high and low-order bits

type tl_addrhi
type tl_addrlo

order relation on beats

relation (X:tl_addrlo <= Y:tl_addrlo)

construct adresses from high- and low-order bits

individual addr_cons(X:tl_addrhi,Y:tl_addrlo) : addr

address constructor is an injection

axiom addr_cons(X1,Y1) = addr_cons(X2,Y2) -> X1=X2 & Y1=Y2

Message formats. The message contain auxiliary fields that are used in the specification, but are not physically present. These are labeled "aux".

structure representing Acquire message

module acq = {
    individual cid : client_id        # client id
    individual id_ : id               # client txid
    individual addr_hi : tl_addrhi    # hi order bits of address
    individual word : tl_addrlo       # requested word if uncached
    individual own:ownership          # what ownership type? (none=uncached)
    individual op : otype             # what operation?
    individual data_ : data           # what data, if any?
    relation block                    # true if full block read or write

    individual ltime_ : ltime         # (aux) logical time
}

Heap of acquire messages

type acq_id
instantiate acqs(X:acq_id) : acq

structure representing Grant message

module gnt = {
    individual cid : client_id        # client id
    individual clnt_txid : id         # client side transaction id
    individual mngr_txid : id         # manager side transaction id
    individual word : tl_addrlo       # low-order bits of this response
    individual own:ownership          # what ownership type? (none = uncached)
    relation relack                   # is this an ack of a Release?
    individual data_ : data           # return value, if any

    individual addr_hi : tl_addrhi    # (aux) hi order bits of address
    individual ltime_ : ltime         # (aux) logical time
}

Heap of grant messages

type gnt_id
instantiate gnts(X:gnt_id) : gnt

structure representing Finish message

module fns = {
    individual cid : client_id        # client id (aux?)
    individual id_ : id               # manager transaction id

    individual addr_hi : tl_addrhi    # (aux) hi order bits of acquire
    individual word : tl_addrlo       # (aux) low-order bits of acquire
    individual own:ownership          # (aux) ownership or acquire
}

Heap of finish messages

type fns_id
instantiate fnss(X:fns_id) : fns

structure representing Release message

module rls = {
    individual cid : client_id      # client id
    individual id_ : id             # client transaction id
    relation voluntary              # is this a voluntary release?
    individual addr_hi : tl_addrhi  # hi order bits of address
    individual word :tl_addrlo      # word being released
    relation dirty                  # is data modified?
    individual data_ : data         # data, if dirty
}

Heap of release messages

type rls_id
instantiate rlss(X:rls_id) : rls

structure representing probe message

module prb = {
    individual cid : client_id      # client id
    individual id_ : id             # txid (is this used?)
    individual addr_hi : tl_addrhi  # hi order bits of address
}

Heap of probe messages

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 component is on ("client" or "manager").

module tl_interface(ref,clnt,mngr,side,cmap) = {

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

    relation ordered

if true, this interface supports PutAtomic messages

    relation supports_uncached_atomic

An Acquire has three phases: requested, accepted and finishing

These predicates keep track of whether there is an acquire in one 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.

    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
    relation unc_r(C:client_id,A:tl_addrhi,W:tl_addrlo)    # there is a requested uncached acquire

    relation excl_a(C:client_id,A:tl_addrhi)               # there is an accepted excl acquire for line
    relation shrd_a(C:client_id,A:tl_addrhi)               # there is an accepted shrd acquire for line
    relation unc_a(C:client_id,A:tl_addrhi,W:tl_addrlo)    # there is an accepted uncached acquire

    relation excl_f(C:client_id,A:tl_addrhi)               # there is an finishing excl acquire for line
    relation shrd_f(C:client_id,A:tl_addrhi)               # there is an finishing shrd acquire for line
    relation unc_f(C:client_id,A:tl_addrhi,W:tl_addrlo)    # there is an finishing uncached acquire

Release messages

A voluntary Release message is considered to be requested from the time it is transmitted until the time its Grant has been transmitted. This predicate tracks which addresses have releases requested (none = no priviledges).

    relation none_r(C:client_id,A:tl_addrhi,W:tl_addrlo)

Probe messages

A word of a Probe message is considered to be requested from the time the Probe is transmitted until the time the corresponding involuntary Release is transmitted. This predicate tracks the addresses that have probes requested.

    relation prb_addr(C:client_id,H:tl_addrhi, W:tl_addrlo)

granted events

A memory event E (see the reference model) has been granted if a corresponding uncached Acquire has been granted. This predicate tracks the granted events.

    relation granted(E:ltime)

Each Acquire has a transaction ID (txid). This map tracks the txid associated with requested acquires for a given hi address. It is a protocol invariant that there is at most one such txid.

    individual addr_rid(C:client_id,H:tl_addrhi) : id

Each Grant has a transaction ID (txid). This map tracks the txid associated with grants for a given hi address. It is a protocol invariant that there is at most one such txid.

    individual addr_gid(C:client_id,H:tl_addrhi) : id

Each voluntary Release has a transaction ID (txid). This map tracks the txid associated with voluntary Releases for a given hi address. It is a protocol invariant that there is at most one such txid.

    individual addr_nid(C:client_id,H:tl_addrhi) : id

The set of outstanding Grant data beats

    relation g_beats(W:tl_addrlo)

Initial condition of interface

Nothing is requested, accepted, finished or granted.

    init    ~excl_r(C,H) & ~shrd_r(C,H) & ~unc_r(C,H,W)
          & ~excl_a(C,H) & ~shrd_a(C,H) & ~unc_a(C,H,W)
          & ~excl_f(C,H) & ~shrd_f(C,H) & ~unc_f(C,H,W)
      & ~none_r(C,H,W) & ~prb_addr(C,H,W) & ~granted(E)

specification of Acquire message

    action tl_Acquire(msg:acq_id) = {

        local c:client_id, hi:tl_addrhi, lo:tl_addrlo, txid: id, ow:ownership, lt:ltime, a:addr, d:data, o:otype {

        c := acqs(msg).cid;
        ow := acqs(msg).own;
        hi := acqs(msg).addr_hi;
        lo := acqs(msg).word;
        txid := acqs(msg).id_;
        lt := acqs(msg).ltime_;
        a := addr_cons(hi,lo);
        d := acqs(msg).data_;
        o := acqs(msg).op;


        if acqs(msg).own = none {

rules for uncached Acquires

(1) May not have a requested acquire with same hi address and word.

        assert ~unc_r(c,hi,lo);

(2) if any requested or accepted transactions with same hi address, txid must match

        assert unc_r(c,hi,W) -> addr_rid(c,hi) = txid;
        assert unc_a(c,hi,W) -> addr_rid(c,hi) = txid;

(3) May not use a txid in use by a requested tx with a different hi addr

        assert (unc_r(c,H,W) | excl_r(c,H) | shrd_r(c,H)) & H ~= hi -> addr_rid(c,H) ~= txid;

(4) No two lock operations can be requested or accept for the same client. This is required for release consistency, 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).id_ = ref.evs(lt).id_);

(5) No two operations request or accepted on same address for the same client. This is required for release consistency, which would be violated by reordering ops on same address. TODO: no client ID's yet

        assert ~(to_ser(E) & ~granted(E)
                         & ref.evs(E).addr_ = ref.evs(lt).addr_
             & ref.evs(E).id_ = ref.evs(lt).id_);

(6) All preventing events are already granted. This is to maintain consistency with unordered channels.

        assert ref.prevents(E,lt) -> granted(E);

(7) Must have correct address, data and op for associated memory event.

        assert addr_cons(hi,lo) = ref.evs(lt).addr_
               & d = ref.evs(lt).data_
               & o = ref.evs(lt).type_;

(8) Must be in uncached address space

        assert ~cached_hi(c,hi);

TODO: HACK: some components do not support PutAtomic

        assert o = cas -> supports_uncached_atomic;

mark the acquire as requested

        unc_r(c,hi,lo) := true;

Associate the address and txid

            addr_rid(c,hi) := txid;

Perform abstract operation

        call abs.request(c,addr_cons(hi,lo),d,o,lt)
        }

        else {

rules for cached Acquires

(1) May not have pending acquire with same ID and ownership and with same hi addr. We can, however, have more than one ownership request in same transaction.

        assert ow = excl -> ~excl_r(c,hi) & ~excl_a(c,hi);
        assert ow = shrd -> ~shrd_r(c,hi) & ~shrd_a(c,hi);

(2) if any requested or accepted transactions with same hi address, txid must match. However, once a prior re4quest is granted, a new txid may be used.

        assert (excl_r(c,hi) | shrd_r(c,hi)) -> addr_rid(c,hi) = txid;
        assert (excl_a(c,hi) | shrd_a(c,hi)) -> addr_rid(c,hi) = txid;

(3) May not use a txid in use by a requested or accepted acquire for a different hi addr

        assert (unc_r(c,H,W) | excl_r(c,H) | shrd_r(c,H) | unc_a(c,H,W) | excl_a(c,H) | shrd_a(c,H)) & H ~= hi -> addr_rid(c,H) ~= txid;

(4) May not have a pending release with same hi addr.

        assert ~none_r(c,hi,W);

(5) No acquires for privs we already have, unless probe requested If a probe is requested, however, the release may be delayed until after a new acquire.

        assert ow = excl & ~prb_addr(c,hi,W) -> ~excl_p(c,addr_cons(hi,W));
        assert ow = shrd & ~prb_addr(c,hi,W) -> ~shrd_p(c,addr_cons(hi,W));

(6) Must be in cached address space.

        assert cached_hi(c,hi);

mark the acquire as requested

        if ow = excl {
            excl_r(c,hi) := true
        };
        if ow = shrd {
            shrd_r(c,hi) := true
        };

Associate the address and txid

            addr_rid(c,hi) := txid

        }

        }
    }
    mixin tl_Acquire before mngr.tl_Acquire

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 {

        c :=  gnts(msg).cid;
        hi := gnts(msg).addr_hi;  # this field is aux
        lo := gnts(msg).word;
        c_txid := gnts(msg).clnt_txid;
        m_txid := gnts(msg).mngr_txid;
        ow := gnts(msg).own;
        lt := gnts(msg).ltime_;
        maddr := addr_cons(hi,lo);                             # construct full address


        if gnts(msg).relack {

A release ack marks the matching Release as completed

Rules for Release acks:

(1) A release ack implies a requested release of all words in the block.

        assert none_r(c,hi,X);

(2) Cannot ack a release if there is an accepted or finishing Acquire for the same hi address. The ack must wait for for Finish.

Todo

allowing this to see what happens assert ~excl_a(c,hi) & ~shrd_a(c,hi) & ~excl_f(c,hi) & ~shrd_f(c,hi);

(3) A release acks txid must match the request

        assert addr_nid(c,hi) = c_txid;

mark the release finished

        none_r(c,hi,X) := false

            }
            else {

TEMPORARY: fix ownership type if it's wrong

        if exists C:client_id, H:tl_addrhi. excl_a(C:client_id,H:tl_addrhi) {
           ow := excl
                };

Rules for normal Grants:

(1) A Grant must match a requested or accepted Acquire. A shared Acquire can be matched by an exclusive Grant.

        assert ow = none -> (unc_r(c,hi,lo) | unc_a(c,hi,lo));
        assert ow = excl -> (excl_r(c,hi) | excl_a(c,hi) | shrd_r(c,hi));
        assert ow = shrd -> (shrd_r(c,hi) | shrd_a(c,hi));

(2) Cannot grant if the memory event is already granted

        assert ow = none -> ~granted(lt);

(3) Cannot grant if there is a pending probe with the same hi address.

        assert ~prb_addr(c,hi,W);

(4) Uncached grant must match memory event, which must be to_ser and serialized.

        assert ow = none -> maddr = ref.evs(lt).addr_ & to_ser(lt) & ref.evs(lt).serialized;

(5) A grant's txid must match its request

        assert addr_rid(c,hi) = c_txid;

(6) Cannot use a manager-side txid if already in use for a different hi address

        assert ~((excl_a(c,H) | excl_f(c,H) | shrd_a(c,H) | shrd_f(c,H) | unc_a(c,H,W) | unc_f(c,H,W))
                 & addr_gid(c,H) = m_txid & H ~= hi);

(7) Cannot use two different manager-side txid's for same hi address.

        assert ~((excl_a(c,H) | excl_f(c,H) | shrd_a(c,H) | shrd_f(c,H) | unc_a(c,H,W) | unc_f(c,H,W))
                 & addr_gid(c,H) ~= m_txid & H = hi);

(8) Cannot grant a request that exactly matches one in progress.

        assert ow = none -> ~unc_a(c,hi,lo) & ~unc_f(c,hi,lo);

(9) If a grant is in progress, this must be an outstanding beat of that grant.

        assert excl_a(C,H) -> ow = excl & C = c & H = hi & g_beats(lo);
        assert shrd_a(C,H) -> ow = shrd & C = c & H = hi & g_beats(lo);
        assert unc_a(C,H,W) -> ow = none & C = c & H = hi & unc_a(c,hi,lo);

If uncached, mark the event granted. If the request is not part of an accepted transaction, move the request to accepted.

If only a share privs are requested, but an exclusive grant is received, we upgrade the shared request to exclusive

Todo

for no, uncached acquire are only one beat, so can never be in accepted state.

        if ow = none {
            unc_r(c,hi,lo) := false;
            unc_f(c,hi,lo) := true  # for now, can't be in accepted state
        }
        else if ow = excl {
            if ~excl_a(c,hi) {
                if excl_r(c,hi) {
                            excl_r(c,hi) := false
                        } else {  # answering a shared acquire with exclusive
                shrd_r(c,hi) := false
                        };
                excl_a(c,hi) := true;
            g_beats(W) := W ~= lo  # record pending beats
            }
                }
        else if ow = shrd {
            if ~shrd_a(c,hi) {
                shrd_r(c,hi) := false;
            shrd_a(c,hi) := true;
            g_beats(W) := W ~= lo  # record pending beats
            }
                };

If we are accepting a new uncached transaction, this associates the new txid with the address for accepted transactions.

            addr_gid(c,hi) := m_txid;

Abstract semantics of grant

        if ow ~= none {                            # cached: perform an abstract grant
            call abs.grant(c,maddr,gnts(msg).data_,ow);

            g_beats(lo) := false;                       # mark the beat completed

if all beats received, move to finishing

            if forall W:tl_addrlo. ow = excl & ~g_beats(W:tl_addrlo) {
                excl_a(c,hi) := false;
            excl_f(c,hi) := true
                    };

if all shrd privs obtained, move to finishing

            if forall W:tl_addrlo. ow = shrd &  ~g_beats(W:tl_addrlo) {
                shrd_a(c,hi) := false;
            shrd_f(c,hi) := true
                    }
        }

        else {                                             # uncached: perform an abstract response
            call abs.response(c,maddr,gnts(msg).data_,ref.evs(lt).type_,lt);
            granted(gnts(msg).ltime_) := true
        }
            }
        }

    }
    mixin tl_Grant before clnt.tl_Grant

specification of Finish message

A finish marks all the Acquires in a transaction as completed.

    action tl_Finish(msg:fns_id) = {
        local c:client_id, hi:tl_addrhi, lo:tl_addrlo, txid: id,  ow:ownership {

        c := fnss(msg).cid;
        txid := fnss(msg).id_;
        hi := fnss(msg).addr_hi;  # this field is aux
        lo := fnss(msg).word;  # this field is aux
        ow := fnss(msg).own;      # this field is aux

Rules for Finishes:

(1) A finished transaction must correspond to some finishing acquire.

        assert ow = none -> unc_f(c,hi,lo);
        assert ow = excl -> excl_f(c,hi);
        assert ow = shrd -> shrd_f(c,hi);

(2) The txid of the finish must match the grant.

        assert addr_gid(c,hi) = txid;

Finish the Acquire

        if ow = none {
            unc_f(c,hi,lo) := false
            };
        if ow = excl {
            excl_f(c,hi) := false
            };
        if ow = shrd {
            shrd_f(c,hi) := false
            }
        }
    }
    mixin tl_Finish before mngr.tl_Finish

specification of Release message

    action tl_Release(msg:rls_id) = {

        local c:client_id, hi:tl_addrhi, lo:tl_addrlo, txid: id, a:addr, d:data {

        c := rlss(msg).cid;
        txid := rlss(msg).id_;
        d := rlss(msg).data_;
        hi := rlss(msg).addr_hi;      # this field is aux
        lo := rlss(msg).word;         # this field is aux
        a := addr_cons(hi,lo);

Rules for all Releases:

(1) Release only cached addresses

        assert cached_hi(c,hi);

(2) No release with pending release with same address.

Because a voluntary release has to be acked before an involuntary release can be issued, we can never have two matching releases pending.

        assert ~none_r(c,hi,lo);

(3) If block is modified, Release must have data

        assert dirt_p(c,a) -> rlss(msg).dirty;

(4) If ordered, we do not allow a release when a release of a different line or different client is partially completed

        assert ordered -> ~((C ~= c | H ~= hi) &
                                 (none_r(C,H,W1) & ~none_r(C,H,W2)
                                 | prb_addr(C,H,W1) & ~prb_addr(C,H,W2)));

        if rlss(msg).voluntary {

Rules for voluntary Releases:

(1) Must have no matching acquires requested or accepted when voluntarily releasing.

        assert ~excl_r(c,hi) & ~excl_a(c,hi) & ~shrd_r(c,hi) & ~shrd_a(c,hi);

(2) if any request releases with same hi address, txid must match

        assert none_r(c,hi,W) -> addr_nid(c,hi) = txid;

(3) May not use a txid in use for a requested voluntary release with a different hi addr

        assert none_r(c,H,L) & H ~= hi -> addr_nid(c,H) ~= txid;

(4): Must have some privs on released words if release is voluntary

        assert excl_p(c,a) | shrd_p(c,a);

(5) No voluntary release if an involuntary one in progress

        assert ~(prb_addr(c,hi,W1) & ~prb_addr(c,hi,W2));

(6) TEMPORARY: voluntary releases must have data In effect, this means clients silently invalid clean blocks. However, this assumption should be remove.

        assert rlss(msg).dirty <-> excl_p(c,a);

(7) A voluntary release beat must be the least word of the block not already released. In other words, voluntary release beats must be in order starting from word zero.

        assert ~none_r(c,hi,W) -> lo <= W;

Mark release as request, record txid

        if rlss(msg).dirty {
            none_r(c,hi,lo) := true
        } else {
                    none_r(c,hi,X) := true   # if no data, just one beat for all
                };
        addr_nid(c,hi) := txid
        }
        else {

Rules for involuntary Releases:

(1) A probe must be requested for the full address.

Note we do allow an involuntary relase with a pending Acquire.

        assert prb_addr(c,hi,lo);

(2) No involuntary release if a voluntary one in progress.

        assert ~none_r(c,hi,X);

(3) Release with data iff exclusive

        assert rlss(msg).dirty <-> excl_p(c,a);

(4) An involuntary release beat must be the least word of the block not already released. In other words, in voluntary release beats must be in order starting from word zero.

        assert prb_addr(c,hi,W) -> lo <= W;

Mark the probe completed. If no data returned, one beat satisfies the probe.

        if rlss(msg).dirty {
            prb_addr(c,hi,lo) := false
                } else {
            prb_addr(c,hi,X) := false
                }
        };

The abstract semantics of release

A dirty release contains one data beat, while a clean release invalidates the entire block

        if rlss(msg).dirty  {
            if excl_p(c,a) {
           call abs.release(c,a,d,excl)
                };
            if shrd_p(c,a) {
           call abs.release(c,a,d,shrd)
                }
        }
        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).

        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))
        }
    }
    }
    mixin tl_Release before mngr.tl_Release

specification of Probe message

    action tl_Probe(msg:prb_id) = {

        local c:client_id, hi:tl_addrhi {

        c := prbs(msg).cid;
        hi := prbs(msg).addr_hi;

Rules for Probes:

(1) Probe only cached addresses

        assert cached_hi(c,hi);

(2) No requested probes on same address

        assert ~prb_addr(c,hi,W);

3) No probe if an Acquire with same hi address is accepted or finishing.

        assert ~excl_a(c,hi) & ~excl_f(c,hi) & ~shrd_a(c,hi) & ~ shrd_f(c,hi);

Mark the probe pending (for all words of line)

        prb_addr(c,hi,W) := true
        }

    }
    mixin tl_Probe before clnt.tl_Probe

Instantiate the abstract interface specification

    instantiate abs : interface_stubs
    instantiate interface(ref,abs,abs,side,cmap)

All or none of a line is cached

    axiom cached(C,addr_cons(H,L)) <-> cached_hi(C,H)

Conjectured invariants of the interface state

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) |
                shrd_r(C,H) | shrd_a(C,H) | shrd_f(C,H)) -> cached_hi(C,H)
    conjecture (unc_r(C,H,L) | unc_a(C,H,L) | unc_f(C,H,L)) -> ~cached_hi(C,H)

An cached acquire must be in only one phase

    conjecture ~(excl_r(C,H) & excl_a(C,H)) & ~(excl_r(C,H) & excl_f(C,H)) & ~(excl_a(C,H) & excl_f(C,H))
    conjecture ~(shrd_r(C,H) & shrd_a(C,H)) & ~(shrd_r(C,H) & shrd_f(C,H)) & ~(shrd_a(C,H) & shrd_f(C,H))

An uncached acquire cannot be accepted (TODO: this will change)

    conjecture ~unc_a(C,H,L)

If accepted acquire, some word must be unserved

    conjecture excl_a(C,H) -> exists W. ~excl_p(C,addr_cons(H,W))
    conjecture shrd_a(C,H) -> exists W. ~shrd_p(C,addr_cons(H,W))

a requested voluntary release is in cached space

    conjecture none_r(C,H,W) -> cached_hi(C,H)

While a voluntary release is pending, to acquires are in progress (but acquires can be finishing, since release can pass finish)

    conjecture none_r(C,H,W) -> ~excl_r(C,H) & ~excl_a(C,H) & ~shrd_r(C,H) & ~shrd_a(C,H)

While a release is pending, client has no privs

    conjecture none_r(C,H,W) & A = addr_cons(H,W) -> ~excl_p(C,A) & ~shrd_p(C,A)

A probe is only in cached space

    conjecture prb_addr(C,H,W) -> cached_hi(C,H)

When finishing and not releasing, we have requested privs

    conjecture excl_f(C,H) & ~none_r(C,H,W) -> excl_p(C,addr_cons(H,W))
    conjecture shrd_f(C,H) & ~none_r(C,H,W) -> shrd_p(C,addr_cons(H,W))

No probe pending with matching accepted or finishing acquire

    conjecture prb_addr(C,H,W) -> ~excl_a(C,H) & ~excl_f(C,H) & ~shrd_a(C,H) & ~shrd_f(C,H)

If a cached acquire is requested and no voluntary release or probe outstanding, we do not have the requested privs

    conjecture excl_r(C,H) & ~none_r(C,H,W) & ~prb_addr(C,H,W) -> ~excl_p(C,addr_cons(H,W))
    conjecture shrd_r(C,H) & ~none_r(C,H,W) & ~prb_addr(C,H,W) -> ~shrd_p(C,addr_cons(H,W))

If an uncached Acquire has been granted, its event has been serialized.

    conjecture granted(E) -> ref.evs(E).serialized

Anything granted is to_ser.

    conjecture granted(E) -> to_ser(E)

If anything to_ser, all prevent events are granted

TEMPORARY conjecture to_ser(E2) & ref.prevents(E1,E2) -> granted(E1)

No two lock operations can be requested for the same client. This is required for release consistency, which would be violated by reordering lock operations.

    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))

(5) No two operations pending on same address for the same client. This is required for release consistency, which would be violated by reordering lock operations. TODO: no client ID's yet

    conjecture ~(to_ser(E1) & to_ser(E2) & ~granted(E1) & ~granted(E2) & E1 ~= E2  &
         ref.evs(E1).id_ = ref.evs(E2).id_
          & ref.evs(E1).addr_ = ref.evs(E2).addr_)

If in accepted phase, request id and accept id must match

    conjecture (excl_a(C,H) | shrd_a(C,H) | unc_a(C,H,W)) -> addr_gid(C,H) = addr_rid(C,H)

No two hi addresses of accepted or finishing transactions can have the same txid

    conjecture
      (excl_a(C,H1) | excl_f(C,H1) | shrd_a(C,H1) | shrd_f(C,H1) | unc_a(C,H1,W1) | unc_f(C,H1,W1))
      & (excl_a(C,H2) | excl_f(C,H2) | shrd_a(C,H2) | shrd_f(C,H2) | unc_a(C,H2,W2) | unc_f(C,H2,W2))
      & H1 ~= H2
       -> addr_gid(C,H1) ~= addr_gid(C,H2)

No two hi addresses of requested transactions can have the same txid

    conjecture
      (excl_r(C,H1) | shrd_r(C,H1) | unc_r(C,H1,W1))
      & (excl_r(C,H2) | shrd_r(C,H2) | unc_r(C,H2,W2))
      & H1 ~= H2
       -> addr_rid(C,H1) ~= addr_rid(C,H2)

No two hi addresses of voluntary releases can have the same txid

    conjecture
     none_r(C,H1,W1) & none_r(C,H2,W2)
      & H1 ~= H2
       -> addr_nid(C,H1) ~= addr_nid(C,H2)

}

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

type client_action = {ca_acquire,ca_finish,ca_perform,ca_fuse}

module tl_generic_client(mngr,ref,side) = {

   action tl_Grant(msg:gnt_id) = {}

   action tl_Probe(msg:prb_id) = {}

   action acquire(a:acq_id) = {
       call mngr.tl_Acquire(a)
   }

   action finish(f:fns_id) = {
       call mngr.tl_Finish(f)
   }

   action release(f:rls_id) = {
       call mngr.tl_Release(f)
   }
   action perform(lt:ltime, sid:id) = {
       assume side(sid) = client;
       call ref.perform(lt,sid)
   }

   action fuse(lt:ltime, lt1:ltime, sid:id) = {
       assume side(sid) = client;
       call ref.fuse(lt,lt1,sid)
   }

   action step = {
     local op:client_action, lt:ltime, lt1:ltime, sid:id, a:acq_id, f:fns_id, r:rls_id {
        if * {
       call acquire(a)
        } else if * {
       call finish(f)
        } else if * {
       call finish(f)
        } else if * {
       call release(r)
        } else if * {
       call perform(lt,sid)
        } else {
       call 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 tl_generic_manager(clnt,ref,side) = {

   action tl_Acquire(msg:acq_id) = {}

   action tl_Finish(msg:fns_id) = {}

   action tl_Release(msg:rls_id) = {}

   action grant(g:gnt_id) = {
      call clnt.tl_Grant(g)
   }

   action probe(g:prb_id) = {
      call clnt.tl_Probe(g)
   }

   action perform(lt:ltime, sid:id) = {
       assume side(sid) = manager;
       call ref.perform(lt,sid)
   }

   action fuse(lt:ltime, lt1:ltime, sid:id) = {
       assume side(sid) = manager;
       call ref.fuse(lt,lt1,sid)
   }

   action step = {
     local lt:ltime, lt1:ltime, sid:id, g:gnt_id, p:prb_id {
        if * {
       call grant(g)
        } else if * {
       call probe(p)
        } else if * {
       call perform(lt,sid)
        } else {
       call fuse(lt,lt1,sid)
        }
     }
   }
}

This module describes the TileLink main memory interface.

This uses only Acquire and Grant messages and is uncached.

module tl_mm_interface(ref,clnt,mngr,side) = {

An Acquire has two phases: requested and accepted

    relation unc_r(A:tl_addrhi,W:tl_addrlo)    # there is a requested uncached acquire
    relation unc_a(A:tl_addrhi,W:tl_addrlo)    # there is an accepted uncached acquire
    relation unc_w(A:tl_addrhi,W:tl_addrlo)    # there is a requested uncached write
    relation unc_wb(A:tl_addrhi)               # there is a requested uncached block write

Each Acquire has a transaction ID (txid). This map tracks the txid associated with requested acquires for a given hi address. It is a protocol invariant that there is at most one such txid.

    individual addr_rid(H:tl_addrhi) : id

Each Grant has a transaction ID (txid). This map tracks the txid associated with grants for a given hi address. It is a protocol invariant that there is at most one such txid.

    individual addr_gid(H:tl_addrhi) : id

An address is dirty if the clients has serialized a write to it. Note this has nothing to do with coherence state.

    relation dirty(A:addr)

Initial condition of interface

Nothing is requested or accepted

    init    ~unc_r(H,W)
          & ~unc_w(H,W)
          & ~unc_a(H,W)
          & ~unc_wb(H)
      & ~dirty(A)

specification of Acquire message

    action tl_Acquire(msg:acq_id) = {

        local hi:tl_addrhi, lo:tl_addrlo, txid: id, ow:ownership, lt:ltime, a:addr, d:data, o:otype, bl:bool {

        ow := acqs(msg).own;
        hi := acqs(msg).addr_hi;
        lo := acqs(msg).word;
        txid := acqs(msg).id_;
        lt := acqs(msg).ltime_;
        a := addr_cons(hi,lo);
        d := acqs(msg).data_;
        o := acqs(msg).op;
        bl := acqs(msg).block;

rules for Acquires

(0) Must be uncached

Temporary

treat cached Acquires as GetBlock assert acqs(msg).own = none;

        if ow ~= none {
            o := read;
        bl := true
        };

(1) May not have a requested acquire with same hi address. TODO: in priciple should allow two with different beat addr

        assert ~unc_r(hi,lo) & ~unc_w(hi,lo);
        assert ~unc_r(hi,W);
        assert unc_w(hi,W) -> (bl & unc_wb(hi));  # may be a beat of multi-beat write

(2) if any requested or accepted transactions with same hi address, txid must match

        assert unc_r(hi,W) -> addr_rid(hi) = txid;
        assert unc_a(hi,W) -> addr_rid(hi) = txid;

(3) May not use a txid in use by a requested tx with a different hi addr

        assert (unc_r(H,W) | unc_w(H,W)) & H ~= hi -> addr_rid(H) ~= txid;

(4) Writes must have correct data

        assert o = write -> d = ref.mem(a);

mark the acquire as requested a block reads marks whole cache block

        if o = read {
            if bl {
                unc_r(hi,X) := true # if block read, request all
                } else {
            unc_r(hi,lo) := true
                }
            } else {
            if bl {
            unc_w(hi,lo) := true;
                unc_wb(hi) := true
                } else {
                unc_w(hi,lo) := true  # if not block write, one beat finishes
                }
            };

Associate the address and txid

        addr_rid(hi) := txid;

Perform abstract operation

        if o = write {
           dirty(a) := false
        }
        }
    }
    mixin tl_Acquire before mngr.tl_Acquire

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 {

        hi := gnts(msg).addr_hi;  # this field is aux
        lo := gnts(msg).word;
        c_txid := gnts(msg).clnt_txid;
        m_txid := gnts(msg).mngr_txid;
        ow := gnts(msg).own;
        lt := gnts(msg).ltime_;
        maddr := addr_cons(hi,lo);                             # construct full address


        assert ~gnts(msg).relack & ow = none;

Rules for normal Grants:

(1) A Grant must match a requested or accepted Acquire. If a multi-beat write, all beats but be received

        assert unc_r(hi,lo) | unc_a(hi,lo) | unc_w(hi,W) | unc_w(hi,lo) & ~unc_wb(hi);

(2) A grant's txid must match its request

        assert addr_rid(hi) = c_txid;

Cannot grant if there is any grant in progress That is, data beats of a grant must be consecutive This assumes an ordered channel

        assert ~(unc_a(H,W) & H ~= hi);

(6) Cannot use a manager-side txid if already in use for a different hi address

        assert ~((unc_a(H,W))
                 & addr_gid(H) = m_txid & H ~= hi);

(7) Cannot use two different manager-side txid's for same hi address.

        assert ~((unc_a(H,W))
                 & addr_gid(H) ~= m_txid & H = hi);

(6) Cannot grant if the txid is already in use for a

different hi address

assert ~(unc_a(H,W) & addr_id(H) = txid & H ~= hi);

(7) Cannot grant if different txid in use for same hi address.

assert ~(unc_a(H,W) & addr_id(H) ~= txid & H = hi);

(8) Cannot grant a request that exactly matches one in progress.

assert ~unc_a(hi,lo);

Data correct if not dirtied by client

        assert ~dirty(maddr) -> gnts(msg).data_ = ref.mem(maddr);

If uncached, mark the event granted. If the request is not part of an accepted transaction, move the request to accepted.

Todo

for no, uncached acquire are only one beat, so can never be in accepted state.

        unc_r(hi,lo) := false; # for now, can't be in accepted state
        unc_w(hi,W) := false;  # one grant for all write beats
        unc_wb(hi) := false;

Transaction is accepted if there are any beats remaining

        unc_a(hi,X) := unc_r(hi,X);

If we are accepting a new uncached transaction, this associates the new txid with the address for accepted transactions.

        addr_gid(hi) := m_txid
        }

    }
    mixin tl_Grant before clnt.tl_Grant

specification of Finish message

A finish marks all the Acquires in a transaction as completed.

    action tl_Finish(msg:fns_id) = {

not allowed

        assert false
    }
    mixin tl_Finish before mngr.tl_Finish

specification of Release message

    action tl_Release(msg:rls_id) = {

not allowed

        assert false
    }
    mixin tl_Release before mngr.tl_Release

specification of Probe message

    action tl_Probe(msg:prb_id) = {

not allowed

        assert false
    }
    mixin tl_Probe before clnt.tl_Probe

specification of perform (serialization)

    action perform(lt:ltime, sid:id) = {

nothing can be serialized on the manager (main memory) side serializing write or atomic dirties the address

       assert side(sid) = client;

       local a:addr,d:data,mo:otype {
           a := ref.evs(lt).addr_;
       d := ref.evs(lt).data_;
       mo := ref.evs(lt).type_;

       if mo ~= read {
        dirty(a) := true  # if modified, mark as dirty
       }
       }
    }
    mixin perform before ref.perform
}