The effect of symmetry sets on TLC performance

[Ron Pressler]

Hi.

When one of my models took what I thought is an inordinate amount of time to model-check, I've decided to profile the TLC run (with a good, honest, profiler), and the result was surprising (to me at least):

Over 99.5% of the time is spent creating permutation states (I obtained similar result when I profiled the initial state computation, doInit). My model has 3 permutation states, two of size 3 and one of size 6, so if I gain a reduction of ~50x in the number of states TLC has to visit, it's taking (well) over 200x of it back due to the TLC implementation, in particular, the various implementations of permute() in Value's subclasses. 

Getting rid of all symmetries, increased the performance (very) significantly, and yields what seems to be a healthier profile:

Later, I found a sweet-spot of a single symmetry set of size 3 which seemed to yield the best performance.

Is there a way to improve the implementation(s) of permute()? A quick glance at the code showed what may possibly be way too many allocations (in tuples and record) due to what seems like an overly eager allocation policy (e.g. arrays are allocated before even a single permuted element is found). But as all that's required of the permutations is a fingerprint, perhaps a more substantial optimization may be possible.

Ron

[Markus Alexander Kuppe]

On 02.12.2015 13:23, Ron Pressler wrote:
> Is there a way to improve the implementation(s) of permute()? A quick
> glance at the code showed what may possibly be way too many allocations
> (in tuples and record) due to what seems like an overly eager allocation
> policy (e.g. arrays are allocated before even a single permuted element
> is found). But as all that's required of the permutations is a
> fingerprint, perhaps a more substantial optimization may be possible.

Hi Ron,

those are interesting findings. Can you send me a (stripped down)
spec/model that exemplifies the performance problem?

Thanks
Markus

[Michael Leuschel]

Hi Markus and Ron,

our experience using the TLC’s symmetry reduction was also mixed.

The extended version of our iFM’2012 paper contains a few example models where we did try TLC’s symmetry reduction:

  http://stups.hhu.de/w/Special:Publication/HansenLeuschelTLA2012

Greetings,

Michael 

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Ron Pressler]

Don't know about a stripped-down spec (it's quite large), but I could send you (for the time being only privately) the actual spec+model. What email address should I send it to?

Ron

[Ron Pressler]

I've thought of the problem some more, and think I have more insight:

1. The current approach actually computes all permuted states from each reachable state by performing the permutations, but storing only a (deterministically) selected representative. This assumes that building such steps through permutations is faster than reaching it through a next step. The difference, however, is not as big as it can be, which can make this optimization not powerful enough or even somewhat harmful, and potentially very harmful in light of point 2.

2. It is possible (and is indeed the case in my model) that many of the permuted states -- while valid -- are not actually reachable. This means that the optimization computes many more states than would have been computed through reachability alone, and due to 1, it is sensitive to even to non-extreme correlations between symmetry sets. As an example, we can have two symmetry sets {a, b, c} and {x, y, z} that are both valid but are strongly correlated in the model which may ensure that in all reachable states, `a` always maps to `x`, `b` to `y` and `c` to `z`. Which means that the optimization will compute 9 steps, while only 3 are actually reachable (i.e. 3x states). As the computation via permutation is less than 3 times faster than computation via next-step, the result is a net loss which may be large.

Problem 1 may be solved through a different implementation of permute(), preferably one that doesn't allocate an actual complete state for each permutation.

Problem 2 may be solved by letting the user supply a predicate which would validate reachable compund permutations. In the example above, it would declare the compund permutation ([a |-> b, b |-> c, c |-> a], [x |-> y, y |-> z, z |->x]) as valid, but ([a |-> b, b |-> c, c |-> a], [x |-> x, y |-> y, z |->z]) as invalid.

Ron

[Leslie Lamport]

Problem 2 does not exist for two reasons.  (1) While TLC fingerprints the permuted state, it computes next states based on the actual state.  Hence, every state that it examines is reachable.  (2) If your spec is actually symmetric, then every permutation of a reachable state is reachable.  If there are permutations that are not reachable, then your model is incorrect.  However, the result of this incorrectness is that TLC may fail to examine a reachable state that it should examine; it will not cause it to examine unreachable states.

Leslie

[Ron Pressler]

On Wednesday, December 2, 2015 at 10:43:06 PM UTC+2, Leslie Lamport wrote:

(1) While TLC fingerprints the permuted state, it computes next states based on the actual state.  Hence, every state that it examines is reachable. 

In order to fingerprint the permuted state, TLC fully constructs it. That's what I meant by "computes" in that context.

 

(2) If your spec is actually symmetric, then every permutation of a reachable state is reachable.  If there are permutations that are not reachable, then your model is incorrect.  However, the result of this incorrectness is that TLC may fail to examine a reachable state that it should examine; it will not cause it to examine unreachable states.

Let me try to explain what I mean with a clearer example, and please let me know if I'm wrong. Suppose I have two variables, `foo` and `bar`, `foo` obtaining one of the values {a, b, c} and `bar` the values {x, y, z}. My initial state maps sets `foo and `bar` in such a way that if `foo` is `a` then `bar` is `x`, if `foo` is `b` then `bar` is `y` and if `foo` is `c` then `bar` is `z`. My model is symmetrical in both sets of values, and every possible initial mapping from {a,b,c} to {x,y,z} is valid, but I'm only interested in symmetries that preserve the original mapping. I am only interested in 3 permutations, while TLC will generate 9. I'm interested in the symmetries because in the course of running the model starting from my initial state, the model will reach a state that is symmetrical in the pair (a, x) to a state with (b, y) which may have already visited, and so have no interest in (re-)exploring. TLC, though, will also generate (for the purpose of fingerprinting) states with the pairing (a, y). Those states are indeed reachable if my initial state allowed them. So it is true that if all 9 permutations are applied to the initial condition, then all 9 permutations of all states are indeed reachable, but that is of no interest because it amounts to no more than running the model with different names, rather than not visiting states that are symmetrical to those I've already visited. 

Again, if I start with the pairing [a |-> x, b |-> y, c |-> z] I may reach a state that is symmetrical with {<<a, x>>, <<b, y>>, <<c, z>>} but not {<<a, y>>, <<b, x>>, <<c, z>>}. If there was a way to let TLC have symmetrical sets of _pairs_ of model values, I could just specify that set of pairs as a symmetry set and have `foo` and `bar` pick a first and second element of a pair respectively, but I'm not aware of a way to do that.

Ron

[Leslie Lamport]

To fingerprint a state, TLC should construct a single new state that
is a permutation of that state and fingerprint the permuted state.
The time to construct that permuted state should be linear in the size
of the state.

A specification is symmetric in a set S iff for every behavior b
allowed by the specification and every permutation p of S, the
behavior obtained by applying p to every state of b is also a behavior
allowed by the specification.  (Applying p to a state means replacing
each element s of S by p(s).) 

I interpret what you have written to meant that your specification
allows only intial states in which foo = a iff bar = x.  Such a
specification is not symmetric in either {a, b, c} or {x, y, z}.  I
believe that the only way for a specification not to be symmetric in a
set S of model values is if it contains an expression of the form
"CHOOSE s \in S : ...".  A model can also produce an asymmetric
specification by using individual model values in S in instantiating a
constant or overriding a definition.

Leslie

[Ron Pressler]

On Thursday, December 3, 2015 at 5:05:30 PM UTC+2, Leslie Lamport wrote:

To fingerprint a state, TLC should construct a single new state that
is a permutation of that state and fingerprint the permuted state.
The time to construct that permuted state should be linear in the size
of the state.

That's perfectly fine, but it should also be significantly less (in practice) than the time to compute (by next-step), or the optimization might not pay off.

 

A specification is symmetric in a set S iff for every behavior b
allowed by the specification and every permutation p of S, the
behavior obtained by applying p to every state of b is also a behavior
allowed by the specification.  (Applying p to a state means replacing
each element s of S by p(s).) 

I believe mine is symmetric in both sets.

 

I interpret what you have written to meant that your specification
allows only intial states in which foo = a iff bar = x.  Such a
specification is not symmetric in either {a, b, c} or {x, y, z}.

Ah, no, that's not what I meant. It allows any initial state, but no matter the mapping between values in the initial state, it is always preserved, so states with different mappings will never be reached. I think I have an effective clarification: consider a model with a single variable `foo` that can obtain the symmetric values `{a, b, c}`. Now introduce a constant, Map, which maps the set to {x, y, z} in any arbitrary way. Then, introduce another variable, `bar` and the following conjunction to the next state formula:

   /\ bar' = Map(foo')

I think this model is semantically symmetrical in both sets, but from any given initial condition, only 3 permutations out of 9 are reachable for each state. TLC, however (I think) will construct all 9. Am I wrong (on one count? both counts? :))

Ron

[Ron Pressler]

On Thursday, December 3, 2015 at 5:16:56 PM UTC+2, Ron Pressler wrote:

Now introduce a constant, Map, which maps the set to {x, y, z} in any arbitrary way.

By "any arbitrary way" I mean any arbitrary bijection, of course. 

[Michael Leuschel]

Hi Ron,

Does the following capture your example ?
I include the Dot rendering of the full state space (as computed by ProB when loading the TLA file) : BijectionCst_Statespace.pdf

I also include the state space obtained using a technique called "permutation flooding", which I think to be quite close to what TLC does. Only one state is checked; the others are marked as permutations. [Permutation flooding is typically not the approach of choice in ProB; but if one stores just fingerprints as in TLC then it should be fine.]

Finally, I also include the state space obtained using the nauty package to compute a canonical forms for every reached state; just one canonical form exists here.

Greetings,
Michael

[Ron Pressler]

On Thursday, December 3, 2015 at 5:52:45 PM UTC+2, leuschel wrote:

Does the following capture your example ?

Yes, except that there is a next state where foo travels in some way over the set and bar maintains the mapping. In my actual model (the one with the profile), the mapping is an actual constant of the model (rather than any arbitrary constant variable), and I'm not interested in exploring the state space for all possible mappings.

Ron

[Leslie Lamport]

   I think this model is semantically symmetrical in both sets

If you are convinced that the model of the spec is symmetrical, then
you should be able to prove that it satisfies the definition of
symmetry.

Thank you for making me realize that symmetry with respect to a set S
can be broken by CHOOSE expressions involving S other than ones of the
form  CHOOSE x \in S : ...   -- for example a CHOOSE expression like

    Map == CHOOSE f \in [S -> T] : ...

As I did mention, symmetry can also be broken by instantiating a
constant like Map with an expression that explicitly mentions
individual elements of S.

Leslie

[Ron Pressler]

Even if not symmetrical in both sets, it is surely symmetrical in {<<a, x>>, <<b, y>>, <<c, z>>}, because the original model (just `foo`) is symmetrical in {x, y, z}, no? Perhaps TLC should provide a way to specify this symmetry (e.g. with a predicate on composed permutations)? 

Ron

 

[Leslie Lamport]

If you look in Specifying Systems, you will see that you can specify
the kind of permutation set you want, if you run TLC from the command
line, by using the appropriate SYMMETRY statement in the cfg file.

This flexibility could be the cause of the performance problem you
have discovered with symmetry.  Given an arbitrary symmetry group, TLC
probably has to generate all permutations of the state to find the one
whose fingerprint it should use.  It's possible that TLC does this
even for the symmetry groups obtained by declaring symmetry sets, even
though in this case there's a faster way to do it.  We will look into
this.

Leslie

[Hengfeng Wei]

Hi leuschel,

I am interested in your iFM'2012 paper.

However, I cannot find it following the link you provide.

Could you please send me a copy? (email: hengxin0912 at gmail dot com)

Best regards,

hengxin