Skip to content

Commit

Permalink
simplify twolayeredcache spec
Browse files Browse the repository at this point in the history
  • Loading branch information
@mt40
mt40 authored Dec 5, 2024
1 parent 44efe35 commit 2329097
Showing 1 changed file with 97 additions and 133 deletions.
230 changes: 97 additions & 133 deletions examples/tools/twolayeredcache
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,210 +2,174 @@ 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,
}

//**********************************************************
// 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 = {
// 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
}

//**********************************************************
Expand Down

0 comments on commit 2329097

Please sign in to comment.