Link Search Menu Expand Document
Pragmatic Formal Modeling

(Implementing New Requirements) Significant improvement

  1. Refining the design
    1. Storage Cleaner Run
    2. Assumptions
  2. Modeling the design
  3. Verifying Storage Cleaner
  4. A quick fix

Refining the design

How do we prevent the cleaner from deleting items just as they are being written? Well, the common sense solution is to check the creation time. We should only start cleaning a key after a safe window of time has passed since its creation. Let’s call it 2 hours.

Storage Cleaner Run

Storage CleanerStorage CleanerDatabaseDatabaseBlob StoreBlob StoreGets batch of keys that have been created more than or exactly 2 hours agoReturns batch of keysQueries for unused keysReturns unused keysBatch deletes unused keysReturns statusalt[any failure]Repeats from beginning

Assumptions

We are making one main assumption: that all of our clocks are accurate within a reasonable margin of error (5 minutes is generous), and our code errs on the side of not deleting based on those margins.

While you can’t always make assumptions about clock time in distributed systems, in this case our time frames are so large (hours) that it’s probably not a bad assumption. Note: this doesn’t mean a program will necessarily check its clock. It could stall and then resume what it’s doing an hour later.

Modeling the design

Now we have to introduce a concept of time in the model. You might think we’ve been using time throughout this whole tutorial, but actually, we were just using ordering. We will need to add the concept of creation time to the blob store. Keep in mind that the state diagram has not changed.

Note: This isn’t adding functionality. We’re just modeling details that have become relevant.

Next Section Download Code Download PDF
Show Code Show LaTex 
---------------------------- MODULE storagecleanerimproved ----------------------------
EXTENDS Naturals, Sequences, FiniteSets

CONSTANTS 
    USERIDS,
    SERVERS,
    METADATAS,
    IMAGES,
    UUIDS,
    CLEANERS

VARIABLES
    (***********************************************************************)
    (* Implementation variables                                            *)
    (***********************************************************************)
    databaseState,
    blobStoreState,
    serverStates,
    cleanerStates,

    \* We just added a time variable here
    time, \* Natural number representing the number of hours that have passed

    (***********************************************************************)
    (* Observability variables                                             *)
    (***********************************************************************)
    operations 

vars == <<databaseState, blobStoreState, 
            serverStates, operations, cleanerStates, time>> 

cleanerVars == <<cleanerStates>>

(***************************************************************************)
(* Strong Typing                                                           *)
(***************************************************************************)

UserIdVal == USERIDS \union {"UNSET"}
MetadataVal == METADATAS \union {"UNSET"}
ImageVal == IMAGES \union {"UNSET"}
UUIDVal == UUIDS \union {"UNSET"}

DatabaseRecord == [
    metadata: MetadataVal,
    imageId: UUIDVal
]

\* A blob store record is modeled to store creation time
BlobStoreRecord == [
    image: ImageVal,
    created: Nat
]  \union {[
    status |-> "UNSET",
    image |-> "UNSET"
]} \* It can still be unset


ServerStateVal == 
    [
        state: {
            "waiting",
            "started_write",
            "wrote_blob",
            "started_read",
            "read_metadata"
        }, 
        userId: UserIdVal,
        metadata:  MetadataVal,
        imageId: UUIDVal,
        image: ImageVal
    ]

CleanerStateVal == 
    [
        state: {
            "waiting", 
            "got_blob_keys", 
            "got_unused_keys",
            "deleting_keys" 
        },
        blobKeys: SUBSET UUIDS,
        unusedBlobKeys: SUBSET UUIDS
    ]


OperationValue == [type: {"READ", "WRITE"}, 
                   userId: UserIdVal, 
                   metadata: MetadataVal, 
                   image:ImageVal]

TypeOk ==
    /\ databaseState \in [USERIDS -> DatabaseRecord]
    \* Blob store is updated to store records. Can be a record or unset
    /\ blobStoreState \in [UUIDS -> BlobStoreRecord]
    /\ serverStates \in [SERVERS -> ServerStateVal]
    /\ cleanerStates \in [CLEANERS -> CleanerStateVal]
    /\ operations \in Seq(OperationValue)
    /\ time \in Nat \* Time is represented as a natural number


Init ==
    /\ databaseState = 
            [u \in USERIDS |-> [metadata |-> "UNSET", imageId |-> "UNSET"]]
    /\ blobStoreState = 
            [u \in UUIDS |->  [status |-> "UNSET", image |-> "UNSET"]]
    /\ serverStates = [s \in SERVERS |->  [state |-> "waiting",
                                           userId |-> "UNSET",
                                           metadata |-> "UNSET",
                                           imageId |-> "UNSET",
                                           image |-> "UNSET"
                                          ]]
    /\ cleanerStates = [c \in CLEANERS |-> [
                                                    state |-> "waiting",
                                                    blobKeys |-> {},
                                                    unusedBlobKeys |-> {}
                                                  ]]
    /\ operations = <<>>
    /\ time = 0 \* Time starts at 0

(***************************************************************************)
(* State Machine                                                           *)
(***************************************************************************)

TimePasses ==
    /\ time' = time + 1
    /\ UNCHANGED <<serverStates, databaseState, blobStoreState, operations, 
                        cleanerStates>>

(***************************************************************************)
(* Server Writes                                                           *)
(***************************************************************************)

ServerStartWrite(s) ==
    /\ serverStates[s].state = "waiting"
    /\ \E u \in USERIDS, m \in METADATAS, i \in IMAGES:
        /\ serverStates' = [serverStates EXCEPT
                                ![s].state ="started_write",
                                ![s].userId = u, 
                                ![s].metadata = m,
                                ![s].image = i]
        /\ operations' = Append(operations, 
                                    [ 
                                       type |-> "WRITE",
                                       userId |-> u,
                                       metadata |-> m,
                                       image |-> i
                                    ])

    /\ UNCHANGED <<databaseState, blobStoreState, cleanerStates>>
    /\ UNCHANGED time


ServerWriteBlob(s) ==
    LET currentState == serverStates[s] 
    IN
    /\ currentState.state = "started_write"
    /\ \E id \in UUIDS:
        /\ blobStoreState[id] = [status |-> "UNSET", image |-> "UNSET"]
        /\ blobStoreState' = [blobStoreState EXCEPT 
                                ![id] = [
                                    image |-> currentState.image,
                                    created |-> time
                                    ]]
        /\ serverStates' = [serverStates EXCEPT
                                ![s].state ="wrote_blob",
                                ![s].imageId = id]
    /\ UNCHANGED <<databaseState, operations>>
    /\ UNCHANGED cleanerVars
    /\ UNCHANGED time

ServerWriteMetadataAndReturn(s) ==
    LET currentState == serverStates[s] 
    IN
        /\ currentState.state = "wrote_blob"
        /\ databaseState' = [databaseState EXCEPT 
                                ![currentState.userId] = [
                                    metadata |-> currentState.metadata, 
                                    imageId |-> currentState.imageId] ]

        /\ serverStates' = [serverStates EXCEPT
                                    ![s].state ="waiting",
                                    ![s].userId ="UNSET",
                                    ![s].metadata = "UNSET",
                                    ![s].image = "UNSET",
                                    ![s].imageId = "UNSET"]
        /\ UNCHANGED <<blobStoreState, operations>>
        /\ UNCHANGED cleanerVars
        /\ UNCHANGED time

ServerFailWrite(s) ==
    /\ serverStates[s].state \in {"started_write", "wrote_blob"}
    /\ serverStates' = [serverStates EXCEPT
                                ![s].state ="waiting",
                                ![s].userId ="UNSET",
                                ![s].metadata = "UNSET",
                                ![s].image = "UNSET",
                                ![s].imageId = "UNSET"]
    /\ UNCHANGED <<databaseState, blobStoreState, operations>>
    /\ UNCHANGED cleanerVars
    /\ UNCHANGED time


(***************************************************************************)
(* Server Reads                                                            *)
(***************************************************************************)

ServerStartRead(s) ==
    /\ serverStates[s].state = "waiting"
    /\ \E u \in USERIDS:
                serverStates' = [serverStates EXCEPT
                                    ![s].state ="started_read",
                                    ![s].userId =u]
   
    /\ UNCHANGED <<databaseState, blobStoreState>> 
    /\ UNCHANGED operations
    /\ UNCHANGED cleanerVars
    /\ UNCHANGED time

ServerReadMetadata(s) ==
    LET currentState == serverStates[s] 
    IN
    /\ currentState.state = "started_read"
    /\ databaseState[currentState.userId].metadata # "UNSET"
    /\ serverStates' = 
        [serverStates EXCEPT
            ![s].state ="read_metadata",
            ![s].metadata = databaseState[currentState.userId].metadata,
            ![s].imageId = databaseState[currentState.userId].imageId]
    /\ UNCHANGED <<databaseState, blobStoreState>>
    /\ UNCHANGED operations
    /\ UNCHANGED cleanerVars
    /\ UNCHANGED time

ServerReadMetadataAndReturnEmpty(s) ==
    LET currentState == serverStates[s] 
    IN
    /\ currentState.state = "started_read"
    /\ databaseState[currentState.userId].metadata = "UNSET"
    /\ serverStates' = [serverStates EXCEPT
                                ![s].state ="waiting",
                                ![s].userId ="UNSET",
                                ![s].metadata = "UNSET",
                                ![s].image = "UNSET",
                                ![s].imageId = "UNSET"]
                                            
    /\ operations' = Append(operations,
                            (***********************************************)
                            (* Returns an empty record                     *)
                            (***********************************************)
                            [ 
                               type |-> "READ",
                               userId |-> currentState.userId,
                               metadata |-> "UNSET",
                               image |-> "UNSET"
                            ])
    /\ UNCHANGED <<databaseState, blobStoreState>>
    /\ UNCHANGED cleanerVars
    /\ UNCHANGED time
    
ServerReadBlobAndReturn(s) ==
    LET currentState == serverStates[s] 
    IN
    /\ currentState.state = "read_metadata"                               
    /\ operations' = Append(operations,
                            [ 
                               type |-> "READ",
                               userId |-> currentState.userId,
                               metadata |-> currentState.metadata,
                               \* Looks up image by imageId
                               image |-> blobStoreState[currentState.imageId].image
                            ])
    /\ serverStates' = [serverStates EXCEPT
                            ![s].state ="waiting",
                            ![s].userId ="UNSET",
                            ![s].metadata = "UNSET",
                            ![s].image = "UNSET",
                            ![s].imageId = "UNSET"]
    /\ UNCHANGED <<databaseState, blobStoreState>>
    /\ UNCHANGED cleanerVars
    /\ UNCHANGED time

(***************************************************************************)
(* Cleaner States                                                          *)
(***************************************************************************)

(***************************************************************************)
(* This is the main change in the logic.                                   *)
(***************************************************************************)
CleanerStartGetBlobKeys(c) ==
    LET current == cleanerStates[c] IN
    /\ current.state = "waiting"
    /\ cleanerStates' = [
        cleanerStates EXCEPT
            ![c].state = "got_blob_keys",
            \* All keys in blockstore
            ![c].blobKeys = {
                k \in UUIDS:
                    LET earliestDeletionTime == blobStoreState[k].created + 2 IN
                    \* That are not unset
                    /\ blobStoreState[k] # [
                        status |-> "UNSET", 
                        image |-> "UNSET"] 
                    \* It must have been created 2 or more hours ago
                    /\ earliestDeletionTime =< time
            }
        ]
    /\ UNCHANGED <<serverStates, databaseState, blobStoreState, operations>>
    /\ UNCHANGED time

CleanerGetUnusedKeys(c) ==
    LET current == cleanerStates[c] IN
    /\ current.state = "got_blob_keys"
    /\ cleanerStates' = [
        cleanerStates EXCEPT
            ![c].state = "got_unused_keys",
            ![c].unusedBlobKeys = 
                {k \in current.blobKeys:
                    \A u \in USERIDS:
                        databaseState[u].imageId # k}
        ]
    /\ UNCHANGED <<serverStates, databaseState, blobStoreState, operations>>
    /\ UNCHANGED time

CleanerDeletingKeys(c) ==
    LET current == cleanerStates[c] IN
    /\ current.state \in {"got_unused_keys", "deleting_keys"}
    /\ Cardinality(current.unusedBlobKeys) # 0
    /\ \E k \in current.unusedBlobKeys:
        /\ blobStoreState' = 
            [blobStoreState EXCEPT 
                ![k] = [status |-> "UNSET", image |-> "UNSET"]]
        /\ cleanerStates' = [
            cleanerStates EXCEPT
                ![c].unusedBlobKeys = current.unusedBlobKeys \ {k}
            ]
    /\ UNCHANGED <<serverStates, databaseState, operations>>
    /\ UNCHANGED time

CleanerFinished(c) ==
    LET current == cleanerStates[c] IN
    /\ current.state = "deleting_keys"
    /\ Cardinality(current.unusedBlobKeys) = 0
    /\ cleanerStates' = [
        cleanerStates EXCEPT
            ![c].state = "waiting",
            ![c].blobKeys = {},
            ![c].unusedBlobKeys = {}
        ]
    /\ UNCHANGED <<serverStates, databaseState, blobStoreState, operations>>
    /\ UNCHANGED time

CleanerFail(c) ==
    LET current == cleanerStates[c] IN
    /\ current.state \in {"got_blob_keys", "got_unused_keys", "deleting_keys"}
    /\ cleanerStates' = [
        cleanerStates EXCEPT
            ![c].state = "waiting",
            ![c].blobKeys = {},
            ![c].unusedBlobKeys = {}
        ]
    /\ UNCHANGED <<serverStates, databaseState, blobStoreState, operations>>
    /\ UNCHANGED time

(***************************************************************************)
(* Specification / Next                                                    *)
(***************************************************************************)
Next ==
    \* Time can pass now
    \/ TimePasses
    \/  \E s \in SERVERS: 
            \/ ServerStartWrite(s)
            \/ ServerWriteBlob(s)
            \/ ServerWriteMetadataAndReturn(s)
            \/ ServerFailWrite(s)
            \/ ServerStartRead(s)
            \/ ServerReadMetadata(s)
            \/ ServerReadMetadataAndReturnEmpty(s)
            \/ ServerReadBlobAndReturn(s)
    \/ \E c \in CLEANERS:
            \/ CleanerStartGetBlobKeys(c)
            \/ CleanerGetUnusedKeys(c)
            \/ CleanerDeletingKeys(c)
            \/ CleanerFinished(c)
            \/ CleanerFail(c)



Spec == Init /\ [][Next]_vars


(***************************************************************************)
(* Invariants                                                              *)
(***************************************************************************)

\* Note that the success criteria hasn't changed this whole time

ConsistentReads ==
    \/ operations = <<>>
    \/ \A i \in 1..Len(operations):
        LET readOp == operations[i] IN
        \/  /\ readOp.type = "READ"
            /\  \/ \E j \in 1..i: 
                    LET writeOp == operations[j] IN
                    /\ writeOp.type = "WRITE"
                    /\ readOp.userId = writeOp.userId
                    /\ readOp.metadata = writeOp.metadata
                    /\ readOp.image = writeOp.image
                \/
                    /\ readOp.metadata = "UNSET"
                    /\ readOp.image = "UNSET"
        \/ readOp.type = "WRITE"

NoOrphanFiles ==
    ~\E k \in UUIDS:
        /\ blobStoreState[k] # [status |-> "UNSET", image |-> "UNSET"]
        /\ \A u \in USERIDS:
            databaseState[u].imageId # k

(***************************************************************************)
(* Properties                                                              *)
(***************************************************************************)

EventuallyNoOrphanFiles == <>NoOrphanFiles

AlwaysEventuallyNoOrphanFiles == []EventuallyNoOrphanFiles

StopAfter3Operations ==
    /\ Len(operations) <= 3
    /\ time <= 2

StopAfter5Operations ==
    Len(operations) <= 5

=============================================================================

Verifying Storage Cleaner

We’re going to start off with the slightly larger model (two servers and two cleaners), since the last test didn’t show behavioral differences. Might as well perform the more rigorous test.

Next Section Download Configuration

Invariant ConsistentReads is violated.

The error we saw previously is gone, implying we fixed the design flaw we hoped to fix. This new error is much more complex. It requires the Server to stall at just the wrong time and be out of commission for 2 hours. This is pretty unlikely; in fact, it’s unlikely enough that some companies might be okay with it. But the fix is obvious: kill the servers after 1 hour of stalling or less. Chances are we were going to do it anyway in implementation, but let’s model it to get the extra assurance.

A quick fix

All the changes in the model are in the server behavior. Despite the large number of changes, all we’re really saying is that if less than an hour has passed since the server request started, it can proceed to the next state. Otherwise, it proceeds to the restart state.

This can be reflected in an updated state diagram for Server writes:

WaitingStartWriteWriteMetadataServerRestartFailWriteWriteBlobAndReturnAssigns start timetimeout casetimeout casetimeout case

This is reflected in the code below.

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

(***************************************************************************)
(* Server Restart                                                          *)
(***************************************************************************)

ServerRestart(s) ==
    LET currentState == serverStates[s] IN 
    LET terminationTime == (currentState.start + 1) IN
    /\ currentState.state # "waiting" \* Server must be active
    \* This is the only state a server can reach if past termination time
    /\ time => terminationTime
    /\ serverStates' = [serverStates EXCEPT
                                ![s].state ="waiting",
                                ![s].userId ="UNSET",
                                ![s].metadata = "UNSET",
                                ![s].image = "UNSET",
                                ![s].imageId = "UNSET"]
    /\ UNCHANGED <<databaseState, blobStoreState, operations>>
    /\ UNCHANGED cleanerVars
    /\ UNCHANGED time

(***************************************************************************)
(* Server Writes                                                           *)
(***************************************************************************)

ServerStartWrite(s) ==
    /\ serverStates[s].state = "waiting"
    /\ \E u \in USERIDS, m \in METADATAS, i \in IMAGES:
        /\ serverStates' = [serverStates EXCEPT
                                ![s].state ="started_write",
                                ![s].userId = u, 
                                ![s].metadata = m,
                                ![s].image = i,
                                \* The time a write request starts
                                ![s].start = time
                                ]
        /\ operations' = Append(operations, 
                                    [ 
                                       type |-> "WRITE",
                                       userId |-> u,
                                       metadata |-> m,
                                       image |-> i
                                    ])
    \* Cleaner state needs to be added as unchanged for all server operations
    /\ UNCHANGED <<databaseState, blobStoreState, cleanerStates>>
    /\ UNCHANGED time

ServerWriteBlob(s) ==
    LET currentState == serverStates[s] IN
    LET terminationTime == (currentState.start + 1) IN
    /\ time < terminationTime \* Can only start this state if server is live
    /\ currentState.state = "started_write"
    /\ \E id \in UUIDS:
        /\ blobStoreState[id] = [status |-> "UNSET", image |-> "UNSET"]
        /\ blobStoreState' = [blobStoreState EXCEPT 
                                ![id] = [
                                    image |-> currentState.image,
                                    created |-> time
                                    ]]
        /\ serverStates' = [serverStates EXCEPT
                                ![s].state ="wrote_blob",
                                ![s].imageId = id]
    /\ UNCHANGED <<databaseState, operations>>
    /\ UNCHANGED cleanerVars
    /\ UNCHANGED time


ServerWriteMetadataAndReturn(s) ==
    LET currentState == serverStates[s] IN
    LET terminationTime == (currentState.start + 1) IN
    /\ time < terminationTime \* Can only start this state if server is live
    /\ currentState.state = "wrote_blob"
    /\ databaseState' = [databaseState EXCEPT 
                            ![currentState.userId] = [
                                metadata |-> currentState.metadata, 
                                imageId |-> currentState.imageId] ]

    /\ serverStates' = [serverStates EXCEPT
                                ![s].state ="waiting",
                                ![s].userId ="UNSET",
                                ![s].metadata = "UNSET",
                                ![s].image = "UNSET",
                                ![s].imageId = "UNSET"]
    /\ UNCHANGED <<blobStoreState, operations>>
    /\ UNCHANGED cleanerVars
    /\ UNCHANGED time

ServerFailWrite(s) ==
    LET currentState == serverStates[s] IN
    LET terminationTime == (currentState.start + 1) IN
    /\ time < terminationTime \* Can only start this state if server is live
    /\ serverStates[s].state \in {"started_write", "wrote_blob"}
    /\ serverStates' = [serverStates EXCEPT
                                ![s].state ="waiting",
                                ![s].userId ="UNSET",
                                ![s].metadata = "UNSET",
                                ![s].image = "UNSET",
                                ![s].imageId = "UNSET"]
    /\ UNCHANGED <<databaseState, blobStoreState, operations>>
    /\ UNCHANGED cleanerVars
    /\ UNCHANGED time


(***************************************************************************)
(* Server Reads                                                            *)
(***************************************************************************)

ServerStartRead(s) ==
    LET currentState == serverStates[s] IN
    /\ serverStates[s].state = "waiting"
    /\ \E u \in USERIDS:
                serverStates' = [serverStates EXCEPT
                                    ![s].state ="started_read",
                                    ![s].userId = u,
                                    \* The time a read request starts
                                    ![s].start = time
                                    ]
   
    /\ UNCHANGED <<databaseState, blobStoreState>> 
    /\ UNCHANGED operations
    /\ UNCHANGED cleanerVars
    /\ UNCHANGED time


ServerReadMetadata(s) ==
    LET currentState == serverStates[s] IN
    LET terminationTime == (currentState.start + 1) IN
    /\ time < terminationTime \* Can only start this state if server is live
    /\ currentState.state = "started_read"
    /\ databaseState[currentState.userId].metadata # "UNSET"
    /\ serverStates' = 
        [serverStates EXCEPT
            ![s].state ="read_metadata",
            ![s].metadata = databaseState[currentState.userId].metadata,
            ![s].imageId = databaseState[currentState.userId].imageId]
    /\ UNCHANGED <<databaseState, blobStoreState>>
    /\ UNCHANGED operations
    /\ UNCHANGED cleanerVars
    /\ UNCHANGED time


ServerReadMetadataAndReturnEmpty(s) ==
    LET currentState == serverStates[s] IN
    LET terminationTime == (currentState.start + 1) IN
    /\ time < terminationTime \* Can only start this state if server is live
    /\ currentState.state = "started_read"
    /\ databaseState[currentState.userId].metadata = "UNSET"
    /\ serverStates' = [serverStates EXCEPT
                                ![s].state ="waiting",
                                ![s].userId ="UNSET",
                                ![s].metadata = "UNSET",
                                ![s].image = "UNSET",
                                ![s].imageId = "UNSET"]
                                            
    /\ operations' = Append(operations,
                            [ 
                               type |-> "READ",
                               userId |-> currentState.userId,
                               metadata |-> "UNSET",
                               image |-> "UNSET"
                            ])
    /\ UNCHANGED <<databaseState, blobStoreState>>
    /\ UNCHANGED cleanerVars
    /\ UNCHANGED time
    
ServerReadBlobAndReturn(s) ==
    LET currentState == serverStates[s] IN
    LET terminationTime == (currentState.start + 1) IN
    /\ time < terminationTime \* Can only start this state if server is live
    /\ currentState.state = "read_metadata"                               
    /\ operations' = Append(operations,
                            [ 
                               type |-> "READ",
                               userId |-> currentState.userId,
                               metadata |-> currentState.metadata,
                               image |-> blobStoreState[currentState.imageId].image
                            ])
    /\ serverStates' = [serverStates EXCEPT
                            ![s].state ="waiting",
                            ![s].userId ="UNSET",
                            ![s].metadata = "UNSET",
                            ![s].image = "UNSET",
                            ![s].imageId = "UNSET"]
    /\ UNCHANGED <<databaseState, blobStoreState>>
    /\ UNCHANGED cleanerVars
    /\ UNCHANGED time

=============================================================================

Looks good, right? Let’s test it.

Next Section

Close but no cigar. Invariant ConsistentReads is violated.

We’ve gotten closer, and our error is even more obscure. Now it requires an interaction of Storage Cleaner, a Read Server, and a Write Server. But there’s a relatively simple fix.

Note: This was the first error that I did not expect. But it is exciting that TLA+ wouldn’t let me get away with it!



Next: (Implementing New Requirements) A working update