Tilelink concrete unordered channel

This is a model of an unordered channel using TileLink concrete interface

include tilelink_concrete_spec

type of message ID

type msg_id

This is the channel model. It is a bi-directional unordered, non-duplicating channel.

module dut(id,clnt,mngr,ref) = {

The message heap

    relation acqs(I:msg_id,M:acq_id)
    relation gnts(I:msg_id,M:gnt_id)
    relation fnss(I:msg_id,M:fns_id)
    relation rlss(I:msg_id,M:rls_id)
    relation prbs(I:msg_id,M:prb_id)

initially the channels are empty

    init ~acqs(I,A) & ~gnts(I,G) & ~fnss(I,F) & ~rlss(I,R) & ~prbs(I,P)

acquire action called by the client side

this just enqueues a acquire message

    action tl_Acquire(msg:acq_id) = {
        local mid:msg_id {
        assume ~acqs(mid,msg);
        acqs(mid,msg) := true
        }
    }

grant action called by the manager side

this just enqueues a grant message

    action tl_Grant(msg:gnt_id) = {
        local mid:msg_id {
        assume ~gnts(mid,msg);
        gnts(mid,msg) := true
        }
    }

finish action called by the client side

this just enqueues a finish message

    action tl_Finish(msg:fns_id) = {
        local mid:msg_id {
        assume ~fnss(mid,msg);
        fnss(mid,msg) := true
        }
    }

release action called by the client side

this just enqueues a release message

    action tl_Release(msg:rls_id) = {
        local mid:msg_id {
        assume ~rlss(mid,msg);
        rlss(mid,msg) := true
        }
    }

probe action called by the manager side

this just enqueues a probe message

    action tl_Probe(msg:prb_id) = {
        local mid:msg_id {
        assume ~prbs(mid,msg);
        prbs(mid,msg) := true
        }
    }

internal action (step)

pick an arbitary message and deliver it.

    action acquire(a:acq_id) = {
       local mid:msg_id {
        assume acqs(mid,a);
        acqs(mid,a) := false; # remove from channel
        call mngr.tl_Acquire(a)
       }
    }

    action grant(a:gnt_id) = {
       local mid:msg_id {
            assume gnts(mid,a);
            gnts(mid,a) := false; # remove from channel
        call clnt.tl_Grant(a)
       }
    }

    action finish(a:fns_id) = {
       local mid:msg_id {
       assume fnss(mid,a);
       fnss(mid,a) := false; # remove from channel
       call mngr.tl_Finish(a)
       }
    }

    action release(a:rls_id) = {
       local mid:msg_id {
       assume rlss(mid,a);
       rlss(mid,a) := false; # remove from channel
       call mngr.tl_Release(a)
       }
    }

    action probe(a:prb_id) = {
       local mid:msg_id {
            assume prbs(mid,a);
            prbs(mid,a) := false; # remove from channel
        call clnt.tl_Probe(a)
       }
    }

    action step = {
       if * {
           local a:acq_id {call acquire(a)}
       } else if * {
           local a:gnt_id {call grant(a)}
       } else if * {
           local a:fns_id {call finish(a)}
       } else if * {
           local a:rls_id {call release(a)}
       } else {
           local a:prb_id {call probe(a)}
       }
    }
}

Verify the module using the standard testbench

include tilelink_concrete_two_port_testbench

The channel makes these assumptions about the system configuration:

1) The cached address set on front and back is the same.

axiom front.cached(A) <-> back.cached(A)

Conjectured invariants of the channel

Abstract interface state invariants

If front has privs, then back also has privs. Channel doesn't dirty the line

conjecture front.excl_p(A) -> back.excl_p(A)
conjecture front.shrd_p(A) -> back.shrd_p(A)

conjecture back.dirt_p(A) & front.excl_p(A) -> front.dirt_p(A)

If back has request to serialize any event, then front does

conjecture back.to_ser(E) -> front.to_ser(E)

If an event has been granted on front, it has been transmitted to back.

conjecture front.granted(E) -> back.granted(E)

A, uncached, serialized client-side event must be to_ser on back

conjecture ~front.cached(ref.evs(T).addr_) & fside(ref.evs(T).id_) = client & ref.evs(T).serialized -> back.to_ser(T)

conjecture front.to_ser(T) & ref.evs(T).serialized -> back.to_ser(T)

Concrete interface state invariants

Every Acquire pending on the back side is pending on the front.

conjecture back.excl_r(H) -> front.excl_r(H)
conjecture back.shrd_r(H) -> front.shrd_r(H)
conjecture back.unc_r(H,L) -> front.unc_r(H,L)

Every Acquire accepted on the back side is pending or accepted on front

conjecture back.excl_a(H) -> front.excl_r(H) | front.excl_a(H)
conjecture back.shrd_a(H) -> front.shrd_r(H) | front.shrd_a(H)
conjecture back.unc_a(H,L) -> front.unc_r(H,L) | front.unc_a(H,L)

Every cached Acquire finishing on the back side not pending on front TODO: false

conjecture back.excl_a(H) -> ~front.excl_r(H) conjecture back.shrd_a(H) -> ~front.shrd_r(H)

Every Acquire accepted on the front side is accepted or finishing on the back

conjecture front.excl_a(H) -> back.excl_a(H) | back.excl_f(H)
conjecture front.shrd_a(H) -> back.shrd_a(H) | back.shrd_f(H)
conjecture front.unc_a(H,L) -> back.unc_a(H,L) | back.unc_f(H,L)

Every Acquire finishing on the front side is finishing on the back

conjecture front.excl_f(H) -> back.excl_f(H)
conjecture front.shrd_f(H) -> back.shrd_f(H)
conjecture front.unc_f(H,L) -> back.unc_f(H,L)

If a release is pending on the back, must be pending on front

conjecture back.none_r(H,W) -> front.none_r(H,W)

if a probe is pending on the fron, must be pending on back

conjecture front.prb_addr(H,W) -> back.prb_addr(H,W)

If any transaction for a given address is on the back then the txid's on back and front match

conjecture (back.excl_a(H1) | back.shrd_a(H1) | back.unc_a(H1,W1))
              -> front.addr_rid(H1) = back.addr_rid(H1)

conjecture (back.excl_r(H1) | back.shrd_r(H1) | back.unc_r(H1,W1))
           -> front.addr_rid(H1) = back.addr_rid(H1)

If front is accepted or finishing, then the txid's on back and front match

conjecture (front.excl_a(H1) | front.shrd_a(H1) | front.unc_a(H1,W1)
        | front.excl_f(H1) | front.shrd_f(H1) | front.unc_f(H1,W1))
           -> front.addr_id(H1) = back.addr_id(H1)

If back is releasing, then its txid matches front

conjecture back.none_r(H,W) -> back.addr_nid(H) = front.addr_nid(H)

if privs on back but not front, and nothing requested on front, then there must be an old probe or voluntary release pending TODO: false?

conjecture A = addr_cons(H,W) & ~front.excl_p(A) & ~front.excl_r(H) & back.excl_p(A) -> front.none_r(H,W) | back.prb_addr(H,W) conjecture A = addr_cons(H,W) & ~front.shrd_p(A) & ~front.shrd_r(H) & back.shrd_p(A) -> front.none_r(H,W) | back.prb_addr(H,W)

if dirty on back but not front, then there must be an old probe or voluntary release pending

conjecture A = addr_cons(H,W) & ~front.dirt_p(A) & back.dirt_p(A)
       -> front.none_r(H,W) | back.prb_addr(H,W)

if an acquire is in the channel an there is no pending probe, then back does not have the requested privs

conjecture front.excl_r(H) & ~back.excl_r(H) & ~back.excl_a(H) & ~back.excl_f(H)
           & ~back.prb_addr(H,W) & A = addr_cons(H,W) -> ~back.excl_p(A)
conjecture front.shrd_r(H) & ~back.shrd_r(H) & ~back.shrd_a(H) & ~back.shrd_f(H)
           & ~back.prb_addr(H,W) & A = addr_cons(H,W) -> ~back.shrd_p(A)

if nothing in progress on either side, front privs match back

conjecture ~front.excl_r(H) & ~front.excl_a(H) & ~back.excl_r(H) & ~back.excl_a(H)
       & ~front.none_r(H,W) & ~back.prb_addr(H,W) & back.excl_p(addr_cons(H,W)) -> front.excl_p(addr_cons(H,W))
conjecture ~front.shrd_r(H) & ~front.shrd_a(H) & ~back.shrd_r(H) & ~back.shrd_a(H)
       & ~front.none_r(H,W) & ~back.prb_addr(H,W) & back.shrd_p(addr_cons(H,W)) -> front.shrd_p(addr_cons(H,W))

if a probe has not yet been responded to, front privs match back this is to show that when the probe response occurs, priviledges match.

conjecture ~front.excl_a(H) & ~back.excl_a(H)
       & ~front.none_r(H,W) & (b.prbs(I1,M1) & prbs(M1).addr_hi = H | front.prb_addr(H,W))
           & back.excl_p(addr_cons(H,W)) -> front.excl_p(addr_cons(H,W))
conjecture ~front.shrd_a(H) & ~back.shrd_a(H)
       & ~front.none_r(H,W) & (b.prbs(I1,M1) & prbs(M1).addr_hi = H | front.prb_addr(H,W))
           & back.shrd_p(addr_cons(H,W)) -> front.shrd_p(addr_cons(H,W))

if nothing in progress on either side, and front has not released, then it has same privs as back

conjecture ~front.excl_r(H) & ~front.excl_a(H) & ~back.excl_r(H) & ~back.excl_a(H)
       & ~front.none_r(H,W) & front.shrd_p(addr_cons(H,W)) & back.excl_p(addr_cons(H,W)) -> front.excl_p(addr_cons(H,W))
conjecture ~front.shrd_r(H) & ~front.shrd_a(H) & ~back.shrd_r(H) & ~back.shrd_a(H)
       & ~front.none_r(H,W) & front.excl_p(addr_cons(H,W)) & back.shrd_p(addr_cons(H,W)) -> front.shrd_p(addr_cons(H,W))

Channel content invariants.

Acquires

Every Acquire message in the channel is pending on the front side and not pending or accepted on the back side. Moreover, all requested words are unserved.

conjecture b.acqs(I1,M1) & H = acqs(M1).addr_hi & acqs(M1).own = excl ->
          front.excl_r(H) & ~back.excl_r(H) & ~back.excl_a(H) & ~back.excl_f(H)
conjecture b.acqs(I1,M1) & H = acqs(M1).addr_hi & acqs(M1).own = shrd ->
          front.shrd_r(H) & ~back.shrd_r(H) & ~back.shrd_a(H) & ~back.shrd_f(H)
conjecture b.acqs(I1,M1) & H = acqs(M1).addr_hi & W = acqs(M1).word & acqs(M1).own = none ->
          front.unc_r(H,W) & ~back.unc_r(H,W)

Must have correct address, data and op and txid if uncached

conjecture b.acqs(I1,M1) & acqs(M1).own = none & E = acqs(M1).ltime_ ->
       addr_cons(acqs(M1).addr_hi,acqs(M1).word) = ref.evs(E).addr_
       & acqs(M1).data_ = ref.evs(E).data_
       & acqs(M1).op = ref.evs(E).type_

Must have correct txid

conjecture b.acqs(I1,M1) -> front.addr_rid(acqs(M1).addr_hi) = acqs(M1).id_

Event must be ready to request on back

conjecture b.acqs(I1,M1) & acqs(M1).own = none & E = acqs(M1).ltime_ ->
       fside(ref.evs(E).id_) = client &
       front.to_ser(E) & ~front.granted(E) & ~back.to_ser(E) &
       (ref.prevents(E1,E) -> back.to_ser(E1))

Channel can contain a given Acquire message at most once

conjecture b.acqs(I1,M1) & b.acqs(I2,M2) & (I1 ~= I2 | M1 ~= M2) ->
       ~(acqs(M1).own = acqs(M2).own & acqs(M1).addr_hi = acqs(M2).addr_hi &
         (acqs(M1).own ~= none | acqs(M1).word = acqs(M2).word))

No acquire in channel if matching grant in channel

conjecture ~(b.acqs(I1,M1) & b.gnts(I2,M2) & gnts(M2).own = acqs(M1).own &
            gnts(M2).addr_hi = acqs(M1).addr_hi &
        (acqs(M1).own ~= none | gnts(M2).word = acqs(M1).word))

Grants

Every non-relack grant in the channel matches an acquire, which must be pending an front and accepted on back. Specified word must be served on back side and unserved on front side. Grants have correct (aux) address and op, and correct data if not dirtied by client.

conjecture b.gnts(I1,M1) & ~gnts(M1).relack & H = gnts(M1).addr_hi & W = gnts(M1).word & gnts(M1).own = none
       & E = gnts(M1).ltime_
          -> back.unc_f(H,W) &  ~back.unc_r(H,W) & front.unc_r(H,W) & ~front.unc_f(H,W)
                 & back.granted(E) & ~front.granted(E)
                 & gnts(M1).data_ = ref.evs(E).data_
         & addr_cons(H,W) = ref.evs(E).addr_

conjecture b.gnts(I1,M1) & ~gnts(M1).relack & H = gnts(M1).addr_hi & W = gnts(M1).word & gnts(M1).own = excl
       & A = addr_cons(H,W)
          -> (back.excl_a(H) | back.excl_f(H)) & (front.excl_r(H) | front.excl_a(H)) & ~front.excl_f(H)
             & back.excl_p(A) & ~front.excl_p(A)
         &(~front.dirt_p(A) & ~back.dirt_p(A) -> gnts(M1).data_ = ref.mem(A))

conjecture b.gnts(I1,M1) & ~gnts(M1).relack & H = gnts(M1).addr_hi & W = gnts(M1).word & gnts(M1).own = shrd
       & A = addr_cons(H,W)
          -> (back.shrd_a(H) | back.shrd_f(H)) & (front.shrd_r(H) | front.shrd_a(H)) & ~front.shrd_f(H)
             & back.shrd_p(A) & ~front.shrd_p(A)
         &(~front.dirt_p(A) & ~back.dirt_p(A) -> gnts(M1).data_ = ref.mem(A))

All grants must have correct txid on front

conjecture b.gnts(I1,M1) & ~gnts(M1).relack & H = gnts(M1).addr_hi -> front.addr_rid(H) = gnts(M1).id_
conjecture b.gnts(I1,M1) & gnts(M1).relack & H = gnts(M1).addr_hi -> front.addr_nid(H) = gnts(M1).id_

All normal grants must have correct txid on back

conjecture b.gnts(I1,M1) & ~gnts(M1).relack & H = gnts(M1).addr_hi -> back.addr_id(H) = gnts(M1).id_

A relack grant means release requested on front but not back and no release in channel and no accepted or finishing transaction on back and no privs on back.

conjecture b.gnts(I1,M1) & gnts(M1).relack & H = gnts(M1).addr_hi & W = gnts(M1).word ->
       front.none_r(H,W) & ~back.none_r(H,W) &
       ~(b.rlss(I2,M2) & H = rlss(M2).addr_hi & W = rlss(M2).word) &
       ~back.excl_a(H) & ~back.excl_f(H) & ~back.shrd_a(H) & ~back.shrd_f(H)
       & ~back.excl_p(addr_cons(H,W)) & ~back.shrd_p(addr_cons(H,W))

Channel can contain a given Grant message at most once

conjecture b.gnts(I1,M1) & b.gnts(I2,M2) & (I1 ~= I2 | M1 ~= M2) ->
         ~((gnts(M1).own = gnts(M2).own | gnts(M1).relack | gnts(M2).relack)
                & gnts(M1).addr_hi = gnts(M2).addr_hi & gnts(M1).word = gnts(M2).word)

Releases

Every voluntary release message in the channel is pending on the front side and not pending on the back side

conjecture b.rlss(I1,M1) & rlss(M1).voluntary & H = rlss(M1).addr_hi & W = rlss(M1).word ->
                  front.none_r(H,W) & ~back.none_r(H,W)

a voluntary release message means some privs on back side

conjecture b.rlss(I1,M1) & rlss(M1).voluntary & A = addr_cons(rlss(M1).addr_hi,rlss(M1).word) ->
          (back.excl_p(A) | back.shrd_p(A))

a dirty release message in channel means excl privs on back side, and vice-versa

conjecture b.rlss(I1,M1) & A = addr_cons(rlss(M1).addr_hi,rlss(M1).word) ->
          (rlss(M1).dirty <-> back.excl_p(A))

dirty release messages have correct data

conjecture b.rlss(I1,M1) & A = addr_cons(rlss(M1).addr_hi,rlss(M1).word) &
         rlss(M1).dirty -> rlss(M1).data_ = ref.mem(A)

Every involuntary release message in the channel matches a probe that is pending on back side and not pending on font side, and there are no privs on the front side.

conjecture b.rlss(I1,M1) & ~rlss(M1).voluntary & H = rlss(M1).addr_hi & W = rlss(M1).word ->
                  back.prb_addr(H,W) & ~front.prb_addr(H,W) & ~front.none_r(H,W)
          & ~front.excl_p(addr_cons(H,W)) & ~front.shrd_p(addr_cons(H,W))

Voluntary relase message must have correct txid on front

conjecture b.rlss(I1,M1) & rlss(M1).voluntary & H = rlss(M1).addr_hi ->
       front.addr_nid(H) = rlss(M1).id_

no two matching release messages can be in channel

conjecture b.rlss(I1,M1) & b.rlss(I2,M2) & (I1 ~= I2 | M1 ~= M2) ->
         ~(rlss(M1).addr_hi = rlss(M2).addr_hi & rlss(M1).word = rlss(M2).word)

Probes

Every Probe message in the channel is pending on the back side and not pending on the front side

conjecture b.prbs(I1,M1) & H = prbs(M1).addr_hi -> back.prb_addr(H,W) & ~front.prb_addr(H,W)

Can't be matching probe and involuntary release in channel

conjecture ~(b.prbs(I1,M1) & b.rlss(I2,M2)
         & ~rlss(M2).voluntary
         & prbs(M1).addr_hi = rlss(M2).addr_hi)

Can't be two matching probes in channel

conjecture b.prbs(I1,M1) & b.prbs(I2,M2) & (I1 ~= I2 | M1 ~= M2) ->
         ~(prbs(M1).addr_hi = prbs(M2).addr_hi)

Finishes

Every Finish message in the channel matches an acquire that is not finishing on the front side and finishing on the back side. Note: uncached acquires may be requested again before the finish arrives. However, while a grant is still in the channel, no mathing request can occur.

conjecture b.fnss(I1,M1) & H = fnss(M1).addr_hi & W = fnss(M1).word & fnss(M1).own = excl ->
          ~front.excl_r(H) & ~front.excl_a(H) & ~front.excl_f(H) & back.excl_f(H)

conjecture b.fnss(I1,M1) & H = fnss(M1).addr_hi & W = fnss(M1).word & fnss(M1).own = shrd ->
          ~front.shrd_r(H) & ~front.shrd_a(H) & ~front.shrd_f(H) & back.shrd_f(H)

conjecture b.fnss(I1,M1) & H = fnss(M1).addr_hi & W = fnss(M1).word & fnss(M1).own = none ->
          ~front.unc_a(H,W) & ~front.unc_f(H,W) & back.unc_f(H,W)

Must have correct txid (relative to back, since front may have moved on)

conjecture b.fnss(I1,M1) -> back.addr_id(fnss(M1).addr_hi) = fnss(M1).id_

No finish in channel if matching non-relack grant in channel

conjecture ~(b.fnss(I1,M1) & b.gnts(I2,M2) & ~gnts(M2).relack & gnts(M2).own = fnss(M1).own &
            gnts(M2).addr_hi = fnss(M1).addr_hi &
        (fnss(M1).own ~= none | gnts(M2).word = fnss(M1).word))

Can't be two matching finishes in channel

conjecture b.fnss(I1,M1) & b.fnss(I2,M2) & (I1 ~= I2 | M1 ~= M2) ->
       ~(fnss(M1).own = fnss(M2).own & fnss(M1).addr_hi = fnss(M2).addr_hi &
         (fnss(M1).own ~= none | fnss(M1).word = fnss(M2).word))