2-layered Cache specification in Quint

[mt40]

Hi everyone.

After some time getting to know Quint. I have done an exercise of designing a 2-layered Cache with the following behaviors:

• 2 layer, N keys, 1 server/cache process, 1 client process
• read from Layer 1, if not exists then Layer 2
• if key is found in Layer 2, write back to Layer 1
• expire time passed = key not exist

Correctness:

• strong consistency: any read returns the latest written value
• validity: any read returns a non-expired value

TODO ideas:

• many client processes
• add stuttering
• inject cache read/write fault

All feedbacks are welcome!

Ok, without further ado. Below is the specification:

module twolayeredcache {
    //**********************************************************
    // TYPE DEFINITIONS
    //**********************************************************
    type CacheLayerValue = {value: str, expire: int}
    type CacheLayer = str -> CacheLayerValue
    type CacheRequest = {tpe: str, key: str, value: str}
    type CacheResponse = {tpe: str, key: str, value: CacheLayerValue, readTime: int}
    type CacheReadResult = {value: CacheLayerValue, readLayer1: bool}

    // tpe: "read" or "write"
    type HistoryEntry = { tpe: str, key: str, value: str, valueExpire: int, time: int }

    //**********************************************************
    // CONSTANTS
    //**********************************************************
    pure val DefaultExpireDuration = 3

    //**********************************************************
    // FUNCTIONAL LAYER
    // Values and functions that are state-independent
    //**********************************************************
    pure val NotFound: CacheLayerValue = {value: "not_found", expire: 0}
    pure def newRequest(): CacheRequest = {
        val tpe = Set("R", "W").chooseSome()
        val key = Set("a", "b", "c").chooseSome()

        if (tpe == "R") {
            {tpe: tpe, key: key, value: ""}
        } else {
            val randomValue = Set("john", "tom", "carl", "alice", "rick").chooseSome()
            {tpe: tpe, key: key, value: randomValue}
        }
    }

    pure def forallListItem(l: List[a], pred: a => bool): bool =
        l.foldl(true, (result, elem) => result and pred(elem))
    
    //**********************************************************
    // STATE MACHINE
    // State-dependent definitions and actions
    //**********************************************************
    var layer1: CacheLayer
    var layer2: CacheLayer

    var requests: List[CacheRequest]
    var responses: List[CacheResponse]

    var history: List[HistoryEntry]
    var historyClock: int

    //**********************************************************
    // HELPERS
    // Functions for convenience
    //**********************************************************
    def require(cond: bool): bool = cond

    def keyExists(key: str, layer: CacheLayer, localTime: int): bool = and {
        layer.keys().contains(key),
        val v = layer.get(key)
        v.expire > localTime
    }

    //**********************************************************
    // ACTIONS
    // 1. Client process
    //**********************************************************

    action sendRequest = all {
        val req = newRequest
        requests' = requests.append(req),

        responses' = responses,
        history' = history,
    }

    action clientProc = all {
        any {
            // receiveResponse,
            sendRequest,
        },
        layer1' = layer1,
        layer2' = layer2,
        historyClock' = historyClock + 1,
    }

    //**********************************************************
    // ACTIONS
    // 1. Server process
    //**********************************************************

    // If this key doesn't exist in L1, read from L2.
    // If key exists in L2, write back to L1 then return.
    // Otherwise, not found.
    def doRead(req: CacheRequest): CacheReadResult = {
        if (keyExists(req.key, layer1, historyClock)){
                {value: layer1.get(req.key), readLayer1: true}
        } else {
            if (keyExists(req.key, layer2, historyClock)) {
                {value: layer2.get(req.key), readLayer1: false}
            } else {
                {value: NotFound, readLayer1: false}
            }
        }
    }

    action handleRead(req: CacheRequest): bool = all {
        val resp = doRead(req)
        all {
            any {
                all {
                    resp.readLayer1,
                    layer1' = layer1,
                    layer2' = layer2,
                },
                all {
                    not(resp.readLayer1),
                    layer1' = layer1.put(req.key, resp.value),
                    layer2' = layer2,
                }
            },
            responses' = responses,
            history' = history.append({
                tpe: "read", 
                key: req.key, 
                value: resp.value.value,
                valueExpire: resp.value.expire,
                time: historyClock,
            }),
        }
    }

    action handleWrite(req: CacheRequest): bool = all {
        layer2' = layer2.put(req.key, {value: req.value, expire: historyClock + DefaultExpireDuration}),
        layer1' = layer1.put(req.key, {value: req.value, expire: historyClock + DefaultExpireDuration}),

        history' = history.append({
            tpe: "write", 
            key: req.key,
            value: req.value,
            valueExpire: 0,
            time: historyClock,
        }),
        responses' = responses,
    }

    action serverProc = all {
        requests.length() > 0,
        {
            val req = requests.head()
            if (req.tpe == "R") {
                handleRead(req)
            } else {
                handleWrite(req)
            }
        },
        requests' = requests.tail(),
        historyClock' = historyClock + 1,
    }

    // INIT:
    action init = all {
        requests' = [],
        responses' = [],
        historyClock' = 1,
        history' = [],
        layer1' = Map("a" -> {value: "1", expire: historyClock + DefaultExpireDuration}),
        layer2' = Map("a" -> {value: "1", expire: historyClock + DefaultExpireDuration}),
    }

    // STEPS:
    action step = any {
        clientProc,
        serverProc,
    }

    //**********************************************************
    // CORRECTNESS
    // 1. Safety Properties / Invariants
    //**********************************************************

    // Any read returns the latest written value. Formally:
    //
    // for any i, j in history:
    //      if i < j and i is a write(k, v) and j is a read(k, v)
    //          then i.time < j.time
    //
    val strongConsistency: bool = {
        val idx = history.indices()
        idx.forall(i => {
            idx.forall(j => {
                i < j
                and history[i].tpe == "write"
                and history[j].tpe == "read"
                and history[i].key == history[j].key
                and history[i].value == history[j].value

                implies history[i].time < history[j].time
            })
        })
    }

    // Any read returns non-expired value
    val validity: bool = {
        val idx = history.indices()
        idx.forall(i => {
            history[i].tpe == "read"
            and history[i].value != NotFound.value

            implies history[i].time < history[i].valueExpire
        })
    }

    val safety: bool = {
        strongConsistency
        and validity
    }

    //**********************************************************
    // CORRECTNESS
    // 2. Liveness Properties / Temporal
    //**********************************************************


    //**********************************************************
    // QUICK TESTS
    //**********************************************************
    // run initAndStepTest = init.then(step)
}

[bugarela]

Hi! Thanks for sharing. If at some point you want to open a PR adding this to our examples folder, we can iterate over PR comments and eventually merge it :)

Perhaps the most important feedback I have is that you can't use chooseSome for non-determinism. It is a deterministic operator, and it is actually not implemented on the Quint simulator as it is quite hard to encode it's behavior in a totally deterministic way. You need to use nondet and oneOf() instead, and those cannot be used outside of actions. See the docs. This is a bit tricky, but non-determinism is super important during model-checking, so we need to follow this rules in order to make it compatible with the underlying tooling. In the following snipped, I moved and adapted things from your newRequest to inside the sendRequest action:

action sendRequest = all {
    nondet tpe = Set("R", "W").oneOf()
    nondet key = Set("a", "b", "c").oneOf()
    nondet value = Set("john", "tom", "carl", "alice", "rick").oneOf()

    pure val req = if (tpe == "R") {
        {tpe: tpe, key: key, value: ""}
    } else {
        {tpe: tpe, key: key, value: value}
    }

    requests' = requests.append(req),
    responses' = responses,
    history' = history,
}

There's one small issue in your init definition. When using all (and more generally in Quint), you can understand it as the actions inside it occurring simultaneously, and you can't use the result of one in another. In your init, you use historyClock in the last two lines, but the assignment historyClock' = 1 will only assign 1 to historyClock in the next state - in this state, it is still undefined. See the error I get:

$ quint run two_layered_cache.qnt
two_layered_cache.qnt:164:51 - error: [QNT502] Variable historyClock not set
164:         layer1' = Map("a" -> {value: "1", expire: historyClock + DefaultExpireDuration}),
                                                       ^^^^^^^^^^^^

Use --seed=0xc625403a6ff57 to reproduce.
error: Runtime error

You can fix it by simply replacing historyClock with 1 on the last couple of lines of init, or creating a pure val for it:

action init = {
    pure val startingClock = 1
    all {
        requests' = [],
        responses' = [],
        historyClock' = startingClock,
        history' = [],
        layer1' = Map("a" -> {value: "1", expire: startingClock + DefaultExpireDuration}),
        layer2' = Map("a" -> {value: "1", expire: startingClock + DefaultExpireDuration}),
    }
}

After these two fixes, I'm able to run your spec on the simulator:

$ quint run two_layered_cache.qnt --invariant=safety

It reports that the invariant holds :D I'll leave it to you to run it yourself and see if the traces match your expectations - I haven't gotten two far in revieweing the behavior itself for now. Let me know if you want assistance with anything else!

[mt40]

Got it, I will change to set when I improve my specs to have multiple client processes. With that, there is actually no ordering of requests.
It will be interesting to see that adding more processes surprisingly reduces the model checking time 😃

[mt40]

hi @bugarela will you be able to review my PR #1549? Let me know if you want to improve anything.

[bugarela]

Hi @mt40! Not this week, I think next one I should - but I thought you meant to change it to support multiple client processes? If you intend to, then it would be nice to get that version into the examples, so I thought I would wait and review the new version. Happy to find some time to review this one though, if you are looking for more feedback before you continue.

[mt40]

hi @bugarela there is this part that I think is not clear:

action step = any {
    clientProc,
    serverProc,
}

My intention is to "randomly" execute the client process or the server process in each step. But I suspect that if clientProc returns true, it will be selected every time.

[bugarela]

That should not be the case, unless serverProc is returning false everytime