2021-06-29
Over the last few days I've been learning and practicing more TLA+. If you don't know what TLA+ is, the best description is directly from the TLA+ website[1]: "TLA+ is a language for modeling software above the code level and hardware above the circuit level, especially concurrent and distributed ones". One can use TLA+ to formally specify systems (especially computer-based ones), and then you can use TLC to check if the system conforms to some a set of criteria. For example, in Ghostferry[2], which is a tool designed to perform live migration of data from one MySQL instance to another, the core algorithm is specified in TLA+ and TLC is used to ensure that the data is identical after the data migration process is complete. More information about TLA+ can be found at the Learn TLA+ website[3].
[3] Learn TLA+ website by Hillel Wayne
In this post, I would like to summarize what I've learned recently using temporal properties. I'll be doing this without introducing prerequisite TLA+ knowledge, for brevity. I assume you are comfortable with things like state predicates, and writing invariants. These are also my own notes, so there may be errors. Use at your own risk, and read Specifying Systems[4] when in doubt.
Until now, I've not explicitly written temporal properties. The only temporal property I've used is the invariant, which is a state predicate that is true for all states. This is great to assert that the system is in a valid state, but does not assert that the system will transition from one particular valid state to another. Since temporal properties can be used to assert that a sequence of states behave in a certain way, it can be used to assert this type of transitions. For example, an invariant can be the fact that if you have a burger from the restaurant, you (should) have paid for it. Other temporal properties you might want to assert is that if you paid money for a burger, a burger should eventually be delivered to you. This is incredibly useful for designing systems, as one usually want to know that things do eventually happen, if satisfying conditions are reached.
Consider the following toy PlusCal spec that is derived basically from the real spec that I was working on:
--fair algorithm TemporalExamples variable i = 1; begin step1: i := 2; step2: i := 3; step3: i := 2; end algorithm;
Although this is a toy example, the temporal properties written here are a simplified version of temporal properties I've written for a state machine whose state transitions requires distributed processes cooperating. The assertion of temporal properties allows me to ensure that state transitions do happen when certain criteria are met.
The state transition is obvious. The variable i goes from: 1 -> 2 -> 3 -> 2. We can write a few temporal properties:
1. Eventually, i will have the value 3, but does not have to remain at this value.
Eventually3 == <>(i = 3)
2. Eventually, i will have the value 2 and it will remain to be 2 thereafter.
Eventually2AndRemains2 == <>[](i = 2)
3. i = 1 "leads to" (~>) i = 2.
OneLeadsToTwo == (i = 1) ~> (i = 2)
4. i = 1 leads to i = 3.
OneLeadsToThree == (i = 1) ~> (i = 3)
So far, all of these temporal properties evaluates to TRUE, which I expected. However, I wrote a few more properties that evaluated to values that I didn't expect:
I want to write a formula to assert that i = 1 leads to i = 2 and i remains at 2 from there on out. This would mean the program would fail this temporal property. My original attempt was:
(i = 1) ~> [](i = 2)
This evaluates to TRUE instead of the FALSE that I wanted. This is because I didn't quite understand the leads to operator (~>). I took it at its English words instead of the precise, mathematical definition given on page 91 of Specifying Systems[4], which states that:
F ~> G == [](F => <>G)
== \A n \in Nat: (s^{+n} |= F) => (\E m \in Nat: (s^{+(n + m)} |= G))
Without going into it too much (for now), this is basically saying that for all states that satisfies F, there exists a state after it that satisfies G. Substituting F = (i = 1) and G = [](i = 2), we can see that F is satisfied for n = initial, and G is satisfied at n + m = step3. To fix this, I have to use the following formula:
OneLeadsToTwoAndRemainsTwoCorrect == /\ ((i = 1) ~> (i = 2)) /\ []((i = 2) => [](i = 2))
This evaluates to FALSE as expected, and will evaluate to TRUE if we change step2 to be i := 2.
I noticed that the following expression was also evaluating to TRUE:
(i = 4) ~> (i = 3)
Clearly, i never equals 4, so I would have imagined this formula to be FALSE. Once again, the answer is on page 11 of Specifying Systems[4]. The definition of ~> uses an imply operator =>, which has the boolean logic of:
+-------+-------+--------+ | P | Q | P => Q | +-------+-------+--------+ | TRUE | TRUE | TRUE | | TRUE | FALSE | FALSE | | FALSE | TRUE | TRUE | | FALSE | FALSE | TRUE | +-------+-------+--------+
Looking at the definition of F ~> G again we see:
F ~> G == [](F => <>G)
== \A n \in Nat: (s^{+n} |= F) => (\E m \in Nat: (s^{+(n + m)} |= G))
== \A n \in Nat: P => Q
Q == (s^{+n} |= F)
P == (\E m \in Nat: (s^{+(n + m)} |= G))
If the behavior F is never satisfied, then P => Q will always evaluate to TRUE. Since in our case F == (i = 4), which is never satisfied, which means the temporal formula will always evaluate to TRUE. If we need to ensure that i = 4 occurs, we need an additional condition and can write:
Eventually4AndThenLeadsTo3 == /\ <>(i = 4) /\ (i = 4) ~> (i = 3)
For the toy system, another tempting temporal property to write is that i = 2 leads to i = 3:
(i = 2) ~> (i = 3)
This evaluates to FALSE. The reason again can be found by looking at the definition of F ~> G = [](F => <>G). There are two instances of n when i = 2: n = step1 and n = step3. The case of (n = step1, n+m = step2) satisfies the formula F => <>G. For the case of n = step3, there is no state at time n + m that satisfies G (i = 3). Since the [] (always) operator expects that all cases evaluates to TRUE, this expression evaluates to FALSE.
If we actually want a property where if i = 2, it leads to i = 3 at least once, we need to assert that (informally) there exists a state such that i = 2 and at least one state after it has i = 3. Or more formally:
\E n \in Nat: (s^{+n} |= (i = 2)) /\ (\E m \in Nat: (s^{+(n+m)} |= (i = 3)))
This can be written via the eventual (<>) operator in TLA+ (see page 91 of Specifying Systems[4]):
TwoLeadsToThreeAtLeastOnce == <>((i = 2) /\ <>(i = 3))
So perhaps, ~> should be called the "always leads to" operator, as I originally thought it meant leads to at least once.
This expression actually suffers a small problem: it requires that i = 2 at some time, which is different from the ~> operator which doesn't require F to be true at any time. You can "fix" this via:
TwoLeadsToThreeAtLeastOnceOrNeverTwo == \/ ~<>(i = 2) \/ <>((i = 2) /\ <>(i = 3))
On page 88 of Specify Systems, there's the following sentence:
A state predicate, viewed as a temporal formula, is true of a behavior [(sequence of states)] iff [(if and only if)] it is true in the first state of the behavior.
This definition means that you can write a temporal property: i = 2 and it will evaluate to FALSE as the initial condition has i = 1. On its own, this is not super interesting, but it is interesting when you're expanding temporal formulas to their formal definition. For example, in section 3.2.3 of the Temporal Logic of Actions paper by Leslie Lamport[5], it was suggested that F ~> G == [](F => <>G) is very different from F => <>G, and the reason is left to the exercise to the reader. Performing this exercise gives me the following:
s |= (F => <>G) \* s is my short hand for sigma according to the book, which is a behavior. (s |= F) => (s |= <>G) \* By definition of =>, see page 92 of Specifying Systems
Since s |= F only checks if F is true for the first state of the behavior, or the initial state, it will evaluate to TRUE forever even if F becomes TRUE at some point in the future and G never becomes TRUE.
This also has interesting implications in the subclause within the expanded expression for the [] and <> operators. For example, it is my understanding that s^{+n} |= F is true iff the state at time n satisfies F. I'm not sure if I internalize this fully, tho.
Some other stuff I've learned:
Some other thoughts:
[4] The Temporal Logic of Actions paper by Leslie Lamport (Section 3.2.3)
[5] Specifying Systems 19 March 2020 version (Section 8.1)
[6] My email to the TLA+ mailing list
Tags: software, math, tla+, notes
Comments? Email me at shuhao >at< shuhaowu <dot> com.