MESI Cache Coherence

The MESI protocol maintains cache coherence in multiprocessor systems. Each cache line is in one of four states: Modified, Exclusive, Shared, or Invalid. The spec verifies that no two caches hold the same value in conflicting states.

The spec

Source

module MESI

// MESI cache coherence protocol
// From: Papamarcos & Patel, "A low-overhead coherence solution for
//       multiprocessors with private cache memories" (ISCA 1984)
// C+1 cores (0..C), each with a cache line for a single address.
// Values 0..V represent possible data values.
// State encoding: 0=Invalid, 1=Shared, 2=Exclusive, 3=Modified
// Bus transactions are modeled atomically.
// Use: specl check mesi.specl -c C=2 -c V=1 --no-deadlock
// Verified: C=3 V=3 -> 144 states, all invariants OK

const C: Int
const V: Int

// Per core: cache line state (0=I, 1=S, 2=E, 3=M)
var cacheState: Dict[Int, Int]
// Per core: cached data value (-1 = not valid)
var cacheData: Dict[Int, Int]
// Memory value
var memory: Int

init {
    cacheState = {c: 0 for c in 0..C};
    cacheData = {c: -1 for c in 0..C};
    memory = 0;
}

// BusRd from Invalid when another core has M: M-holder flushes
// Both requester and M-holder go to S
action PrRdMissFromM(core: 0..C, mHolder: 0..C) {
    require core != mHolder;
    require cacheState[core] == 0;
    require cacheState[mHolder] == 3;
    cacheState = {c: (if c == core then 1
        else if c == mHolder then 1
        else cacheState[c]) for c in 0..C};
    cacheData = cacheData | {core: cacheData[mHolder]};
    memory = cacheData[mHolder];
}

// BusRd from Invalid when another core has E (no M exists): E-holder -> S
action PrRdMissFromE(core: 0..C, eHolder: 0..C) {
    require core != eHolder;
    require cacheState[core] == 0;
    require cacheState[eHolder] == 2;
    require not (any c in 0..C: c != core and cacheState[c] == 3);
    cacheState = {c: (if c == core then 1
        else if c == eHolder then 1
        else cacheState[c]) for c in 0..C};
    cacheData = cacheData | {core: memory};
}

// BusRd from Invalid when others have S only (no M or E)
action PrRdMissFromS(core: 0..C) {
    require cacheState[core] == 0;
    require any c in 0..C: c != core and cacheState[c] == 1;
    require not (any c in 0..C: c != core and (cacheState[c] == 2 or cacheState[c] == 3));
    cacheState = cacheState | {core: 1};
    cacheData = cacheData | {core: memory};
}

// BusRd from Invalid when no other cache has the line -> Exclusive
action PrRdMissNoSharers(core: 0..C) {
    require cacheState[core] == 0;
    require not (any c in 0..C: c != core and cacheState[c] != 0);
    cacheState = cacheState | {core: 2};
    cacheData = cacheData | {core: memory};
}

// Processor Write from Invalid: BusRdX
// If an M-holder exists, it flushes first
action PrWrFromInvalidWithM(core: 0..C, val: 0..V, mHolder: 0..C) {
    require core != mHolder;
    require cacheState[core] == 0;
    require cacheState[mHolder] == 3;
    memory = cacheData[mHolder];
    cacheState = {c: (if c == core then 3 else 0) for c in 0..C};
    cacheData = {c: (if c == core then val else -1) for c in 0..C};
}

// Write from Invalid, no M-holder
action PrWrFromInvalidNoM(core: 0..C, val: 0..V) {
    require cacheState[core] == 0;
    require not (any c in 0..C: c != core and cacheState[c] == 3);
    cacheState = {c: (if c == core then 3 else 0) for c in 0..C};
    cacheData = {c: (if c == core then val else -1) for c in 0..C};
}

// Processor Write from Shared: BusUpgr (invalidate other S copies)
action PrWrFromShared(core: 0..C, val: 0..V) {
    require cacheState[core] == 1;
    cacheState = {c: (if c == core then 3 else if cacheState[c] == 1 then 0 else cacheState[c]) for c in 0..C};
    cacheData = {c: (if c == core then val else if cacheState[c] == 1 then -1 else cacheData[c]) for c in 0..C};
}

// Processor Write from Exclusive: silent upgrade, no bus transaction
action PrWrFromExclusive(core: 0..C, val: 0..V) {
    require cacheState[core] == 2;
    cacheState = cacheState | {core: 3};
    cacheData = cacheData | {core: val};
}

// Processor Write from Modified: already M, just update value
action PrWrFromModified(core: 0..C, val: 0..V) {
    require cacheState[core] == 3;
    cacheData = cacheData | {core: val};
}

// Eviction from Modified: writeback to memory
action EvictModified(core: 0..C) {
    require cacheState[core] == 3;
    memory = cacheData[core];
    cacheState = cacheState | {core: 0};
    cacheData = cacheData | {core: -1};
}

// Eviction from Exclusive or Shared: silent
action EvictClean(core: 0..C) {
    require cacheState[core] == 1 or cacheState[core] == 2;
    cacheState = cacheState | {core: 0};
    cacheData = cacheData | {core: -1};
}

// SWMR: if M exists, no other valid copies
invariant SWMR {
    all c1 in 0..C: all c2 in 0..C:
        (c1 != c2 and cacheState[c1] == 3) implies cacheState[c2] == 0
}

// Exclusive exclusivity: if E exists, no other valid copies
invariant ExclusiveExclusive {
    all c1 in 0..C: all c2 in 0..C:
        (c1 != c2 and cacheState[c1] == 2) implies cacheState[c2] == 0
}

// Data coherence: all S-state caches agree with memory
invariant SharedMatchesMemory {
    all c in 0..C: cacheState[c] == 1 implies cacheData[c] == memory
}

// Data coherence: E-state cache matches memory
invariant ExclusiveMatchesMemory {
    all c in 0..C: cacheState[c] == 2 implies cacheData[c] == memory
}

What to notice

• Full dict comprehension with if/then/else. The actions use conditional comprehensions to update all caches simultaneously — when one cache takes exclusive ownership, all others invalidate.
• Hardware domain. This models a real CPU cache protocol, demonstrating that Specl works for hardware verification, not just distributed systems.
• Inherently small state space. Even with many caches, there are only 4 states per cache line, keeping the state space manageable.

specl check mesi.specl -c C=2 -c V=1 --no-deadlock