TLA+ spec for HHVM's live type-to-file reverse index

facts.tla

------------------------------- MODULE facts -------------------------------

EXTENDS Integers

CONSTANTS
    NumFiles,
    NumTypes,
    NumRequests,
    FinalClock

ASSUME
    /\ NumFiles \in Nat
    /\ NumTypes \in Nat
    /\ NumRequests \in Nat
    /\ FinalClock \in Nat

Files == 111+1..111+NumFiles
Types == 221+1..221+NumTypes

Empty == "empty"
Partial == "partial"
Complete == "complete"

----

(* --algorithm facts

variables
    watchman = [
        clock |-> 0,
        file_to_types |-> [f \in Files |-> {}]
    ],
    mem = [
        clock |-> 0,
        file_to_types |-> [
            f \in Files |-> [
                state |-> Empty,
                in |-> {}
            ]
        ],
        type_to_files |-> [
            t \in Types |-> [
                state |-> Empty,
                in |-> {},
                ex |-> {}
            ]
        ]
    ],
    db = [
        clock |-> 0,
        file_to_types |-> [f \in Files |-> {}]
    ],
    pending_db = [
        clock |-> 0,
        file_to_types |-> [f \in Files |-> {}]
    ];

define
    ChangedFiles ==
        CASE mem.clock = 0 /\ db.clock = 0 ->
            Files
        [] mem.clock = 0 /\ db.clock > 0 ->
            {
                f \in Files:
                    \/ mem.file_to_types[f].state = Empty
                    \/ db.file_to_types[f] /= watchman.file_to_types[f]
            }
        [] OTHER ->
            {
                f \in Files:
                    \/ mem.file_to_types[f].state = Empty
                    \/ mem.file_to_types[f].in /= watchman.file_to_types[f]
            }

end define;

process Request \in 1..NumRequests begin
Wait:
    await watchman.clock > 0;
RequestUpdate:
    while TRUE do
        mem.clock := watchman.clock ||
        mem.file_to_types := [
            f \in Files |->
                IF
                    f \in ChangedFiles
                THEN
                    [
                        state |-> Complete,
                        in |-> watchman.file_to_types[f]
                    ]
                ELSE
                    mem.file_to_types[f]
        ] ||
        mem.type_to_files := [
            t \in Types |-> [
                state |->
                    CASE mem.type_to_files[t].state /= Empty ->
                        mem.type_to_files[t].state
                    [] \E f \in ChangedFiles: t \in watchman.file_to_types[f] ->
                        Partial
                    [] OTHER ->
                        Empty,
                in |->
                    {
                        f \in Files:
                            CASE f \in ChangedFiles ->
                                t \in watchman.file_to_types[f]
                            [] OTHER ->
                                f \in mem.type_to_files[t].in
                    },
                ex |->
                    {
                        f \in Files:
                            CASE f \in ChangedFiles ->
                                /\ mem.type_to_files[t].state /= Complete
                                /\ t \in mem.file_to_types[f].in
                                /\ t \notin watchman.file_to_types[f]
                            [] OTHER ->
                                f \in mem.type_to_files[t].ex
                    }
            ]
        ];
FillFromDB:
        while TRUE do
            either
                goto RequestUpdate;
            or
                with f \in Files do
                    when mem.file_to_types[f].state /= Complete;
                    \* Call db.getFileTypes(f) and put its results in memory
                    mem.file_to_types[f] := [
                        state |-> Complete,
                        in |-> db.file_to_types[f]
                    ];
                end with;
            or
                with t \in Types do
                    when mem.type_to_files[t].state /= Complete;
                    \* Call db.getTypeFiles(t) and put its results in memory
                    mem.type_to_files[t] := [
                        state |-> Complete,
                        in |->
                            mem.type_to_files[t].in \union
                            {
                                f \in Files:
                                    /\ f \notin mem.type_to_files[t].ex
                                    /\ t \in db.file_to_types[f]
                            },
                        ex |-> {}
                    ];
                end with;
            end either;
        end while;
    end while;
end process;

process Watchman = 300 begin
ChangeFile:
    while watchman.clock < FinalClock do
        with f \in Files do
            with tys \in SUBSET Types do
                watchman.file_to_types[f] := tys ||
                watchman.clock := watchman.clock + 1;
            end with;
        end with;
MaybeTriggerDBUpdate:
        either
            goto ChangeFile;
        or
            pending_db := watchman;
        end either;
    end while;
end process;

process DBUpdate = 400 begin
UpdateDB:
    while TRUE do
        if pending_db.clock > db.clock then
            db := pending_db;
        end if;
    end while;
end process;

end algorithm; *)
\* BEGIN TRANSLATION (chksum(pcal) = "b132d214" /\ chksum(tla) = "36d6a71d")
VARIABLES watchman, mem, db, pending_db, pc

(* define statement *)
ChangedFiles ==
    CASE mem.clock = 0 /\ db.clock = 0 ->
        Files
    [] mem.clock = 0 /\ db.clock > 0 ->
        {
            f \in Files:
                \/ mem.file_to_types[f].state = Empty
                \/ db.file_to_types[f] /= watchman.file_to_types[f]
        }
    [] OTHER ->
        {
            f \in Files:
                \/ mem.file_to_types[f].state = Empty
                \/ mem.file_to_types[f].in /= watchman.file_to_types[f]
        }


vars == << watchman, mem, db, pending_db, pc >>

ProcSet == (1..NumRequests) \cup {300} \cup {400}

Init == (* Global variables *)
        /\ watchman =            [
                          clock |-> 0,
                          file_to_types |-> [f \in Files |-> {}]
                      ]
        /\ mem =       [
                     clock |-> 0,
                     file_to_types |-> [
                         f \in Files |-> [
                             state |-> Empty,
                             in |-> {}
                         ]
                     ],
                     type_to_files |-> [
                         t \in Types |-> [
                             state |-> Empty,
                             in |-> {},
                             ex |-> {}
                         ]
                     ]
                 ]
        /\ db =      [
                    clock |-> 0,
                    file_to_types |-> [f \in Files |-> {}]
                ]
        /\ pending_db =              [
                            clock |-> 0,
                            file_to_types |-> [f \in Files |-> {}]
                        ]
        /\ pc = [self \in ProcSet |-> CASE self \in 1..NumRequests -> "Wait"
                                        [] self = 300 -> "ChangeFile"
                                        [] self = 400 -> "UpdateDB"]

Wait(self) == /\ pc[self] = "Wait"
              /\ watchman.clock > 0
              /\ pc' = [pc EXCEPT ![self] = "RequestUpdate"]
              /\ UNCHANGED << watchman, mem, db, pending_db >>

RequestUpdate(self) == /\ pc[self] = "RequestUpdate"
                       /\ mem' = [mem EXCEPT !.clock = watchman.clock,
                                             !.file_to_types =                      [
                                                                   f \in Files |->
                                                                       IF
                                                                           f \in ChangedFiles
                                                                       THEN
                                                                           [
                                                                               state |-> Complete,
                                                                               in |-> watchman.file_to_types[f]
                                                                           ]
                                                                       ELSE
                                                                           mem.file_to_types[f]
                                                               ],
                                             !.type_to_files =                      [
                                                                   t \in Types |-> [
                                                                       state |->
                                                                           CASE mem.type_to_files[t].state /= Empty ->
                                                                               mem.type_to_files[t].state
                                                                           [] \E f \in ChangedFiles: t \in watchman.file_to_types[f] ->
                                                                               Partial
                                                                           [] OTHER ->
                                                                               Empty,
                                                                       in |->
                                                                           {
                                                                               f \in Files:
                                                                                   CASE f \in ChangedFiles ->
                                                                                       t \in watchman.file_to_types[f]
                                                                                   [] OTHER ->
                                                                                       f \in mem.type_to_files[t].in
                                                                           },
                                                                       ex |->
                                                                           {
                                                                               f \in Files:
                                                                                   CASE f \in ChangedFiles ->
                                                                                       /\ mem.type_to_files[t].state /= Complete
                                                                                       /\ t \in mem.file_to_types[f].in
                                                                                       /\ t \notin watchman.file_to_types[f]
                                                                                   [] OTHER ->
                                                                                       f \in mem.type_to_files[t].ex
                                                                           }
                                                                   ]
                                                               ]]
                       /\ pc' = [pc EXCEPT ![self] = "FillFromDB"]
                       /\ UNCHANGED << watchman, db, pending_db >>

FillFromDB(self) == /\ pc[self] = "FillFromDB"
                    /\ \/ /\ pc' = [pc EXCEPT ![self] = "RequestUpdate"]
                          /\ mem' = mem
                       \/ /\ \E f \in Files:
                               /\ mem.file_to_types[f].state /= Complete
                               /\ mem' = [mem EXCEPT !.file_to_types[f] =                         [
                                                                              state |-> Complete,
                                                                              in |-> db.file_to_types[f]
                                                                          ]]
                          /\ pc' = [pc EXCEPT ![self] = "FillFromDB"]
                       \/ /\ \E t \in Types:
                               /\ mem.type_to_files[t].state /= Complete
                               /\ mem' = [mem EXCEPT !.type_to_files[t] =                         [
                                                                              state |-> Complete,
                                                                              in |->
                                                                                  mem.type_to_files[t].in \union
                                                                                  {
                                                                                      f \in Files:
                                                                                          /\ f \notin mem.type_to_files[t].ex
                                                                                          /\ t \in db.file_to_types[f]
                                                                                  },
                                                                              ex |-> {}
                                                                          ]]
                          /\ pc' = [pc EXCEPT ![self] = "FillFromDB"]
                    /\ UNCHANGED << watchman, db, pending_db >>

Request(self) == Wait(self) \/ RequestUpdate(self) \/ FillFromDB(self)

ChangeFile == /\ pc[300] = "ChangeFile"
              /\ IF watchman.clock < FinalClock
                    THEN /\ \E f \in Files:
                              \E tys \in SUBSET Types:
                                watchman' = [watchman EXCEPT !.file_to_types[f] = tys,
                                                             !.clock = watchman.clock + 1]
                         /\ pc' = [pc EXCEPT ![300] = "MaybeTriggerDBUpdate"]
                    ELSE /\ pc' = [pc EXCEPT ![300] = "Done"]
                         /\ UNCHANGED watchman
              /\ UNCHANGED << mem, db, pending_db >>

MaybeTriggerDBUpdate == /\ pc[300] = "MaybeTriggerDBUpdate"
                        /\ \/ /\ pc' = [pc EXCEPT ![300] = "ChangeFile"]
                              /\ UNCHANGED pending_db
                           \/ /\ pending_db' = watchman
                              /\ pc' = [pc EXCEPT ![300] = "ChangeFile"]
                        /\ UNCHANGED << watchman, mem, db >>

Watchman == ChangeFile \/ MaybeTriggerDBUpdate

UpdateDB == /\ pc[400] = "UpdateDB"
            /\ IF pending_db.clock > db.clock
                  THEN /\ db' = pending_db
                  ELSE /\ TRUE
                       /\ db' = db
            /\ pc' = [pc EXCEPT ![400] = "UpdateDB"]
            /\ UNCHANGED << watchman, mem, pending_db >>

DBUpdate == UpdateDB

Next == Watchman \/ DBUpdate
           \/ (\E self \in 1..NumRequests: Request(self))

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

\* END TRANSLATION 

----

EachFileToTypeIsCorrectOrIncomplete ==
    \A f \in Files:
        mem.file_to_types[f].state = Complete =>
            mem.file_to_types[f].in = watchman.file_to_types[f]

EachTypeToFileIsCorrectOrIncomplete ==
    \A t \in Types:
        mem.type_to_files[t].state = Complete =>
            \A f \in Files:
                (
                    /\ f \in mem.type_to_files[t].in
                    /\
                        \/ mem.file_to_types[f].state /= Complete
                        \/ t \in mem.file_to_types[f].in
                ) = (
                    t \in watchman.file_to_types[f]
                )

----

(* Invariants *)

GetFileToTypeCorrect ==
    mem.clock = watchman.clock => EachFileToTypeIsCorrectOrIncomplete

GetTypeToFileCorrect ==
    mem.clock = watchman.clock => EachTypeToFileIsCorrectOrIncomplete
    
(* Properties *)

Liveness == <>(mem.clock = watchman.clock)

=============================================================================
\* Modification History
\* Last modified Wed Mar 17 01:20:05 PDT 2021 by jhemphill
\* Created Tue Mar 09 16:07:52 PST 2021 by jhemphill