TLA+ with concurrency

Graham Hay

Last time, we built a specification for a simple state machine. We can add some concurrency, by providing a list of customers, each with their own account:

CONSTANTS Customers

The value will be provided in the config file:

Customers = {c1, c2}

This is a set, containing two customers. We can add more, but the search space will balloon dramatically, and the model checker will take far longer to run.

We now initialise the variables for each customer:

Init ==
    /\ state = [c \in Customers |-> "open"]
    /\ balance = [c \in Customers |-> 0]

You can think of those as a dictionary initialiser, with the same value for every customer:

State 1: <Initial predicate>
/\ state = (c1 :> "open" @@ c2 :> "open")
/\ balance = (c1 :> 0 @@ c2 :> 0)

And now, every time round the loop:

Next ==
   /\ \E customer \in Customers:
        \/ \E amount \in 1..10:
                Deposit(customer, amount)
        \/ \E amount \in 1..10:
                Withdraw(customer, amount)
        \/ Close(customer)
        \/ Reopen(customer)

We first pick a customer, and then an action to perform on their account. For example:

Init
Next
Deposit(c1, 5)
Next
Close(c2)
Next
Withdraw(c1, 3)
...

Each transition is also updated, to check the variables for that customer:

Deposit(customer, amount) ==
    /\ state[customer] = "open"
    /\ balance[customer] < 100
    /\ balance' = [balance EXCEPT![customer] = (balance[customer] + amount)]
    /\ UNCHANGED <<state>>

And the invariant is updated to check every balance:

NoNegativeBalance ==
    /\ \A customer \in Customers:
        balance[customer] >= 0

We can run this version, without any problems:

Computing initial states...
Finished computing initial states: 1 distinct state generated at 2023-03-09 15:53:06.
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 2.5E-9
  based on the actual fingerprints:  val = 7.4E-14
996601 states generated, 48400 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 27.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 16 and the 95th percentile is 2).
Finished in 02s at (2023-03-09 15:53:08)

But the more observant amongst you will have noted that there is no interaction between the accounts.

We can solve this, by adding a “transfer” transition:

  \/ \E from, to \in Customers, amount \in 1..10:
        Transfer(from, to, amount)

This is slightly more interesting, but because the transfer is done atomically, our model still succeeds. So, as a final flourish, we can instead queue the actual work for later.

Error: Invariant NoNegativeBalance is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ state = (c1 :> "open" @@ c2 :> "open")
/\ balance = (c1 :> 0 @@ c2 :> 0)
/\ transfers = {}

State 2: <Next line 50, col 5 to line 57, col 23 of module bank>
/\ state = (c1 :> "open" @@ c2 :> "open")
/\ balance = (c1 :> 0 @@ c2 :> 1)
/\ transfers = {}

State 3: <Next line 50, col 5 to line 57, col 23 of module bank>
/\ state = (c1 :> "open" @@ c2 :> "open")
/\ balance = (c1 :> 0 @@ c2 :> 1)
/\ transfers = {[amount |-> 1, from |-> c2, to |-> c1]}

State 4: <Next line 50, col 5 to line 57, col 23 of module bank>
/\ state = (c1 :> "open" @@ c2 :> "open")
/\ balance = (c1 :> 0 @@ c2 :> 0)
/\ transfers = {[amount |-> 1, from |-> c2, to |-> c1]}

State 5: <Next line 50, col 5 to line 57, col 23 of module bank>
/\ state = (c1 :> "open" @@ c2 :> "open")
/\ balance = (c1 :> 1 @@ c2 :> -1)
/\ transfers = {}

Now customer 2 has £1 in their account, they write a check for c1, but sneakily empty their account before it is cashed.

Leave a comment