Tilelink concrete snoopy

This is an abstract model of simple snoopy cache using TileLink

include tilelink_concrete_spec

Transaction ID's

type tid

Pending Acquire transactions

The snoopy cache model

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

The cache

    individual cache_data(A:addr) : data
    relation cache_excl(A:tl_addrhi, W:tl_addrlo)
    relation cache_shrd(A:tl_addrhi, W:tl_addrlo)

protocol state

    relation pend_excl(A:tl_addrhi,W:tl_addrlo)
    relation pend_shrd(A:tl_addrhi,W:tl_addrlo)
    relation pend_rls(A:tl_addrhi,W:tl_addrlo)
    relation pend_prb(A:tl_addrhi,W:tl_addrlo)
    relation wait_finish

    init ~cache_excl(A,W) & ~cache_shrd(A,W) & ~pend_rls(A,W) & ~pend_prb(A,W) & ~pend_excl(A,W) & ~pend_shrd(H,W) & ~wait_finish

release action called by the client side not supported

    action tl_Release(msg:rls_id) = {
        assert false  # block it
    }

produce a finish for a given hi addr

    action send_finish(ahi:tl_addrhi, ow:ownership) = {
        local f:fns_id {
        assume fnss(f).id_ = myid;
        assume fnss(f).addr_hi = ahi;
        assume fnss(f).own = ow;
        call mngr.tl_Finish(f)
        }
    }

grant action called by the manager side

    action tl_Grant(msg:gnt_id) = {

        if gnts(msg).relack {

on a release ack, mark release completed

        local ahi:tl_addrhi, w:tl_addrlo {
            w := gnts(msg).word;
            assert exists H. pend_rls(H,w);
        assume pend_rls(ahi,w);
            pend_rls(ahi,w) := false
            }
        }

    else {
        local a:addr, ahi:tl_addrhi, t:tid, w:tl_addrlo {

            w := gnts(msg).word;

        if gnts(msg).own = excl {

find the corresponding transaction

            assert exists H. pend_excl(H,w);
            assume pend_excl(ahi,w);
            a := addr_cons(ahi,w);
            cache_excl(ahi,w) := true;
            cache_data(a) := gnts(msg).data_;
            pend_excl(ahi,w) := false;
            if forall W:tl_addrlo. ~pend_excl(ahi,W:tl_addrlo) {
            call send_finish(ahi,excl)      # fire off a corresponding finish
            }
        }
        else {

find the corresponding transaction

            assert exists H. pend_shrd(H,w);
            assume pend_shrd(ahi,w);
            a := addr_cons(ahi,w);
            cache_shrd(ahi,w) := true;
            if ~cache_excl(ahi,w) {  # ignore data if we might be dirty
                cache_data(a) := gnts(msg).data_
                    };
            pend_shrd(ahi,w) := false;
            if forall W:tl_addrlo. ~pend_shrd(ahi,W:tl_addrlo) {
            call send_finish(ahi,shrd)      # fire off a corresponding finish
            }
                }
        }
    }
    }

construct and send an uncached Grant message

    action grant(mid:id, ahi:tl_addrhi, w:tl_addrlo, d:data, lt:ltime) = {
        local g:gnt_id {
        assume gnts(g).id_ = mid;
        assume gnts(g).word = w;
        assume gnts(g).data_ = d;
        assume gnts(g).ltime_ = lt;
        assume ~gnts(g).relack;
        assume gnts(g).own = none;
        assume gnts(g).addr_hi = ahi;
        call clnt.tl_Grant(g)
        }
    }

Acquire action called by the client side

    action tl_Acquire(msg:acq_id) = {
        assume acqs(msg).own = none;     #only support uncached
    assume ~wait_finish;             # block if last request not finished
    local o:otype, a:addr, d:data, lt:ltime, mid:id, ahi: tl_addrhi, wrd:tl_addrlo {
          o := acqs(msg).op;

          wrd := acqs(msg).word;
          ahi := acqs(msg).addr_hi;
          a := addr_cons(ahi,wrd);
          lt := acqs(msg).ltime_;
          mid := acqs(msg).id_;

              assume o ~= cas;                # don't support cas for now
              if o = read {
              assume cache_excl(ahi,wrd) | cache_shrd(ahi,wrd); # models channel blocking
              d := cache_data(a);
              call ref.perform(lt,myid); # ghost
              call grant(mid,ahi,wrd,d,lt)
              } else { # o = write
              assume cache_excl(ahi,wrd); # models channel blocking
          d := acqs(msg).data_;
              cache_data(a) := d;
              call ref.perform(lt,myid); # ghost
                  call grant(mid,ahi,wrd,d,lt)
              };
          wait_finish := true
        }
    }

internal acquire action TODO: should be able to control words set

    action acquire(ahi:tl_addrhi, word: tl_addrlo, own_:ownership) = {
       local a : addr, msg:acq_id {

         assume own_ ~= none;

         assume ~(pend_excl(H,W) | pend_shrd(H,W)) & H ~= ahi;     # no threading, for now
     assume ~(pend_excl(ahi,W) & own_=excl);                   # not if already acquiring
     assume ~(pend_shrd(ahi,W) & own_=shrd);                   # not if already acquiring

construct an Acquire message

     assume acqs(msg).id_ = myid;
     assume acqs(msg).addr_hi = ahi;
     assume acqs(msg).own = own_;

other Acquire fields are don't-care here.

         if own_ = excl {
             assume ~cache_excl(ahi,W);
         pend_excl(ahi,W) := true
     } else {
             assume ~cache_shrd(ahi,W);
         pend_shrd(ahi,W) := true
         };

     call mngr.tl_Acquire(msg)
       }
    }

steps common to a voluntary and involuntary release

    action send_release(r:rls_id) = {

        local ahi:tl_addrhi, wrd: tl_addrlo, a:addr {

must return the data if exclusive

        wrd := rlss(r).word;
        ahi := rlss(r).addr_hi;
        a := addr_cons(ahi,wrd);
        assume rlss(r).data_ = cache_data(a);
        assume rlss(r).dirty <-> cache_excl(ahi,wrd);

erase privs being released

        cache_excl(ahi,wrd) := false;
        cache_shrd(ahi,wrd) := false;

        call mngr.tl_Release(r)
        }
    }

on receiving a probe, send a release

    action tl_Probe(msg:prb_id) = {

        pend_prb(prbs(msg).addr_hi,W) := true

    }

mark client transaction finished

    action tl_Finish(msg:fns_id) = {
        wait_finish := false
    }


    action vol_release(ahi:tl_addrhi, wrd: tl_addrlo) = {

single threaded

    assume ~pend_rls(H,W) & H ~= ahi;

can only release words for which we have privs

    assume cache_excl(ahi,wrd) | cache_shrd(ahi,wrd);

block the release if we don't have the grants yet

    assume ~pend_excl(ahi,W) & ~pend_shrd(ahi,W);

can't release anything with pending release

        assume ~pend_rls(ahi,W);

        local msg:rls_id, a:addr {

build a release message

        assume rlss(msg).id_ = myid;
        assume rlss(msg).voluntary;
        assume rlss(msg).addr_hi = ahi;
        assume rlss(msg).word = wrd;

mark the release pending

        pend_rls(ahi,wrd) := true;

        call send_release(msg)
        }
    }


    action invol_release(ahi:tl_addrhi, wrd: tl_addrlo) = {

        assume pend_prb(ahi,wrd);

block the probe if we don't have the grants yet

    assume ~pend_excl(ahi,W) & ~pend_shrd(ahi,W);

can't release anything with pending release

        assume ~pend_rls(ahi,W);

        local msg:rls_id, a:addr {

build a release message

        assume rlss(msg).id_ = myid;
        assume ~rlss(msg).voluntary;
        assume rlss(msg).addr_hi = ahi;
        assume rlss(msg).word = wrd;

        call send_release(msg);

mark probe complete

        pend_prb(ahi,wrd) := false

        }
    }

internal action (step)

we can either acquire or release a line

    action step = {
        local ahi:tl_addrhi, wrd: tl_addrlo, own:ownership {
        if * {
            call acquire(ahi, wrd, own)
        } else if * {
            call vol_release(ahi, wrd)
            } else {
            call invol_release(ahi, wrd)
            }
    }
    }
}

Verify the module using the standard testbench

include tilelink_concrete_two_port_testbench

The cache makes two assumptions about the system configuration:

1) supports only one client

axiom fside(I) = client & fside(J) = client -> I = J

2) everything uncached on front side and cached on back side

axiom ~front.cached(A) & back.cached(A)

Conjectured invariants

conjecture b.pend_prb(H,W) <-> back.prb_addr(H,W)

conjecture b.pend_rls(H,W) <-> back.none_r(H,W)

conjecture b.cache_excl(H,W) <-> back.excl_p(addr_cons(H,W))

conjecture b.cache_shrd(H,W) <-> back.shrd_p(addr_cons(H,W))

conjecture b.pend_excl(H,W) -> back.excl_r(H) | back.excl_a(H)

conjecture back.excl_r(H) -> b.pend_excl(H,W)

conjecture back.excl_a(H) -> exists W. b.pend_excl(H,W)

conjecture b.pend_shrd(H,W) -> back.shrd_r(H) | back.shrd_a(H)

conjecture back.shrd_r(H) -> b.pend_shrd(H,W)

conjecture back.shrd_a(H) -> exists W. b.pend_shrd(H,W)

conjecture ~back.excl_f(H) & ~back.shrd_f(H)

conjecture ~back.unc_r(H,W) & ~back.unc_a(H,W) & ~back.unc_f(H,W)

conjecture ~front.unc_r(H,W) & ~front.unc_a(H,W)

conjecture ~front.excl_r(H) & ~front.excl_a(H) & ~front.excl_f(H)

conjecture ~front.shrd_r(H) & ~front.shrd_a(H) & ~front.shrd_f(H)

conjecture front.unc_f(H,W) -> b.wait_finish

conjecture front.unc_f(H1,W1) & front.unc_f(H2,W2) ->  (H1 = H2 & W1 = W2)

conjecture (b.cache_excl(H,W) | b.cache_shrd(H,W)) -> b.cache_data(addr_cons(H,W)) = ref.mem(addr_cons(H,W))

conjecture ~(b.pend_rls(H1,W1) & b.pend_rls(H2,W2) & H1 ~= H2)

conjecture ~(b.pend_excl(H1,W1) & b.pend_excl(H2,W2) & H1 ~= H2)

conjecture ~(b.pend_shrd(H1,W1) & b.pend_shrd(H2,W2) & H1 ~= H2)

conjecture (back.excl_r(H) | back.shrd_r(H)) -> back.addr_rid(H) = buf_id

conjecture (back.excl_a(H) | back.shrd_a(H) | back.excl_f(H) | back.shrd_f(H)) -> back.addr_id(H) = buf_id

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

conjecture ~(b.cache_shrd(H,W) & b.pend_shrd(H,W)) & ~(b.cache_excl(H,W) & b.pend_excl(H,W))

conjecture b.pend_excl(H,W1) & ~b.cache_excl(H,W2) -> b.pend_excl(H,W2)

conjecture b.pend_shrd(H,W1) & ~b.cache_shrd(H,W2) -> b.pend_shrd(H,W2)

export c.acquire
export c.finish
export c.release
export c.perform
export c.fuse