From 232909700b2e987bd6e18ae4cd0436e9c96fddbf Mon Sep 17 00:00:00 2001 From: Minh Thai Date: Thu, 5 Dec 2024 20:40:25 +0700 Subject: [PATCH] simplify twolayeredcache spec --- examples/tools/twolayeredcache | 230 ++++++++++++++------------------- 1 file changed, 97 insertions(+), 133 deletions(-) diff --git a/examples/tools/twolayeredcache b/examples/tools/twolayeredcache index 120eb9cc8..3fbe5c402 100644 --- a/examples/tools/twolayeredcache +++ b/examples/tools/twolayeredcache @@ -2,168 +2,134 @@ 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} + type CacheLayer = Set[int] + type ClientPID = int // tpe: "read" or "write" - type HistoryEntry = { tpe: str, key: str, value: str, valueExpire: int, time: int } + type HistoryEntry = { tpe: str, value: 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 val ClientProcesses: Set[ClientPID] = 1.to(10) + pure val MaxVal = 1000000 + pure val Expired = -99 + pure val NotFound = -98 //********************************************************** // STATE MACHINE // State-dependent definitions and actions //********************************************************** - var layer1: CacheLayer - var layer2: CacheLayer - var requests: List[CacheRequest] - var responses: List[CacheResponse] + var l1: CacheLayer + var l2: CacheLayer + var num: int + // Global log of system events. Use to specify correctness + // properties below. var history: List[HistoryEntry] - var historyClock: int + + //********************************************************** + // FUNCTIONAL LAYER + // Values and functions that are state-independent + //********************************************************** + + action writeLayer(layer: CacheLayer, v: int): bool = all { + layer' = layer.union(Set(v)) + } //********************************************************** // HELPERS // Functions for convenience //********************************************************** - 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 { - 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} - } + action writeCache(pid: ClientPID, v: int): bool = all { + writeLayer(l1, v), + writeLayer(l2, v), + history' = history.append({ + tpe: "write", + value: v, + }), + } - requests' = requests.append(req), - responses' = responses, - history' = history, + action handleNotFound: bool = all { + l1' = l1, + l2' = l2, + history' = history.append({ + tpe: "read", + value: NotFound, + }), } - action clientProc = all { - any { - // receiveResponse, - sendRequest, - }, - layer1' = layer1, - layer2' = layer2, - historyClock' = historyClock + 1, + action handleL1Found(v: int): bool = all { + l1' = l1, + l2' = l2, + history' = history.append({ + tpe: "read", + value: v, + }), } - //********************************************************** - // ACTIONS - // 1. Server process - //********************************************************** + action handleL2Found(v: int): bool = all { + writeLayer(l1, v), + l2' = l2, + history' = history.append({ + tpe: "read", + value: v, + }), + } - // 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} + action handleFound(v: int): bool = { + if(l1.contains(v)) { + handleL1Found(v) } else { - if (keyExists(req.key, layer2, historyClock)) { - {value: layer2.get(req.key), readLayer1: false} - } else { - {value: NotFound, readLayer1: false} - } + handleL2Found(v) } } - 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, - }), + // If this val doesn't exist in L1, read from L2. + // If val exists in L2, write back to L1 then return. + // Otherwise, not found (false). + action readCache(pid: ClientPID, v: int): bool = { + if (not(l1.contains(v)) and not(l2.contains(v))) { + handleNotFound + } else { + handleFound(v) } } - 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) - } + action clientProc = all { + num' = num + 1, + nondet pid = ClientProcesses.oneOf() + nondet readVal = 1.to(num).oneOf() + any { + writeCache(pid, num), + readCache(pid, readVal), }, - requests' = requests.tail(), - historyClock' = historyClock + 1, } - // INIT: action init = all { - requests' = [], - responses' = [], - historyClock' = 1, + num' = 0, + l1' = Set(), + l2' = Set(), history' = [], - layer1' = Map("a" -> {value: "1", expire: 1 + DefaultExpireDuration}), - layer2' = Map("a" -> {value: "1", expire: 1 + DefaultExpireDuration}), } - // STEPS: + action stutter = all { + num' = num, + l1' = l1, + l2' = l2, + history' = history, + } + action step = any { clientProc, - serverProc, + stutter, } //********************************************************** @@ -171,41 +137,39 @@ module twolayeredcache { // 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 = { + // Read the latest write + val readAfterWrite: 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 + implies history[i].value <= history[j].value }) }) } - // Any read returns non-expired value - val validity: bool = { + // Later write must contain a greater value + val writeAfterWrite: 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 + idx.forall(j => { + i < j + and history[i].tpe == "write" + and history[j].tpe == "write" + implies history[i].value < history[j].value + }) }) } + val strongConsistency: bool = { + readAfterWrite + and writeAfterWrite + } + val safety: bool = { strongConsistency - and validity } //**********************************************************