You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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:
pragmaticformalmodeling/caching/naive-model/cacherequirements.tla
Line 32 in ea86b1b
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 theCacheStartReadThroughFill
disjunct removed fromcacheinvalidationv3!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) forfacebookcacheinvalidation
,cacheinvalidationv1
, andcacheinvalidationv2
:PS: Nice real-world tutorial on TLA+!
The text was updated successfully, but these errors were encountered: