>> Hello. My name is Ron Pressler.
By day, I work at Oracle and OpenJDK.
That's the main implementation of the Java platform.
But I've been working with TLA plus both
professionally and mostly as a hobby for several years.
This talk is intended is what I'll call a TLA plus Truffle.
Back in the '80s,
the computer scientist, Jon Bentley,
wrote a column in the Communications of
the ACM called Programming Pearls.
That way she wrote,
''Just as natural pearls grow from
grains of sand that has irritated oysters,
these programming pearls have grown from
real problems that have irritated programmers.
The programs are fun,
and they teach important programming techniques
and fundamental design principles.''
Years later, Richard Bird
edited a column in the similar vein in the Journal of
Functional Programming and explained that a pearl is not
original research or an industrial case study,
but an instructive example, a nifty presentation,
or an interesting application of
a technique that should be polished,
elegant, instructive, and entertaining.
The idea was borrowed elsewhere in
the form of graphics gems and perhaps others.
In the same spirit,
I'd propose TLA plus Truffles.
I don't promise to live up to those standards,
but I will try to offer something for everyone.
Some manipulation of formal logic,
some exploration of semantics,
some use of TLC,
and some interesting applications.
We have quite a journey ahead of us so let's begin.
As we all know, Leslie Lamport,
the inventor of TLA plus and the logic as its core.
The temporal logic of actions, or TLA,
recommends that system specifications
be written as state machines,
which in TLA are written as
the canonical formula of
an initial states predicate, a state transition,
or an action with a subscript that can be any state function,
but normally is a tuple containing
the variables mentioned in the formula,
and some fairness conditions.
This is very good advice.
Indeed, the TLC model checker that comes with the TLA plus
toolbox can only change TLA plus formulas of this canonical form.
But I would like to talk about a different shape of formula.
Show how it can be checked with
TLC albeit with some inconveniences,
and present three examples where such formulas could be useful.
A TLA formula F specifies a class of behaviors,
where a behavior in TLA,
as you should know, is an infinite sequence of states.
Each state a mapping from variables to values.
Our formula only mentions a finite small set of variables,
but the class of satisfied behaviors contain
those that assign any arbitrary value to any variable,
not mentioned in the formula at each state.
In other words, the formula describes all those behaviors of
an entire world that contains our system of interest.
If formula F describes a world containing one system,
and formula G a world containing another,
then a world containing both will
be an intersection of those worlds,
and it is described by the formula that is
the conjunction of F and G. In this way,
conjunction in TLA describes any form of
composition of two or more systems or components.
Or if they interact in any way,
then they must share some of the variables they mentioned.
That conjunction is such as simple expression of
composition in TLA has some immediate consequences.
For example, it has immediate results of
propositional logic that if F implies A,
meaning that the property A [inaudible] in Fs world,
and G implies B, then the conjunction of F
and G implies both A and B.
This is always true,
but we must be careful,
as it could be true vacuously.
The intersection of the two worlds could be empty if
the conjunction of the two formulas is equivalent to false.
This is the one downside of TLAs
elegant formalization of composition that I can think of.
Unfortunately, while it is possible to check if
a specific formula's equal to false in TLC,
TLC does not currently offer
a way to do it generally and automatically,
even though it could,
by allowing us to check if
the specification implies a false property.
I think it should and hope it will.
We will be looking at conjunctions of canonical forms.
They don't specify one state machine,
but a composition of two or possibly more.
This can be used to write a composed specification,
and we'll see one example of that.
But because TLA doesn't
distinguish between systems and properties,
it can also be used to specify and check interesting properties.
To be able to check such a formula in TLC,
we'll need to transform it into the canonical form.
In the next few slides,
I will use colors to distinguish clauses
rather than subscripts like init 1 and init 2.
I hope that will be cleared.
First, we rewrite our formula like so.
Then we see that most of it can
be easily copied into a canonical formula.
The initial saint predicate and the fairness conditions.
But the problem is the middle parts
containing the temporal operator and the action.
Because a canonical formula allows only one box action clause.
To rewrite the two box action clauses into one,
we'll use some logical identities.
Number 1, we know from
propositional logic that conjunction and
disjunction distribute to [inaudible] one another.
Number 2, we know that in temporal logic,
box A and box B is equal to box A and B.
Finally, we know in TLA,
box square brackets action_vars is
equal to box action or unchanged vars.
The shaded area has formulas that aren't well-formed in TLA,
but we can use them to make a correct deduction.
Using those identities, we can
rewrite the two box action clauses into one.
We get this, and then this well-formed TLA expression.
If one set of variables is contained in the other,
we can eliminate either the second or third disjunct
because it will equal false,
and if the two sets of variables are the same,
we can eliminate both and just remain with a first disjunct.
With this, we now know how to conjoin
two canonical formulas into one canonical formula in TLA.
What can we do in TLA plus,
and in particular, in a way that is checkable by TLC?
We begin by writing the result
from the previous slide as a definition.
But this doesn't quite work with TLC.
The reason is that when TLC evaluates an expression,
it requires that the first time it encounters a prime variable,
possibly after skipping arbitrary disjunct,
it must appear in the form x equals something,
or x is a member of something.
This might not be the case here in the second and third disjunct,
even if we write NextA and NextB carefully.
Fortunately, unchanged x is interpreted as x prime equals x.
All we need to do is change the order of our conjuncts.
We put unchanged first and we're done.
Instead of writing the first back,
we write the equivalent bottom one that
is canonical and it can be checked by TLC.
There might be some certainties with fairness, but to be honest,
fairness is not needed in the examples I'll show you,
so I didn't look into that and
I'll leave out fairness in the rest of the talk.
Now what if we want to compose more than two formulas?
We just repeat, this actually works.
By the way this is why I don't include the books in
square brackets in definition of composed.
That's the idea. Now what can we do with it?
The first use case I'd like to show is specifications in
the style of behavioral programming
invented by David Harel and his students.
Behavioral programming is a paradigm that
Harel believes could make going from
specification to implementation easier
in iterative and interactive process.
The idea is that we write a program by gradually
layering rules with different priorities on top of each other.
To change the program,
we add a new rule that refines is.
The rules are actually called behaviors or behavior threads,
each of which corresponds quite nicely
to a state machines specification in TLA,
and the layering of rules corresponds
to conjoining canonical formulas.
In this use case,
we are actually going to write
a specification as a conjunction of canonical formulas.
The paper gives an example of specifying
slash programming the game of Tic-Tac-Toe,
and using what I showed you,
I was able to specify the game until a plus in
the gradual iterative style of behavioral programming.
I will go over the example very quickly
just to give you a taste of the idea.
There is no need to carefully read the spec snippet on the slides,
I'll point out the important bits.
We begin by specifying a three-by-three board,
where each set if there is
a free square an X or an O piece is placed in it.
We can already say to property that says that
the fill square is never vacated and check it with TLC.
We then know a rule that enforces alternating terms,
first, X plays then O and so on.
This rule is expressed as
a separate state machine in the formula enforce turns,
which is then conjoined to the previous factor form
Tic-Tac-Toe 2 that we can
check once we apply the technique we learned.
We then add a rule, another state machine detect when,
that detects a win or a drawer.
We can again can join it to
Tic-Tac-Toe 2 and check some properties.
If we play like this,
the players making arbitrary moves,
this is a TLC output beget.
But now we start adding tactics,
each has its own rule and canonical formula that we can
join to the previous one and that we can check its every step.
First we say that if a player can complete
line by marking an empty square, they do it.
Then we add a rule that if we can block
the opponent from winning in the next turn,
we'll do it, but we give it
a lower priority than completing our own line in winning.
Then we add a lower priority rule,
that if the center square is free we place our square there.
Here for example, we can check that
the first move will always place a piece in the center square.
Finally, we add a rule with a lower priority,
so that says that if a corner is free place a piece there.
At these points, we can already check that the rules we
have so far will always lead to a draw.
To check each of these tabs,
we can join the spanks as we learned,
and this is the full spank containing all seven rules.
Checking it with all the interesting properties
takes only about seven seconds on my machine.
Obviously, there are fewer states
than when we play without tactics.
Now I don't know if this sounds
specification is helpful in TLA plus.
My conclusion from this particular example
is that perhaps not so much,
but maybe this specification is too simple,
you can find the full specification here and judge for yourself.
But I think it's cool that we can use TLC to check
at least some specifications that are
not in the canonical state machine style.
Here are some resources where you
can learn more about behavioral programming.
In the next example,
we're not going to use conjunction to write a specification,
but rather to check a special property
called a possibility property.
The idea is based on a paper by Leslie Lamport.
A possibility property asks,
''Is it always possible to get from
any reachable state of the system to some state P?''
In the paper, Lamport says that while
possibility properties are not as
important as safety or liveness properties,
they can be of interest as a sanity check.
TLA, being a linear temporal logic,
does not allow to directly express possibility,
but Lamport shows that if the possibility property holds,
it is always possible to find some new action
M with associated fairness G that restricts and directs
the state machines next state action
to take us from any ometer reachable state of
the system to the state P. This is
a process analogous to existential quantifier elimination,
and then this is a proposition we need to prove.
While the spec is given as a canonical formula,
the proposition isn't canonical.
We have a conjunction with another temporal subformula.
But unlike the previous example,
we have this diamond operator here,
but we can't get rid of it.
It means that at some points the M action starts occurring,
restricting the next action,
so we can recreate the same effect with
additional variable and another fairness condition.
We add a new Boolean variable T initialized to false,
and we add a fairness condition
that says that eventually it will become true,
this will trigger the operation of M. Now,
we have a conjunction of canonical formulas that we can check.
We then notice that the set of variables
vars is a subset of vars union t,
and so one of the disjuncts in the composition drops
off and after a few steps of
rewriting that I'm skipping, for example,
I wanted to take the unchanged t clause outside the parentheses,
so I introduced the sub-action trigger
that triggers the operation of
M. We get this canonical formula
and the proposition that we can then check in TLC.
I haven't actually tried this because
I don't have a good example to try it on.
But if you come up with one, send it my way.
In the final example,
we're also going to use conjunction,
not to specify but to check.
Only this time, it's not going to be
a property of the specification,
but of a real system.
One of the questions we often hear from TLA plus
newcomers and not just newcomers is,
how do I know that my system conforms to the specification?
While humanity currently lacks the technology to soundly verify
spec conformance on systems of
size that TLA plus is routinely use to specify,
perhaps there is some way to test conformance
that is more mechanical than just by inspection.
There might not be sound but at least could be
useful in effectively finding bugs in the implementation.
One such technique is called Model-Based Trace-Checking.
The idea is to gather logs of execution traces from a real system,
the implementation language doesn't matter,
and using model checker to find
inconsistencies between the traces in the specified model.
Of course, because its traces are finite,
we can only check for violations of safety properties.
In TLA, a specification G conforms with F, or implements F,
or refines F if the clause of behaviors
G allows is contained in those F allows.
Formally, this happens when G implies
F. This by the way is my favorite feature of TLA,
that the abstraction refinement relation
is expressed as ordinary implication.
We would be able to soundly check if a real system implementation
conforms with the spec if
all of it's behaviors are allowed by the spec.
Instead, we check that only some of it's behaviors,
those that come from execution traces
extracted from log files, satisfy the spec.
Just remember that a single trace
doesn't represent a single TLA behavior,
but a whole class.
Aside from matter of suturing,
the trace allows any unmentioned variable to take any value.
We're still talking about classes of
behaviors which we could then represent with a TLA plus formula.
Let's begin with a specification of a simple system.
We have a clock that goes tick tock.
Every time it ticks,
x and y are assigned an arbitrary value between zero and nine,
and every time it tocks,
z is assigned the sum of x and y.
TLC tells us that this system has 2,000 states.
For the purpose of demonstration,
I will embed the trace directly in the TLA
plus file as a sequence of tuples.
Of course, in real usage,
we'll probably want to write a TLC operator override in
Java that will read the trace directly from a log file,
and I believe some people have already written such operators and
contributed them to the TLA plus community modules.
We could write the formula that expresses
the trace as behaviors in TLA plus like so.
We instantiate the system spec,
we define a read operation,
we start by reading the first entry,
and then at each step,
we read another until there's none left.
There are several things that TLC doesn't like here.
It doesn't like the tuple equality in the initial [inaudible].
And it doesn't like a primed operator as
the first occurrence of a prime variable.
It also doesn't let us directly use Model!vars.
To make this work with TLC,
we write the formula in
a more cumbersome and less general way with
this Read and ReadNext definitions but it works.
Then to check conformance,
we simply check that this holds.
I want to point out two things here.
First, because we're only dealing with finite traces,
we can only check conformance with the safety part of the system.
We also turn off deadlock detection in TLC.
Second, because we're just checking the trace,
then it doesn't matter how complex our system spec is.
The number of states is determined by the trace, not the system.
The trace has 20 records and TLC
finds 20 states arranged linearly.
We can do even better and exploit
TLC to check many traces at once.
Suppose we have multiple log files.
Again, for the purpose of demonstration,
here I've embedded them in the TLA plus specification.
This is how we turn the traces into a formula.
The only thing that's changed from before is
I've added another index variable, log,
that is non-deterministically chosen at
the initial state and then remains unchanged during the behavior.
Again, we check and we get
a small state space that looks unsurprisingly like this.
So far so good,
but we haven't done anything interesting
with conjunction just yet.
Here the plot thickens.
Supposing a log file only
records some of the variables in our system.
For example, suppose it only logs a value of z.
Does such a trace conform to our spec nodes?
Does our model allow for such an observable behaviors of z?
We really want to check this with a variables x, y,
and tickTock, treated as hidden on observed variables.
It means that for every behavior and trace behavior,
there exists a corresponding behavior that satisfies Model!Safety
with matching values for z and some values for x, y, and tickTock.
But TLC can't check properties with temporal quantifiers.
So we need to get rid of it somehow.
Ordinarily, we'd eliminate the temporal
existential by constructing the sought-after behavior ourselves,
adding auxiliary variables in
a refinement mapping to fill in
the values for the hidden variables.
We read the trace as before.
But to turn it into a formula we can check against a system model,
we add an auxiliary variable tt that
adds a suturing step to mimic the ticks and the tocks.
Then we conjure appropriate values for x and y. This works.
But as those of you who tried it know,
adding a refinement mapping and
auxiliary variables is not always easy.
Ordinarily, we don't have a choice.
But in this case,
we can use the unique properties of a trace
combined with the power of conjunction to do the work for us.
This is what we want to check.
To use TLC, we must still eliminate that temporal quantifier,
but we wanted it automatically.
We notice something special about trace behavior.
Even though, as I mentioned,
it corresponds to some infinite class of behaviors,
we can think of it as
a single behavior as far as our variables are concerned.
This is a little hand-wavy and
the details include equivalence classes.
The proposition is true if Model!Safety contains trace behavior.
But because there is effectively
just one element and trace behavior,
this happens if and only if their conjunction is not empty.
This is analogous to a set with one element that is
contained in another set if and only
if their intersection is not empty.
That's equivalent to saying that it is
not a theorem that this conjunction is equal to false,
which is equivalent to saying that it is not
a theorem that the conjunction implies false.
Thanks to what we know,
this is something we can check.
We use the conjunction technique to define
the conjoin formula in a way that TLC can check,
and then we need to check that this is not false.
As I mentioned before,
TLC does not currently allow us to
check if a formula implies false.
I hope it will someday.
But that's okay because we can always find something equivalent.
We pick a property that must be true for every behavior,
so that asserting it isn't true is
equivalent to saying that our specification is false.
Because we want to show that this is not a theorem,
we challenge TLC to find a counterexample.
If it finds one, we know that the conjunction is not
empty and that our trace does conform to our system model,
and this is indeed what we find.
But notice what we get.
TLC explores many more states than there are in the trace,
but far fewer states than there are in
the system that I pasted here below for reference.
TLC finds a violation of
the incorrect assertion that our conjunction is
empty and that violation it finds matches our trace.
If you look at the error trace TLC produces,
it actually fills in conforming
values of the hidden variables for us.
It automatically a suturing steps for the ticks and the tocks,
and it automatically finds values for x and y.
You can find the full specification here.
How effective is this technique in finding bugs in the real world?
On the one hand, checking such a small portion of
all system behaviors seems like a stab in the dark.
On the other hand, perhaps
many translation bugs are shallow and surface quickly.
In any event, this technique might help localize
bugs when analyzing traces known to be faulty.
I'll leave it to others to find out and report.
You can find modules with TLC operators that
can read log files in the TLA plus community modules,
and an example of using
this technique in the wonderful walk-through
tutorial of the TLA plus tools by Markus Kuppe.
This is all. I hope you enjoyed.