Example: Two-layered Cache

[mt40]

Continued from this thread: #1548 (comment)

This is a design of an imagined Two-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

Model checking output:

Launching Apalache server
[ok] No violation found (187959ms).
You may increase --max-steps.
Use --verbosity to produce more (or less) output.
Shutting down Apalache server

[mt40]

hi @bugarela I simplified my spec a bit, inspired by the simplicity of https://github.com/mt40/azure-cosmos-tla/blob/master/general-model/cosmos_client.tla

Here are what's changed:

• Remove key-value pairs and use a monotonic increasing num instead. This means I'm only considering only 1 key. Since keys are independent anyway, if 1 key works, then it's trivial to see that N keys would also work.
• Removed server_process, client read/write directly from the cache layers
• Remove expired_time logic. I think that's too detail and too long for an example/learning purpose.
• Adding multiple client processes

The result is 100 LOCs stripped, much faster verify time using Apalache.

[bugarela]

Hi @mt40! This seems like a great simplification. I'm very busy this week, but I'll dive into this next week and get you a nice review.

[bugarela]

Hi! Thanks again for creating this. I've made some comments, but also tweaked it a bit locally to incorporate some of these suggestions and also use sum types for the HistoryEntry, which I believe makes it easier to use and to read.

I added both the resulting file (after my changes) and the diff to this gist: https://gist.github.com/bugarela/5d5586abd7f6c56f71a7f05e3a92bbeb

I have 2 more high-level comments tho:

1. I don't understand how the cache layers can get out of sync in this model. Everytime we write to l1 we also write to l2 and vice-versa, so they will always be the same. I've tried debugging and it doesn't seem like action handleL2Found is ever called.
2. I saw in the other discussion that you might be running Apalache with only 2 steps. I tried running the simulator with 10 steps and it found an issue:

quint run two_layered_cache.qnt --invariant=safety  --max-steps=10

An example execution:

[State 0] { history: [], l1: Set(), l2: Set(), num: 0 }

[State 1] { history: [], l1: Set(), l2: Set(), num: 0 }

[State 2] { history: [Write(0)], l1: Set(0), l2: Set(0), num: 1 }

[State 3] { history: [Write(0)], l1: Set(0), l2: Set(0), num: 1 }

[State 4] { history: [Write(0)], l1: Set(0), l2: Set(0), num: 1 }

[State 5] { history: [Write(0)], l1: Set(0), l2: Set(0), num: 1 }

[State 6] { history: [Write(0), Write(1)], l1: Set(0, 1), l2: Set(0, 1), num: 2 }

[State 7] { history: [Write(0), Write(1), Write(2)], l1: Set(0, 1, 2), l2: Set(0, 1, 2), num: 3 }

[State 8] { history: [Write(0), Write(1), Write(2), Write(3)], l1: Set(0, 1, 2, 3), l2: Set(0, 1, 2, 3), num: 4 }

[State 9]
{ history: [Write(0), Write(1), Write(2), Write(3), Read(2)], l1: Set(0, 1, 2, 3), l2: Set(0, 1, 2, 3), num: 5 }

[violation] Found an issue (14ms).
Use --verbosity=3 to show executions.
Use --seed=0x16e3c92d0963bf to reproduce.
error: Invariant violated

[bugarela]

In order to get some highlighting on GitHub while we don't have official support, we add this comment at the beginning which tells it to consider this as a bluespec file, which is the best matching highlighting for Quint at the moment.

Also, adding underscores to the module name will make it easier to read (which we should also do for the file name).

Suggested change

	module twolayeredcache {
	// -*- mode: Bluespec; -*-
	module two_layered_cache {

[bugarela]

Also, if you can add a header comment here explaining the context and/or adding links about it, and include you as an author, it would be great. Like this one:

quint/examples/classic/distributed/ewd840/ewd840.qnt

Lines 3 to 10 in 7b968e5

	/**
	* Quint spefication for EWD840: an algorithm for distributed termination
	* detection on a ring, due to Dijkstra, published as EWD 840: Derivation
	* of a termination detection algorithm for distributed computations (with
	* W.H.J.Feijen and A.J.M. van Gasteren).
	*
	* Igor Konnov and Gabriela Moreira, Informal Systems, 2022-2023
	*/

[bugarela]

I wonder if this would fit into one of the existing folders. I think it could be under classic/distributed, WDYT?

[bugarela]

This is part of your functional layer section, but it is an action and interacts with state, so I think it should belong in either helpers or actions.

[bugarela]

Minor thing, but we refer to Quint definitions as operators

Suggested change

	// Functions for convenience
	// Operators for convenience

[bugarela]

Some of these are not used. Shall we remove them?

Suggested change

	pure val DefaultExpireDuration = 3
	pure val ClientProcesses: Set[ClientPID] = 1.to(10)
	pure val MaxVal = 1000000
	pure val Expired = -99
	pure val NotFound = -98
	pure val ClientProcesses: Set[ClientPID] = 1.to(10)
	pure val NotFound = -98

[bugarela]

This is easier to read and follows the comment more closely

Suggested change

	if (not(l1.contains(v)) and not(l2.contains(v))) {
	handleNotFound
	} else {
	handleFound(v)
	}
	if (l1.contains(v) or l2.contains(v)) {
	handleFound(v)
	} else {
	handleNotFound
	}

[bugarela]

Passing the state variable "as reference" here and assigning to a parameter is not valid Quint. I noticed Apalache is working with that, I guess because it's made for TLA+ and TLA+ allows arbitrary usage of the prime operator ('). In Quint, you can only use it directly with state variables, so you'd actually have to use something like this:

Suggested change

	action writeLayer(layer: CacheLayer, v: int): bool = all {
	layer' = layer.union(Set(v))
	}
	action writeL1(v: int): bool = all {
	l1' = l1.union(Set(v))
	}
	action writeL2(v: int): bool = all {
	l2' = l2.union(Set(v))
	}

Using the Quint simulator (quint run) with the current definition results in a Runtime Error.