Link Search Menu Expand Document
Pragmatic Formal Modeling

Adding cache invalidation

  1. Designing an initial cache invalidation solution
    1. Initial cache invalidation
  2. Initial cache invalidation solution
    1. Modeling
    2. Verification
  3. Updated cache invalidation solution
    1. An updated design
      1. Updated cache invalidation
    2. Modeling
    3. Verification
  4. Summary

Designing an initial cache invalidation solution

As we determined earlier, we need to be able to systematically evict out-of-date values from the cache. We do that with cache invalidation.

Whenever the database updates a value, it put an invalidation message on a queue. The cache will process messages from that queue: if it contains the key it will evict the value, otherwise it will do nothing.

Assumptions:

  • Our invalidation queue does not guarantee in-order delivery.
  • Our invalidation queue is durable and guarantees at-least-once delivery.

Initial cache invalidation

WriterWriterDatabaseDatabaseCache Invalidation QueueCache Invalidation QueueCacheCacheUpdates dataAdds updated key to queuePolls queueReturns invalidation itemEvicts invalidated key from queuealt[Key not in Cache]Does nothing

Initial cache invalidation solution

Modeling

We are now dealing with multiple processes, cache fill and invalidation, that may interact. Therefore it is necessary to break the processes down into their component steps, which may be executed simultaneously. Also, for context, a Cache Fill describes the process of the Cache requesting data from the Database, the Database responding, and the Cache incorporating that data.

It is now worthwhile to model the cache’s state machine.

InactiveCacheStartReadThroughFillDatabaseRespondToCacheFillCacheCompleteFillCacheFailFill

There is also a very simple message-handling state machine:

InvalidationMessageOnQueueCacheHandleInvalidationMessage

Note that the cache requirements and the underlying data models that are checked stay the same.

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

EXTENDS Naturals

CONSTANTS
    KEYS


VARIABLES
    database,
    cache,
    cacheFillStates, \* cacheFillStatus[key] = Fill state
    invalidationQueue


INSTANCE cacherequirements

vars == <<database, cache, cacheFillStates, invalidationQueue>>

InvalidationMessage == [key: KEYS]

CacheFillState == [state: {"inactive", "started", "respondedto"}, version: DataVersion]

CacheValue == CacheMiss \union CacheHit

TypeOk ==
    /\ database \in [KEYS -> DataVersion]
    /\ cache \in [KEYS -> CacheValue]
    \* We track the cache fill state for each key. It is a multipart process
    /\ cacheFillStates \in [KEYS -> CacheFillState]
    \* We model invalidationQueue as a set, because we cannot guarantee in-order delivery
    /\ invalidationQueue \in SUBSET InvalidationMessage
    
Init ==
    /\ database = [k \in KEYS |-> 0]
    /\ cache = [k \in KEYS |-> [type |-> "miss"]]
    \* Cache fill states start inactive
    /\ cacheFillStates = [k \in KEYS |-> [
                                state |-> "inactive", 
                                \* Version set to earliest possible version
                                version |-> 0]
                          ]
    \* The invalidation queue starts empty
    /\ invalidationQueue = {}


DatabaseUpdate(k) ==
    \* The version of that key is incremented, representing a write
    /\ database' = [database EXCEPT
                        ![k] = database[k] + 1]
    \* Adds invalidation message to queue.
    \* We don't need to model a delay in adding message as the cache can 
    \* always delay handling message to similar effect.
    /\ invalidationQueue' = invalidationQueue \union {[key |-> k]}
    /\ UNCHANGED <<cache, cacheFillStates>>

\* Cache Fill behavior
CacheStartReadThroughFill(k) ==
    \* Read-through only occurs when the cache is unset for that value
    /\ cache[k] \in CacheMiss
    \* One cache fill request at a time
    /\ cacheFillStates[k].state = "inactive"
    /\ cacheFillStates' = [cacheFillStates EXCEPT ![k].state = "started"]
    /\ UNCHANGED <<database, cache, invalidationQueue>>

\* This is the moment the database provides a value for cache fill
DatabaseRespondToCacheFill(k) ==
    /\ cacheFillStates[k].state = "started"
    /\ cacheFillStates' = [cacheFillStates EXCEPT 
                            ![k].state = "respondedto",
                            ![k].version = database[k] 
                           ]
    /\ UNCHANGED <<database, cache, invalidationQueue>>
    
 \* Cache incorporates the data
CacheCompleteFill(k) == 
    /\ cacheFillStates[k].state = "respondedto"
    /\ cacheFillStates' = [cacheFillStates EXCEPT \* Reset to 0 
                            ![k].state = "inactive",
                            ![k].version = 0
                           ]
    /\ cache' = [cache EXCEPT
                        ![k] = [
                           \* Cache value is now a hit
                           type |-> "hit",
                           \* Set to whatever came back in response
                           version |-> cacheFillStates[k].version
                        ]
                ]
    /\ UNCHANGED <<database, invalidationQueue>>
    
\* Cache fails to fill
CacheFailFill(k) == 
    /\ cacheFillStates[k].state = "respondedto"
     \* Cache fill state is reset, having not filled cache
    /\ cacheFillStates' = [cacheFillStates EXCEPT
                            ![k].state = "inactive",
                            ![k].version = 0
                           ]
    /\ UNCHANGED <<database, cache, invalidationQueue>>
    
\* Handle invalidation message. Assume it is not taken off queue in case of
\* failure. Therefore failure modeled as CacheHandleInvalidationMessage not
\* occurring.
CacheHandleInvalidationMessage == 
    /\ \E message \in invalidationQueue: \* Dequeue invalidation queue in any order
        \* Remove message from queue
        /\ invalidationQueue' = invalidationQueue \ {message}
        \* Evict item from cache
        /\ cache' = [cache EXCEPT ![message.key] = [type |-> "miss"]]
    /\ UNCHANGED <<cacheFillStates, database>>

\* Cache eviction model is unchanged
CacheEvict(k) ==
    /\ cache[k] \in CacheHit
    /\ cache' = [cache EXCEPT ![k] = [type |-> "miss"]]
    /\ UNCHANGED <<database, cacheFillStates, invalidationQueue>>

\* The cache will always be able to...
CacheFairness ==
    \E k \in KEYS:
        \* Complete the cache fill process
        \/ CacheStartReadThroughFill(k) 
        \/ DatabaseRespondToCacheFill(k) \* Write
        \/ CacheCompleteFill(k)
        \* Process invalidation messages
        \/ CacheHandleInvalidationMessage



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

Next == 
    \E k \in KEYS:
        \* Database states
        \/ DatabaseUpdate(k)
        \* Cache states
        \/ CacheStartReadThroughFill(k)
        \/ DatabaseRespondToCacheFill(k)
        \/ CacheCompleteFill(k)
        \/ CacheHandleInvalidationMessage
        \/ 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 Wed Jun 15 12:45:25 MST 2022 by elliotswart
\* Created Tue Jun 14 20:36:02 MST 2022 by elliotswart

Verification

When we go to verify it we get an error:

Next Section Download Configuration

Temporal property violated.

  • Stuttering No more updates, and cache remains inconsistent

Clearly we have a race condition between cache invalidation and cache fill. Let’s try to rectify that.

Updated cache invalidation solution

An updated design

So our data has been versioned all along for observability. It’s time to start using the versions in our solution. This isn’t unrealistic, as databases can send snapshot times along with results and invalidations.

Let’s also start sending the data along with the invalidations, so that we can update the cache when things change.

Whenever a cache fill comes back, or an invalidation message is received, we will compare the version we just received to the version in the cache. We will only modify the cache if the version is higher. That way we don’t need to be concerned with race conditions of that sort. Whichever comes back first will be compared to the one that comes back second, and the cache will eventually have the same value.

Updated cache invalidation

WriterWriterDatabaseDatabaseCache Invalidation QueueCache Invalidation QueueCacheCacheUpdates dataAdds updated key andversioned data to queuePolls queueReturns invalidation itemalt[Key not in Cache]Does nothingalt[Key in Cache]Does nothingalt[Cache data olderthan invalidation]Replaces old versionwith data from message

Modeling

We should update the state machines to:

InactiveCacheStartReadThroughFillDatabaseRespondToCacheFillCacheCompleteFillCacheFailFillCacheIgnoreFillfill version is older than stored version
InvalidationMessageOnQueueCacheHandleInvalidationMessageCacheIgnoreInvalidationMessagemessage version is older than stored version

This is reflected in the code below.

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

 \* Cache incorporates the data
CacheCompleteFill(k) == 
    /\ cacheFillStates[k].state = "respondedto"
       \* Either the cache is empty for that key
    /\ \/ cache[k] \in CacheMiss
       \* or we are filling a newer version
       \/ /\ cache[k] \notin CacheMiss
          /\ cache[k].version < cacheFillStates[k].version
    /\ cacheFillStates' = [cacheFillStates EXCEPT \* Reset to 0 
                            ![k].state = "inactive",
                            ![k].version = 0
                           ]
    /\ cache' = [cache EXCEPT
                        ![k] = [
                           type |-> "hit",
                           version |-> cacheFillStates[k].version
                        ]
                ]
    /\ UNCHANGED <<database, invalidationQueue>>

CacheIgnoreFill(k) == 
    /\ cacheFillStates[k].state = "respondedto"
    \* If we have a newer version in cache, ignore fill
    /\ /\ cache[k] \in CacheHit
       /\ cache[k].version >= cacheFillStates[k].version
    /\ cacheFillStates' = [cacheFillStates EXCEPT \* Reset to 0 
                            ![k].state = "inactive",
                            ![k].version = 0
                           ]
    \* Don't update cache
    /\ UNCHANGED <<cache, database, invalidationQueue>>


CacheHandleInvalidationMessage == 
    /\ \E message \in invalidationQueue: \* Dequeue invalidation queue in any order
           \* Key must be in cache
        /\ /\ cache[message.key] \in CacheHit
           \* Message needs to be newer than the cache
           /\ cache[message.key].version < message.version
        \* Update item in cache
        /\ cache' = [cache EXCEPT 
                        ![message.key] = [
                            type |-> "hit",
                            \* Update to version in invalidation message
                            version |-> message.version
                        ]]
        \* Remove message from queue because handled
        /\ invalidationQueue' = invalidationQueue \ {message}

    /\ UNCHANGED <<cacheFillStates, database>>

CacheIgnoreInvalidationMessage == 
    /\ \E message \in invalidationQueue: \* Dequeue invalidation queue in any order
           \* Ignore invalidation messages for messages not in cache
        /\ \/ cache[message.key] \in CacheMiss
           \* Or when the cache already has the same or larger version
           \/ /\ cache[message.key] \notin CacheMiss
              /\ cache[message.key].version >= message.version
        \* Remove message from queue to ignore
        /\ invalidationQueue' = invalidationQueue \ {message}
    \* Don't update cache
    /\ UNCHANGED <<cacheFillStates, database, cache>>

=============================================================================
\* Modification History
\* Last modified Wed Jun 15 13:58:25 MST 2022 by elliotswart
\* Created Wed Jun 15 13:58:13 MST 2022 by elliotswart

Verification

We run it and experience a different error.

Next Section Download Configuration

Temporal property violated.

  • Stuttering No more updates, and cache remains inconsistent

Summary

Our main problem remaining is that cache invalidation messages are ignored if the key is not in the cache. In this case, a cache fill can be completed incorrectly with the old value. More broadly, the solution doesn’t take ongoing cache fills into consideration. We should address this in our next design.



Next: Working cache invalidation