Weak property cacherequirements!DatabaseAndCacheConsistent

[lemmy]

pragmaticformalmodeling/caching/naive-model/cacherequirements.tla

Line 32 in ea86b1b

\/ cache[k] \in CacheMiss

Checking the property []<>DatabaseAndCacheConsistent with the definition where cache misses are permissible (above), is satisfied by, e.g., the trivial system of an always empty cache. For example, []<>DatabaseAndCacheConsistent holds with the CacheStartReadThroughFill disjunct removed from cacheinvalidationv3!CacheFairness. However, removing \/ cache[k] \in CacheMiss would obviously make the property too strong, since it would require all keys to be added to the cache.

The following two properties pass for cacheinvalidationv3, and appear to trigger the same counterexamples (please verify) for facebookcacheinvalidation, cacheinvalidationv1, and cacheinvalidationv2:

RepeatedlyCacheUsed ==
    []<>\E k \in DOMAIN cache: cache[k] \in CacheHit

RepeatedlyInSync ==
    []<>\A k \in DOMAIN cache: cache[k] \in CacheHit => cache[k].version = database[k]

PS: Nice real-world tutorial on TLA+!