Tilelink concrete directory

This is an abstract model of simple directory using TileLink.

The directory has two client ports, clnt0 and clnt1

include tilelink_concrete_spec

This module is a directory for a single port

module dir(myid,clnt,other,ref,mem) = {

    relation cache_excl(H:tl_addrhi,W:tl_addrlo)
    relation cache_shrd(H:tl_addrhi,W:tl_addrlo)

    relation pend_excl(A:tl_addrhi,W:tl_addrlo)
    relation pend_shrd(A:tl_addrhi,W:tl_addrlo)
    relation pend_prb(A:tl_addrhi,W:tl_addrlo)
    relation pend_fnse(A:tl_addrhi)
    relation pend_fnss(A:tl_addrhi)
    individual addr_id(A:tl_addrhi) : id
    individual addr_nid(A:tl_addrhi) : id

    init ~cache_excl(H,W)
    init ~cache_shrd(H,W)
    init ~pend_excl(A,W)
    init ~pend_shrd(A,W)
    init ~pend_prb(A,W)
    init ~pend_fnse(A)
    init ~pend_fnss(A)

release action called by the client side

    action tl_Release(msg:rls_id) = {
        local hi:tl_addrhi, lo:tl_addrlo {
        hi := rlss(msg).addr_hi;
        lo := rlss(msg).word;

        if rlss(msg).voluntary {
            assume ~pend_excl(hi,W) & ~pend_shrd(hi,W);
            assume ~pend_fnse(hi) & ~pend_fnss(hi)
            };

            if rlss(msg).dirty {
            mem(addr_cons(hi,lo)) := rlss(msg).data_
            };
        cache_excl(hi,lo) := false;
        cache_shrd(hi,lo) := false;

        if rlss(msg).voluntary {
        local rsp:gnt_id {
            assume gnts(rsp).id_ = rlss(msg).id_;
            assume gnts(rsp).addr_hi = hi;
            assume gnts(rsp).word = lo;
            assume gnts(rsp).relack;
            call clnt.tl_Grant(rsp)
                }
            }
        else {
            pend_prb(hi,lo) := false
            }
        }
    }

acquire action called by the client side

    action tl_Acquire(msg:acq_id) = {
        local hi:tl_addrhi, lo:tl_addrlo, ow:ownership, txid:id {
        hi := acqs(msg).addr_hi;
        ow := acqs(msg).own;
        txid := acqs(msg).id_;

block the acquire if we can't grant

rule: Cannot grant if there is a pending probe with the same hi address

        assume ~pend_prb(hi,W);

rule: Cannot grant if the txid if already in use for a different hi address

        assume ~((pend_excl(H,W) | pend_fnse(H) | pend_shrd(H,W) | pend_fnss(H))
             & addr_id(H) = txid & H ~= hi);

rule: Cannot grant if different txid in use for same hi address.

            assume ~((pend_excl(H,W) | pend_fnse(H) | pend_shrd(H,W) | pend_fnss(H))
                 & addr_id(H) ~= txid & H = hi);


        addr_id(hi) := txid;

        if ow = excl {
            pend_excl(hi,W) := true
        }
            else {
            pend_shrd(hi,W) := true
            }
        }
    }

internal grant action

    action grant(hi:tl_addrhi, lo:tl_addrlo, ow:ownership) = {

    assume ow ~= none;

cannot grant privs if other client has exclusive

    assume ~other.cache_excl(hi,W);

    if ow = excl {
        assume pend_excl(hi,lo);
        pend_excl(hi,lo) := false;
        if forall W:tl_addrlo. ~pend_excl(hi,W:tl_addrlo) {
            pend_fnse(hi) := true
            };
        cache_excl(hi,lo) := true
        }
    else {
        assume pend_shrd(hi,lo);
        pend_shrd(hi,lo) := false;
        if forall W:tl_addrlo. ~pend_shrd(hi,W:tl_addrlo) {
            pend_fnss(hi) := true
            };
        cache_shrd(hi,lo) := true
        };

    local rsp:gnt_id {
        assume gnts(rsp).id_ = addr_id(hi);
        assume gnts(rsp).addr_hi = hi;
        assume gnts(rsp).word = lo;
        assume gnts(rsp).own = ow;
        assume gnts(rsp).data_ = mem(addr_cons(hi,lo));
        assume ~gnts(rsp).relack;
        call clnt.tl_Grant(rsp)
        }
    }

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

        txid := fnss(msg).id_;

        assert exists H. addr_id(H) = txid & (pend_fnss(H) | pend_fnse(H));  # look up addr by txid
        assume addr_id(hi) = txid & (pend_fnss(hi) | pend_fnse(hi));

tricky: if both excl and shrd are request, we don't know which this is the finish for, so we just guess

        if pend_fnss(hi) {
            pend_fnss(hi) := false
        } else {
            pend_fnse(hi) := false
            }
        }
    }

internal probe action

    action probe(hi:tl_addrhi) = {

if the other client has requested privs and we have excl, then we probe

       if exists W1:tl_addrlo,W2:tl_addrlo.
            ((other.pend_excl(hi,W1:tl_addrlo) | other.pend_shrd(hi,W1:tl_addrlo))
               & cache_excl(hi,W2:tl_addrlo)) {

probe rules

      assume ~pend_prb(hi,W);

      assume ~(pend_excl(hi,W) | pend_fnse(hi) | pend_shrd(hi,W) | pend_fnss(hi));

      local rsp:prb_id {
          assume prbs(rsp).addr_hi = hi;
          call clnt.tl_Probe(rsp)
      };

      pend_prb(hi,W) := true

       }
    }

   action step = {
     local hi:tl_addrhi, lo:tl_addrlo, ow:ownership {
        if * {
       call grant(hi,lo,ow)
        } else {
       call probe(hi)
        }
     }
   }
}

module dut(myid,clnt0,clnt1,ref) = {

The directory state

    individual mem(A:addr) : data

    init mem(A) = ref.mem(A)

    instantiate dir0 : dir(myid,clnt0,dir1,ref,mem)
    instantiate dir1 : dir(myid,clnt1,dir0,ref,mem)

    action step = {
       if * {
           call dir0.step
       } else {
           call dir1.step
       }
    }
}

Verify the module using the standard testbench

include tilelink_concrete_two_client_testbench

The directory makes assumptions about the system configuration:

1) everything cached on both ports

axiom intf0.cached(A) & intf1.cached(A)

Conjectured invariants

module dirinv(b,intf) = {

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

    conjecture ~intf.none_r(H,W)

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

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

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

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

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

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

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

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

Note: fnse and fnss can be swapped because finish messages don't carry their ownership status.

    conjecture ((intf.excl_f(H) <-> b.pend_fnse(H)) & (intf.shrd_f(H) <-> b.pend_fnss(H)))
               | ((intf.excl_f(H) <-> b.pend_fnss(H)) & (intf.shrd_f(H) <-> b.pend_fnse(H)))

    conjecture (b.pend_excl(H,W) -> ~b.pend_fnse(H)) & (b.pend_shrd(H,W) -> ~b.pend_fnss(H))

Note: if we think an excl finish is pending and it isn't, it is because a shrd finish is pending, but the finishes got crossed (see note above). This means we have not released, so we must have excl privs. This implies that a new excl request cannot come in to confuse us.

    conjecture (~intf.excl_f(H) & b.pend_fnse(H) -> intf.excl_p(addr_cons(H,W)))
               & (~intf.shrd_f(H) & b.pend_fnss(H) -> intf.shrd_p(addr_cons(H,W)))

    conjecture (intf.excl_r(H) | intf.shrd_r(H)) -> intf.addr_rid(H) = b.addr_id(H)

    conjecture (intf.excl_a(H) | intf.shrd_a(H) | intf.excl_f(H) | intf.shrd_f(H)) -> intf.addr_id(H)  = b.addr_id(H)

    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)

    conjecture ~(b.pend_prb(H,W1) & (b.pend_excl(H,W2) | b.pend_fnse(H) | b.pend_shrd(H,W2) | b.pend_fnss(H)))

    conjecture ~((b.pend_excl(H1,W1) | b.pend_shrd(H1,W1) | b.pend_fnse(H1) | b.pend_fnss(H1))
                 & (b.pend_excl(H2,W2) | b.pend_shrd(H2,W2) | b.pend_fnse(H2) | b.pend_fnss(H2))
                 & H1 ~= H2 & b.addr_id(H1) = b.addr_id(H2))
}

instantiate dirinv(b.dir0,intf0)
instantiate dirinv(b.dir1,intf1)

conjecture ~b.dir0.cache_excl(H,W) & ~b.dir1.cache_excl(H,W) -> b.mem(addr_cons(H,W)) = ref.mem(addr_cons(H,W))

conjecture ~intf0.dirt_p(A) & ~intf1.dirt_p(A) -> b.mem(A) = ref.mem(A)

conjecture ~(b.dir0.cache_excl(H,W) & b.dir1.cache_excl(H,W))