“Temporal logic of actions (TLA) is a logic developed by Leslie Lamport, which combines temporal logic with a logic of actions. It is used to describe behaviours of concurrent systems.” [1]
TLA+ is a formal specification language built on top of the TLA logic. It is used to design and verify the correct behavior of programs and is especially useful in distributed and concurrent systems. PlusCal is a formal specification language as well that gets transcompiled to TLA+. It is used to specify algorithms.
TLA, TLA+ and PlusCal were all developed by Leslie Lamport, whom offers free courses on his website . This article intends to give a brief overview what TLA+ and PlusCal are useful for and what not and wants to encourage every reader to head to Mr. Lampert’s website check out his tutorials.
A brief word about the tutorials, Mr. Lamport provided a TLA+ video course, that is also mirrored to Youtube. The PlusCal tutorial is in written form. Both are on point and easy to understand.
TLA+ and PlusCal development can be done with the provided TLA+ Toolbox. VS Code offers a TLA+ addon as well, but it obviously differs from the Toolbox view and can make things unnecessary hard for beginners.
Even tough the TLA+ and PlusCal community is not large both languages are used to validate and develop critical systems at Amazon, Microsoft and Intel.
TLA+:
To visualize the TLA+ syntax we will solve the Die Hard 3 4 gallons of water problem (as does Leslie Lamport in his tutorials, but different).
The problem states that the protagonists have a 3 and a 5 gallon water jug and they need to get exactly 4 gallons of water, but there are no markings or other external help.
To start tackling the problem with TLA+ we need to start our Toolbox and add/create a new spec. To do that click on “File”, “Open Spec” and “Add New Spec”. I named the spec “DieHard”.
To work with integers we need to import them with adding “Integers” to the extends key word.
EXTENDS TLC, IntegersBefore we define our functions we first need to define what variables we do have. In this case we have two, on for each jug of water.
VARIABLES small, bigWhen we want to refer to a variable in the next state we need to add a ” ‘ ” sign to the variable. Like this: small'.
Functions in TLA+ are not what programmers are used to most of the time. They are logical formulas that are either true or false. If a function is false it can not be executed. Functions can consist of sub functions. When a function consists of multiple sub functions that are true, each one of them could be executed and the Model Checker will evaluate any possibilities.
For every TLA+ project two function have to be defined. The Init defines the initial values and therefor state and the Next function updates the state every step. It is convention to name the Init and Next function Init and Next, but you could specify it in the Toolbox.
If the Next function evaluates to false there is no valid next step and we hit a deadlock.
In this case or Init function would set our two variables to 0.
Init == (small = 0) /\ (big = 0)Notice that our function name is followed by a double ==. After that there are two conditions separated by an TLA+ representation of an &&.
For our Next function we need to know what kind of state changes (actions) are possible.
In our scenario we could either fill the small or the big jug, empty one of them or fill the contents of one of them into the other.
With that we could define our Next function based on the sub functions:
Next == (FillSmall) \/ (FillBig) \/ (EmptySmall) \/ (EmptyBig) \/ (SmallToBig) \/ (BigToSmall)For readability purposes does TLA+ also support the following syntax:
Next == \/ FillSmall
\/ FillBig
\/ EmptySmall
\/ EmptyBig
\/ SmallToBig
\/ BigToSmallFill and empty both jugs is straight forward:
FillSmall == (small' = 3) /\ (big' = big)
FillBig == (small' = small) /\ (big' = 5)
EmptySmall == (small' = 0) /\ (big' = big)
EmptyBig == (small' = small) /\ (big' = 0)The functions filling water from one jug to the other are similar to each other but more complex than the previous ones.
To get a better understanding what we want to write in code we should check what possible cases there are.
In case of a SmallToBig we should check if there are less or equal than the capacity limit of the 5 gallon in both jugs. If yes we know that the small jug will be empty in the next step and the value of the big jug in the next step is the sum of both jugs now. If the sum of both jugs is greater than the capacity limit of 5, then we know big’ will be 5 and the small jug can fill the amount of water to the big jug, that the big jug is missing to get to max capacity. In TLA+ it looks like that:
SmallToBig == IF big + small =< 5
THEN /\ small' = 0
/\ big' = big + small
ELSE /\ small' = small - (5 - big)
/\ big' = 5TLA+ relies on spacing to handle encapsulated IFs, as well as functions separated by ands, or ors and no parenthesis.
Similar to SmallToBig is BigToSmall:
BigToSmall == IF big + small =< 3
THEN /\ big' = 0
/\ small' = big + small
ELSE /\ big' = small - (3 - big)
/\ small' = 3Now we’re done writing the spec, but we do not check if our variables are always in defined states.
For this we could add another function (I called it TypeOk, like Mr. Lamport):
TypeOk == (small \in 0..3) /\ (big \in 0..5)To make sure the checker watches the TypeOk function we need to add it as Invariant to the Model.
To do that click on “TLC Model Checker” and “New Model”. There you’ll see that the IDE has already filled in our Init and Next function as function to be executed for Init and Next. Now click on “What to check”, “Invariants” and “Add” to type in “TypeOk”.
With that the TLC Model Checker will check that the TypeOk function is never false.
Now we have a model to check but we are missing one thing. We never specified that our program should stop when big = 4. To do that we add another Invariant and write this time big /= 4. After that we can click on the small green arrow “run”.
Now the TLC Model Checker should run and finish with an error: “Invariant big /= 4 is violated.”. That means we found a solution to our predefined problem! In the error trace will be an example with the fewest steps required to create the situation that violated the invariant.
The whole spec looks like that:
---- MODULE dieHard ----
EXTENDS TLC, Integers
VARIABLES small, big
Init == (small = 0) /\ (big = 0)
TypeOk == (small \in 0..3) /\ (big \in 0..5)
FillSmall == (small' = 3) /\ (big' = big)
FillBig == (small' = small) /\ (big' = 5)
EmptySmall == (small' = 0) /\ (big' = big)
EmptyBig == (small' = small) /\ (big' = 0)
SmallToBig == IF big + small =< 5
THEN /\ small' = 0
/\ big' = big + small
ELSE /\ small' = small - (5 - big)
/\ big' = 5
BigToSmall == IF big + small =< 3
THEN /\ big' = 0
/\ small' = big + small
ELSE /\ big' = small - (3 - big)
/\ small' = 3
Next == \/ FillSmall
\/ FillBig
\/ EmptySmall
\/ EmptyBig
\/ SmallToBig
\/ BigToSmall
====PlusCal:
In contrast to TLA+ that is intended to model system based on their states, PlusCal is intended to model and check algorithms.
PlusCal has to different types of syntax. The prolix p-syntax and the more compact c-syntax [2]. We will use the c-syntax here because it is more natural to programmers.
In this example we will check a simple banking algorithm for bugs. The example is from https://learntla.com/introduction/example/, another great resource to learn TLA+ and PlusCal!
In this scenario we have to persons with bank accounts. Alice and Bob. Alice can transfer money to bob, but can not send more money than what she has. To make our example more interesting we make the algorithm execution concurrent.
PlusCal Code is written inside the TLA+ spec, encapsulated in a block comment. It is only allowed to have one PlusCal algorithm per spec file.
To check our algorithm we need to open our Toolbox IDE and click on “File”, “Open Spec”, “Add New Spec” and give it a name.
In our first line we need to import Integers like this: EXTENDS Integers. After that we can start our PlusCal algorithm block comment:
EXTENDS Integers
(* --algorithm bank_account {
// in algorithm block comment
}
end algorithm; *)Our algorithm needs to be placed in between the brackets. First of all we should define our variables and their values. We do that with the key word “variables” and at the end we add a semicolon.
variables alice_account = 10, bob_account = 10,
transfer_amount_1 \in 1..20,
transfer_amount_2 \in 1..20; As we stated before we want our algorithm to be executed concurrent. To specify that we need to encapsulate our code with brackets after the “process” key word.
process (Transfer_1 = 1) {
Condition_1:
if (alice_account >= transfer_amount_1) {
Do_Transfer_1:
alice_account := alice_account - transfer_amount_1;
bob_account := bob_account + transfer_amount_1;
}
}In the first line you see a so called label. It forces the execution to be atomic in the spacing indicated block or until the next label. In this case it forces the atomic execution until the next label “Do_Transfer_1”. The if statement and the lines below are trivial.
To get a second process to execute the same code we can add a second, slightly modified process block below the first one.
process (Transfer_2 = 2) {
Condition_2:
if (alice_account >= transfer_amount_2) {
Do_Transfer_2:
alice_account := alice_account - transfer_amount_2;
bob_account := bob_account + transfer_amount_2;
}
}The full spec looks like this:
---------------------------- MODULE bank_account ----------------------------
EXTENDS Integers
(* --algorithm bank_account {
variables alice_account = 10, bob_account = 10,
transfer_amount_1 \in 1..20,
transfer_amount_2 \in 1..20;
process (Transfer_1 = 1) {
Condition_1:
if (alice_account >= transfer_amount_1) {
Do_Transfer_1:
alice_account := alice_account - transfer_amount_1;
bob_account := bob_account + transfer_amount_1;
}
}
process (Transfer_2 = 2) {
Condition_2:
if (alice_account >= transfer_amount_2) {
Do_Transfer_2:
alice_account := alice_account - transfer_amount_2;
bob_account := bob_account + transfer_amount_2;
}
}
}
end algorithm; *)
=============================================================================Now that we have our PlusCal code, but we still can not check if the algorithm has any errors. To do that we need to transcompile it to TLA+ with “ctrl + T” or under “Files”, “Translate PlusCal Algorithm”.
With the TLA+ spec we now need to create a model as well as add our condition (alice_bank account >= 0) as invariant.
This is done as before by clicking “TLC Model Checker”, “New Model”, “ok” and “Invariants”, “Add”.
Now we can finally test our algorithm by clicking on the green button on the model site.
Our results show that our program has bugs and violates the invariant “alice_account >= 0”. It also shows the least amounts of steps to reproduce the bug. In this case the problem is, that we do atomic actions to check the account balance and update the balance, but we need to make the check and the update one atomic execution.
To fix this we need to remove the second label in both process blocks.
Useful Usage:
TLA+:
TLA+ is most useful in modeling and validating concurrent and/or distributed systems, where it is not absolutely clear in which order which steps are executed. On the other hand in systems that are not concurrent and run on only one computer it can not utilize its advantages.
PlusCal:
PlusCal is very useful in verifying and developing algorithms used by concurrent systems and it is a bit easier to write for programmers than TLA+.
Summary:
In this blog entry we have seen how useful TLA+ and PlusCal are when designing and testing distributed and/or concurrent systems and how easy they are to pick up. Even though the community is not large, there are no excuses to not learn both languages when designing distributed systems is part of your job.
To get you hooked up there is the first video of the TLA+ video course:
Leave a Reply
You must be logged in to post a comment.