Link Search Menu Expand Document
Pragmatic Formal Modeling

A naive model of caching

  1. Designing a naive cache
  2. Success criteria
  3. Modeling the cache
  4. Verifying the cache
  5. Summary

Designing a naive cache

In addition to the parameters described previously, we will make a few design decisions:

  • Caches will only be filled during reads (as pictured below).
  • We will not worry about cache invalidation.
  • We will only model a single cache. We are assuming it is either one server, or one consistent replica set. Note: While there are generally many cache servers, the complexity of cache invalidation (at this level) can be modeled with just one cache and one database.

So essentially the only operation we are implementing is the read described in the last section.

Web ServerWeb ServerCacheCacheDatabaseDatabaseRequests queryalt[cache miss]Requests query resultReturns dataCaches query resultReturns data

Now we have all our design parameters. Let’s model!

Success criteria

Because caches are so well understood, we can come up with our success criteria before modeling. Note how it defines certain key data models, so success can be defined.

Next Section Download Code Download PDF
Show Code Show LaTex 
------------------------- MODULE cacherequirements -------------------------

EXTENDS Naturals

CONSTANTS
    KEYS \* The full set of keys in the database

VARIABLES
    database, \* database[key] = DataVersion
    cache \* cache[key] = CacheValue


\* The maximum number of versions a key can have in this model
MaxVersions == 4

\* Data versions are scoped to an individual key
DataVersion == Nat

\* Represents the absence of a value in a cache
CacheMiss == [type: {"miss"}]

\* Represents the presence of a value in a cache, as well as the value
CacheHit == [type : {"hit"}, version: DataVersion]

DatabaseAndCacheConsistent ==
    \A k \in KEYS:
        \* If the key is in cache
        \/ /\ cache[k] \in CacheHit
            \* It should be the same version as the database
           /\ cache[k].version = database[k]
        \* A cache miss is also okay. A cache won't hold everything
        \/ cache[k] \in CacheMiss

\* This means that at some point, the database and cache are consistent.
\* It is important to note that this is not eventual consistency.
\* This only says it needs to be eventually consistent once.
EventuallyDatabaseAndCacheConsistent == <>DatabaseAndCacheConsistent 

\* The cache must be always eventually consistent.
AlwaysEventuallyDatabaseAndCacheConsistent == 
    []EventuallyDatabaseAndCacheConsistent

\* Used as a state constraint to prevent unbounded testing
\* with infinite versions.
DatabaseRecordsDoNotExceedMaxVersion == 
    \A k \in KEYS:
        database[k] < MaxVersions

=============================================================================
\* Modification History
\* Last modified Tue Jun 14 22:44:55 MST 2022 by elliotswart
\* Created Tue Jun 14 21:36:26 MST 2022 by elliotswart

Note: the requirements are their own TLA+ module. In all our models, we will import it. We can think of it a bit like an interface in a standard programming language.

Modeling the cache

We model the cache, importing the cache requirements module rather than redefining the expressions it provides.

Next Section Download Code Download PDF
Show Code Show LaTex 
----------------------------- MODULE naivecache -----------------------------

EXTENDS Naturals

CONSTANTS
    KEYS \* The full set of keys in the database


VARIABLES
    database, \* database[key] = DataVersion
    cache \* cache[key] = CacheValue

\* Imports cache requirements to test against
INSTANCE cacherequirements


vars == <<database, cache>>

\* A cache can hold a hit or a miss for any given key
CacheValue == CacheMiss \union CacheHit

TypeOk ==
    \* database is a mapping of keys to a data version
    /\ database \in [KEYS -> DataVersion]
    \* cache is a mapping of kets to a cache value
    /\ cache \in [KEYS -> CacheValue]
    
Init ==
    \* All keys in the database are initialized to their first version
    /\ database = [k \in KEYS |-> 0]
    \* All keys in the cache are initialized to a miss, i.e. no data in cache
    /\ cache = [k \in KEYS |-> [type |-> "miss"]]


DatabaseUpdate(k) ==
    \* The version of that key is incremented, representing a write
    /\ database' = [database EXCEPT
                        ![k] = database[k] + 1]
    /\ UNCHANGED cache

CacheRead(k) == 
    \* The data is already in the cache
    /\ cache[k] \in CacheHit
    \* So the cache remains the same
    /\ UNCHANGED cache
    /\ UNCHANGED database

CacheReadThrough(k) ==
    \* The data is not in the cache
    /\ cache[k] \in CacheMiss 
    \* So it is read from the database
    /\ cache' = [cache EXCEPT
                        ![k] = [
                           \* Cache value is now a hit
                           type |-> "hit",
                           \* Set to whatever version is in database
                           version |-> database[k]
                        ]
                ]
    /\ UNCHANGED database
  
CacheEvict(k) ==
    \* The data is in cache, so can be evicted
    /\ cache[k] \in CacheHit
    \* cache[k]is turned into a miss
    /\ cache' = [cache EXCEPT ![k] = [type |-> "miss"]]
    /\ UNCHANGED database

(***************************************************************************)
(* Fairness: Normally no operation is guaranteed to happen; it just may.   *)
(* However, that means that the cache could just stop reading forever.     *)
(* And so it would never update. Now that doesn't seem reasonable.         *)
(***************************************************************************)

\* The cache will always be able to...
CacheFairness ==
    \E k \in KEYS:
        \/ CacheRead(k) \* Read
        \/ CacheReadThrough(k) \* Write
        \* CacheEvict(k) is not here, because CacheEvict is something that
        \*               may happen. It is not guaranteed



(***************************************************************************)
(* Specification                                                           *)
(***************************************************************************)

Next == 
    \E k \in KEYS:
        \* Database states
        \/ DatabaseUpdate(k)
        \* Cache states
        \/ CacheRead(k)
        \/ CacheReadThrough(k)
        \/ CacheEvict(k)

\* Cache fairness is included as part of the specification of system behavior.
\* This is just how the system works.
Spec == Init /\ [][Next]_vars /\ WF_vars(CacheFairness)

=============================================================================
\* Modification History
\* Last modified Tue Jun 14 22:51:06 MST 2022 by elliotswart
\* Created Tue Jun 14 20:36:02 MST 2022 by elliotswart

Verifying the cache

First let’s try setting DatabaseAndCacheConsistent as an invariant and see what happens. This says that the cache and the database must always be consistent with each other.

Next Section

Invariant DatabaseAndCacheConsistent is violated.

  • 3. DatabaseUpdate The database updates to version 1 of key 1. No longer consistent with cache.
    • cache
      • k1
        • type: hit
        • version: 0
    • database
      • k1 : 1

This is what we’d expect. The Cache and the Database are not always consistent with each other. If this passed, we should doubt the model.

What if we use the eventually consistent property AlwaysEventuallyDatabaseAndCacheConsistent? We get another error. Temporal property violations are not as clear as logical ones.

Next Section

Temporal properties were violated.

  • Stuttering Cache could do nothing, and remained inconsistent

Because we have no way of guaranteeing that a key will be evicted from the cache, as soon as the key is set, the cache will not change.

Summary

As we can see, our current model of cache is not eventually consistent with the database. We need to systematically clear the cache of outdated values. We need cache invalidation.



Next: Adding cache invalidation