Apalache trail tips: how to check your specs faster

Difficulty: Red trail – Medium

This tutorial collects tips and tricks that demonstrate the strong sides of Apalache.

Tip 1: Use TLA+ constructs instead of explicit iteration

The Apalache antipatterns mention that one should not use explicit iteration (e.g., ApaFoldSet and ApaFoldSeqLeft), unless it is really needed. In this tip, we present a concrete example that demonstrates how explicit iteration slows down Apalache.

In our example, we model a system of processes from a set Proc that are equipped with individual clocks. These clocks may be completely unsynchronized. However, they get updated uniformly, that is, all clocks have the same speed.

Let's have a look at the first part of this specification:

-------------------------- MODULE FoldExcept ----------------------------------
(*
 * This specification measures performance in the presence of an anti-pattern.
 *)

EXTENDS Integers, Apalache 

CONSTANT
    \* A fixed set of processes
    \*
    \* @type: Set(Str);
    Proc

VARIABLES
    \* Process clocks
    \*
    \* @type: Str -> Int;
    clocks,
    \* Drift between pairs of clocks
    \*
    \* @type: <<Str, Str>> -> Int;
    drift

As we can see, the constant Proc is a specification parameter. For instance, it can be equal to { "p1", "p2", "p3" }. The variable clocks assigns a clock value to each process from Proc, whereas the variable drift collects the clock difference for each pair of processes from Proc. This relation is easy to see in the predicate Init:

Init ==
    /\ clocks \in [ Proc -> Nat ]
    /\ drift = [ <<p, q>> \in Proc \X Proc |-> clocks[p] - clocks[q] ]

Further, we write down a step of our system:

\* Uniformly advance the clocks and update the drifts.
\* Constructing functions without iteration.
NextFast ==
    \E delta \in Nat \ { 0 }:
        /\ clocks' = [ p \in Proc |-> clocks[p] + delta ]
        /\ drift' = [ <<p, q>> \in Proc \X Proc |-> clocks'[p] - clocks'[q] ]

The transition predicate NextFast uniformly advances the clocks of all processes by a non-negative number delta. Simultaneously, it updates the clock differences in the function drift.

It is easy to see that drift actually does not change between the steps. We can formulate this observation as an action invariant:

\* Check that the clock drifts do not change
DriftInv ==
    \A p, q \in Proc:
        drift'[p, q] = drift[p, q]

Our version of NextFast is quite concise and it uses the good parts of TLA+. However, new TLA+ users would probably write it differently. Below, you can see the version that is more likely to be written by a specification writer who has good experience in software engineering:

\* Uniformly advance the clocks and update the drifts.
\* Constructing functions via explicit iteration. More like a program.
NextSlow ==
    \E delta \in Nat \ { 0 }:
        /\  LET \* @type: (Str -> Int, Str) => (Str -> Int);
                IncrementInLoop(clk, p) ==
                [ clk EXCEPT ![p] = @ + delta ]
            IN
            clocks' = ApaFoldSet(IncrementInLoop, clocks, Proc)
        /\  LET \* @type: (<<Str, Str>> -> Int, <<Str, Str>>)
                \*          => <<Str, Str>> -> Int;
                SubtractInLoop(dft, pair) ==
                LET p == pair[1]
                    q == pair[2]
                IN
                [ dft EXCEPT ![p, q] = clocks'[p] - clocks'[q] ]
            IN
            drift' = ApaFoldSet(SubtractInLoop, drift, Proc \X Proc)

The version NextSlow is less concise than NextFast, but it is probably easier to read for a software engineer. Indeed, we update the variable clocks via a set fold, which implements an iteration over the set of processes. What makes it easier to understand for a software engineer is a local update in the operator IncrementInLoop. Likewise, the variable drift is iteratively updated with the operator SubtractInLoop.

If ApaFoldSet looks unfamiliar to you, check the page on folding sets and sequences.

Although NextSlow may look more familiar, it is significantly harder for Apalache to check than NextFast. To see the difference, we measure performance of Apalache for several sizes of Proc: 3, 5, 7, and 10. We do this by running Apalache for the values of N equal to 3, 5, 7, 10. To this end we define several model files called MC_FoldExcept${N}.tla for N=3,5,7,10. For instance, MC_FoldExcept3.tla looks as follows:

--------------------- MODULE MC_FoldExcept3 ---------------------------------

Proc == { "p1", "p2", "p3" }

VARIABLES
    \* Process clocks
    \*
    \* @type: Str -> Int;
    clocks,
    \* Drift between pairs of clocks
    \*
    \* @type: <<Str, Str>> -> Int;
    drift

INSTANCE FoldExcept    

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

We run Apalache for different instances of N:

apalache-mc check --next=NextSlow --inv=DriftInv MC_FoldExcept${N}.tla
apalache-mc check --next=NextFast --inv=DriftInv MC_FoldExcept${N}.tla

The plot below shows the running times for the versions NextSlow and NextFast:

The plot speaks for itself. The version NextFast is dramatically faster than NextSlow for an increasing number of processes. Interestingly, NextFast is also more concise. In principle, both NextFast and NextSlow describe the same behavior. However, NextFast looks higher-level: It looks like it computes clocks and drifts in parallel, whereas NextSlow computes these functions in a loop (though the order of iteration is unknown). Actually, whether these functions are computed sequentially or in parallel is irrelevant for our specification, as both NextFast and NextSlow describe a single step of our system! We can view NextSlow as an implementation of NextFast, as NextSlow contains a bit more computation details.

From the performance angle, the above plot may seem counterintuitive to software engineers. Indeed, we are simply updating an array-like data structure in a loop. Normally, it should not be computationally expensive. However, behind the scenes, Apalache is producing constraints about all function elements for each iteration. Intuitively, you can think of it as being fully copied at every iteration, instead of one element being updated. From this perspective, the iteration in NextSlow should clearly be less efficient.