Search code examples
tla+

Specifying liveness so a cycle doesn't happen in TLA+

I'm writing a specification of a simple client-server interaction to learn TLA+:

-------------------------------- MODULE Bar --------------------------------
VARIABLES
    sessionOK, \* if session is OK or expired
    msg        \* message currently on the wire

vars == <<msg, sessionOK>>

TypeOK ==
    /\ sessionOK \in {TRUE, FALSE}
    /\ msg \in {
         "Query",
         "OK",
         "Unauthorized",
         "null"
       }

Init ==
    /\ msg = "null"
    /\ sessionOK = FALSE

Query ==
    /\ msg \in {"null", "OK"}
    /\ msg' = "Query"
    /\ UNCHANGED <<sessionOK>>

OK ==
    /\ msg = "Query"
    /\ sessionOK = TRUE
    /\ msg' = "OK"
    /\ UNCHANGED <<sessionOK>>

Unauthorized ==
    /\ msg = "Query"
    /\ sessionOK = FALSE
    /\ msg' = "Unauthorized"
    /\ UNCHANGED <<sessionOK>>

Authorize ==
    /\ msg = "Unauthorized"
    /\ msg' = "null"
    /\ sessionOK' = TRUE

Expire ==
    /\ sessionOK = TRUE
    /\ sessionOK' = FALSE
    /\ UNCHANGED <<msg>>

Next ==
    \/ Query
    \/ Unauthorized
    \/ OK
    \/ Authorize
    \/ Expire

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

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

As you can hopefully see the client can run some query against a server, and if the session is OK, it will get a result, otherwise it gets a message that it needs to authorize and then retry. The session can expire at any time.

I want to ensure that the client eventually will get a result, so I added this line to properties:

(msg = "Query") ~> (msg = "OK")

Upon model checking, I'm confronted with a counter-example going like this: Init -> (Query -> Unauthorized -> Authorize -> Expire), with the part in parentheses repeating indefinitely. My first thought was to make a strong fairness requirement on OK step. However the problem is in this scenario OK step is never enabled.

I could add things like []<><<OK>>_vars (which reads "it's always the case that eventually OK occurs"), but this feels like cheating, and from what I gather specifying liveness using arbitrary temporal formulas -- and not weak or strong fairness -- is frowned upon.

How can I use weak or strong fairness to guarantee that a query will eventually get a response? Or maybe my model is bad? I'm out of ideas...

Solution

  • I'm answering my own question. If anyone thinks they have a better answer, please share.

    I found this aptly-named thread How to test a process eventually succeeds after indefinite number of retries?, where Leslie Lamport himself points out we can just assert fairness on a conjuction of an action and some other formula. In our scenario Spec then looks like this:

    Spec ==
    /\ Init
    /\ [][Next]_vars
    /\ WF_vars(Next)
    /\ SF_vars(OK)
    /\ SF_vars(Query /\ (sessionOK = TRUE))

    Now, what do each of these formulas in conjuction mean? The first three are quite obvious and were included in my attempt at defining Spec.

    1. Init is true on the first state of the behaviour.
    2. Next is true for every step of the behaviour (with stuttering allowed).
    3. Next will continue to occur if it continues to be enabled indefinitely, so a system doesn't come to a stop in the middle of message exchange.

    Fourth one was my intuition: it fixes the situation where the query is made, and then the session expires.

    1. If OK is repeatedly enabled (possible to happen) then it will eventually happen.

    And fifth is what was missing: it fixes the situation where OK was never enabled in the first place, because the session expired before the Query could happen.

    1. If it is repeatedly the case that Query can happen and the session is valid at the same time, it will eventually happen.