|
\/ 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+!
pragmaticformalmodeling/caching/naive-model/cacherequirements.tla
Line 32 in ea86b1b
Checking the property
[]<>DatabaseAndCacheConsistentwith the definition where cache misses are permissible (above), is satisfied by, e.g., the trivial system of an always empty cache. For example,[]<>DatabaseAndCacheConsistentholds with theCacheStartReadThroughFilldisjunct removed fromcacheinvalidationv3!CacheFairness. However, removing\/ cache[k] \in CacheMisswould 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) forfacebookcacheinvalidation,cacheinvalidationv1, andcacheinvalidationv2:PS: Nice real-world tutorial on TLA+!