Modeling Redux with TLA+

Update 01/07/19

Greetings from 2019! The good news is that Chicago isn’t yet a radioactive crater. The bad news is almost everything I said about refinement in this article is wrong. I’m working on writing a more in-depth, rigorous treatment of refinement as its own article. But this one is currently explaining something that definitely isn’t refinement. mkay thanks!

Update 2020-10-05: I’m probably not going to write that article on refinement in the near future and also Chicago is a radioactive crater.

Someone suggested that I model Redux in TLA+ and here we are. I spent about twenty minutes reading Redux tutorials and ran this by a few friends, so hopefully I didn’t misunderstand it too much. This post also uses a few more advanced TLA+ topics: if you are unfamiliar with TLA+, it should be mostly followable, but I’d recommend checking out my piece on deployments too, which is much simpler. Also, this is more about exploring modeling than convincing Redux people to use formal methods. Consider this more an example than a practical tutorial.

Redux is a Javascript library for managing global state. You manage the state in three steps:

1. Various thingies send actions to Redux, consisting of the action type and any parameters you need.
2. Redux then runs the actions through your reducers, which are pure transformations on your state object.
3. Once all of the reducers run, Redux finishes by updating your store, which contains all of the state.

Actions are handled synchronously: there should never be a case where actions are “queued up” waiting for your last action to finish. My impression is that the main advantage of Redux is that the reducers create a “blessed” set of state mutations. All global mutations have to correspond with some registered action, which adds auditing and oversight to your changes. For this to work, though, you must only track and mutate global state through Redux. Otherwise you lose the benefits.

Here’s a simple redux app I stole from Glitch:

const { createStore } = require('redux')

const rootReducer = (state={counter: 0}, action) => {
  switch(action.type) {
    case 'INCR':
      return { counter: state.counter + 1 }
    case 'DECR':
      return { counter: state.counter - 1 }
    default:
      return state
  }
  //return state
}

const store = createStore(rootReducer)

module.exports = store

The message hits the reducers, which either increment or decrement your counter. This is what we’ll be modeling in TLA+. We’ll do two separate things with our spec. First we’ll implement the reduce-update component of Redux, then we’ll prove it refines a simpler design, and finally we’ll integrate it with other components of our spec. Reminder, TLA+ is a specification language, not a programming language. We do this to blueprint our system and find errors in our designs, not to confirm the code itself works.

Let’s start with the reducer.

---- MODULE redux_reducer ----
CONSTANT NULL

LOCAL INSTANCE Integers
LOCAL INSTANCE TLC
LOCAL ReducerActions == {"INC", "DEC"}

(* --algorithm redux
variables
  state = [stack |-> 0];
  action = NULL;

define
  TypeOk == 
    /\ action \in ReducerActions \cup {NULL}
    /\ state.stack \in 0..12 
end define;

begin
  ReduceAndUpdate: \* One step
    await action \in ReducerActions;
    state := 
      CASE action = "INC" -> "stack" :> (state.stack + 1) % 12
        [] action = "DEC" -> "stack" :> (state.stack - 1) % 12
      @@ state;
    action := NULL;
  goto ReduceAndUpdate;
end algorithm;*)
====

This is a fairly standard PlusCal algorithm. TypeOk is a type invariant: the action must be acceptable, and for simplification we’ll keep the stack in a preset range. The ReduceAndUpdate step waits for an incoming action, then updates the state. :> and @@ are both TLC utility operators: f @@ g merges functions f and g, where for f overrides g for shared keys. "stack" :> 0 is the function that only maps “stack” to 0. Together, this corresponds to an “update” to stack.¹

Why are we doing these in the same step? Shouldn’t we be returning a value and then updating state? Remember, ReduceAndUpdate corresponds to a single, uninterruptable step. There’s no way, using Redux, to do any concurrency tricks between the reduction and the update. There may be cases where something else does something side-effecty between those two that is dependent on the state. In that case, there’s difference between having one step or two, and we would want to use two separate steps. Here, though, I’m using one for simplicity.

Next we actually have to do something with this. There’s a few ways we can use it. The first that comes to mind is proving a refinement, where we show that our reducer “acts like” a more abstract system. The other is we can use it as a verified component as part of a larger spec we want to use. In both cases, we’d do this by creating another TLA+ file, instantiating the reducer, and proving some property. We’ll start with the refinement example.

Refinement

Redux is a way of managing global state by forcing us to go through the reducer. This should (should) be equivalent to having a global stack and directly updating it without using the action-reduce-update cycle. What we’ll do is model a global stack without the reducer, then run both it and the reducer version simultaneously. If they both always end up with the same stack, then the two should be equivalent.² Since Redux is more complicated, we can say it refines the global version. Careful refinement is one of the precious few ways we know of to prove code correct at scale.

Up until now we’ve been doing everything in PlusCal. I’m a big fan of PlusCal and think it’s the best place for most people to start. You can get quite a lot done with PlusCal, but it has some limitations. The big one here is that while it can be used as a component (with some finagling), it’s not designed to use other components with actions in them. In particular, we can’t import a PlusCal spec into another PlusCal spec. So our main spec will have to be done in TLA+.

---- MODULE redux ----
EXTENDS Integers, TLC, Sequences
CONSTANT NULL
VARIABLES stack, reducer_state, reducer_pc, action

ReducerActions == {"INC", "DEC"}

Reducer == INSTANCE redux_reducer WITH 
  pc <- reducer_pc,
  state <- reducer_state,
  action <- action

We start by creating the variables of the full system, including those of reducer component. Then we instantiate the reducer. This imports all of its possible actions as actions in the redux specification.³ Since ReduceAndUpdate is a valid action in the component, Reducer!ReduceAndUpdate is a valid action here. It will update the variables we injected in, so reducing will change the state of state too.

Also note the stack variable. This is completely unaffected by the reducer. It’s what will represent our “global” version.

\* some convenience stuff`
vars == << stack, reducer_state, reducer_pc, action >>
reducer_vars == << reducer_state, reducer_pc >>

TypeOk ==
  /\ Reducer!TypeOk
  /\ stack \in 0..11

Init == 
  /\ Reducer!Init
  /\ stack = 0

We establish that for the whole spec to be correct, it has to follow how Reducer would init its own values, as well as properly initialize the global stack.

Increase == 
  /\ stack' = (stack + 1) % 12
  /\ action' = "INC"

Decrease == 
  /\ stack' = (stack - 1) % 12
  /\ action' = "DEC"

Step ==
  /\ ~ENABLED Reducer!Next
  /\ \/ Increase
     \/ Decrease
  /\ UNCHANGED reducer_vars

Next == Step \/ (Reducer!Next /\ UNCHANGED stack)
Spec == Init /\ [][Next]_vars

Finally, we have our actions. These are the two possible transitions we can have: either we increase the stack or decrease it. In either case, we fire off the appropriate action to see what our reducer does. Notice that Step can’t affect the state variable, just as the Reducer can’t affect stack. The two systems manipulate their state independent of each other, communicating only with action. Also note that Step is only enabled when Reducer!Next isn’t. Our spec will wait for the reducer to complete its own actions before doing something else. Next and Spec, of course, cap us off.

As for the invariant: we’re running a Step, then a ReduceAndUpdate, then another Step, and so on and so forth. Each Step + ReduceAndUpdate makes a single cycle in our two specs. At the end of each cycle, both of the systems should have the same internal state of the stack. The invariant that comes to mind is

ENABLED Step <=> stack = reducer_state.stack

We can run this in TLC. If we do, we don’t get any errors, confirming that the systems are equivalent. To show what it looks like when this all fails, let’s change the Increase to modular on 13:

TypeOk ==
-  /\ stack \in 0..11
+  /\ stack \in 0..12

Increase == 
-  /\ stack' = (stack + 1) % 12
+  /\ stack' = (stack + 1) % 13
  /\ action' = "INC"

TLA+ is not only able to identify that the equivalence invariant has failed, it’s able to identify the series of steps that leads to the invariant failing.

Let’s change it back so we can demo how this practically works as a component.

Safe Global State

In order for Redux to “work”, you need to use it for all of your global state management. If you don’t, then all of the advantages - mutation bookkeeping, state history, etc - completely disappear. In practice you do this by being careful not to mutate state without using actions. This is extremely difficult to verify in your implementation. However, in your design, you can simply make a temporal property.

\* at the bottom of redux_reducer
SingleSourceOfTruth == [][
  (state' /= state) => ENABLED ReduceAndUpdate /\ (~ENABLED ReduceAndUpdate)'
]_state

This looks a little complicated, but it actually represents a simple idea. IF, in a given step, the value of state changes, THEN ReduceAndUpdate started the step enabled and ended it disabled. Since ReduceAndUpdate automatically disables itself, we can be reasonably assured that the ReduceAndUpdate step happened and updated the state.⁴ If the value of state did not change, then none of this matters and we’re fine.

This is a pretty powerful invariant: if we check that this temporal property holds, then even if we include the reducer in another spec and that spec updates the state, it still counts as a spec failure! The component is able to show that something else updated the global state without going through its channels. To demonstrate what a failure looks like, let’s add a new “Reset” action to our main spec.

+ Reset ==
+   /\ stack' = 0
+   /\ action' = NULL
+   /\ reducer_state' = [stack |-> 0]
+   /\ UNCHANGED reducer_pc

- Next == Step \/ (Reducer!Next /\ UNCHANGED stack)
+ Next == Step \/ Reset \/ (Reducer!Next /\ UNCHANGED global_vars)

Reset puts everything back to the start: our stack is zero, our state is zero, our action is zero, and our reducer pc doesn’t change (since it’s always on the same action anyway). If we run this, though, we get an error:

Reset updates the stack. Since that didn’t happen through ReduceAndUpdate, our spec fails. This works no matter how many components our spec has and how they are integrated.

Conclusion

While I mostly use it for verifying designs, TLA+ is a very versatile tool. Our example was pretty simple but we could easily extend it to more complex cases, like multiple reducers or async actions. What really interested me about this, though, was how specifying Redux helped me understand it. Redux is usually presented as a pretty complicated topic to “get”, but the JS folk I talked to said this spec mostly matches how Redux is supposed to work. Comprehension is one of the major benefits of specification; it’s just less visceral than formally verifying properties.

If you’re interested in learning the basics of TLA+, I wrote a free online tutorial that focuses on day-to-day use. I’m also working on a full book, but that won’t out for a few more months. Oh hey look here

Thanks to Greg Wilson, Craig Bass, and Jeff Auriemma for their feedback!