problems debugging liveness errors.

[david streader]

Hi

     Specifying the Alternating bit protocol as component processes in PlusCal  and showing it is a refinement of a one place buffer. The refinement works fo  safety properties but fails when i try to check the liveness properties. I have attached a png showing  a small fragment of the State Graph and the error trace.  What I do not understand is why this is failing. The error trace is the cycle of three states in the top right of the State Graph but two of these states offer the ability to exit the loop (via an ssd step) but the translated PlusCal has added the strong fairness clauses for all the steps:

Spec == /\ Init /\ [][Next]_vars

        /\ WF_vars(Next)

        /\ SF_vars(ssd)

        /\ SF_vars(sData)

        /\ SF_vars(rData)

        /\ SF_vars(wire)

        /\ SF_vars(ackWire)

        /\ SF_vars(sender)

I assume that I have misunderstood some thing but I thought that looping forever was prohibited by these strong fairness clauses. Hence I can not see how to correct my spec.

   thanks in advance for any help   david

[Jay Parlar]

Can you include the specs themselves? The definition of strong fairness is subtle, it’s not simply that it disallows looping. I don’t know that I’d be able to diagnose the problem without seeing the specs (others might be able to though).

[david streader]

Hi Jay Sorry I set this as an assignment (safety only) so I cannot post the spec for another week.  My fault I should have thought of this before I posted the question. 

   But if  strong fairness on a step that exits a loop does not require the exiting step to  eventually be taken then I have some fundamental errors as to what strong fairness means.

[Jay Parlar]

Strong fairness means an action which is enabled infinitely often will eventually be taken. So it can be disabled and renabled over and over, but as long as it always gets renabled, then it will eventually be taken. Which is essentially what you said.

But if, for example, an action is enabled infinitely often and there are _two_ ways to step out of it (because of non determinism in the action), you are NOT guaranteed that both ways out will eventually be taken.

To guarantee that, you’d have to further subdivide the action, and have strong fairness on the subdivisions.

As an example,

Foo == /\ x = 1
/\ \E y \in {2, 3} : x’ = y

If x is repeatedly toggled between 0 and 1 by some other action, and you have strong fairness on Foo, then you’re guaranteed that the Foo action will eventually take place. But it taking place by always choosing 2 would be valid, there’s no guarantee that eventually it would assign 3 to x in the next state.

My guess is that your PlusCal is being turned into actions which contain non-determinism, and TLC is showing you a trace where only one side of the non-determinism ever occurs.

I hope this helps!
Jay P.

[david streader]

Many thanks for you time and effort.

I have gutted the specification so it is a lot  smaller but some what  artificial. Run TLC with a model with CORRUPT_DATA a model value and Message <<9>> plus the property Fin

The problem is, the state graph shows that from the initial state two distinct steps are possible.  Hence   the nondeterminism you mentioned does not apply. Yet  with Spec the we get a temporal error with trace looping back to the initial state. But with  MySpec == Spec /\ SF_vars(sData/\ pc'["send"]="ssd") the error disappeared hence TLC behaves as if these two steps are not distinct.

I have constructed many small examples for teaching and the state graph has so far always agreed with TLC.  Consequently I have been using it to help analyses the liveness behaviour of the TLA+ specs.

 In this example the state graph and TLC disagree.  

Checking the spec by hand I find that I agree with the state Graph and disagree with TLC.

 thanks again.  david

[Jay Parlar]

I believe I see your misunderstanding:

The temporal-property violating loop occurs under the following steps:

 - we start in your initial state

 - then we take a `rData` step, pink arrow, wherein `wayBack` becomes <<1>>

 - then we take an `aWire` step, green arrow, wherein `endBack` becomes <<1>> and `wayBack` returns to <<>>

 - then we take an `sData` step, blue arrow, which brings us back to the initial state

As a reminder, Spec looks like this

Spec == /\ Init /\ [][Next]_vars

        /\ WF_vars(Next)

        /\ SF_vars(ackWire)

        /\ SF_vars(sData \/ ssd)

        /\ SF_vars(receiver)

(I replaced `sender` with `sData \/ ssd`, as that is what `sender` is defined as)

If we look at your initial state in the state graph, we can see that there are two possible exists from it:

 - A pink arrow to the right, 'rData', which is the one involved in the infinite loop

 - A blue arrow to the left, 'sData', which is the one you _want_ to see eventually taken

Your question roughly is: "Why is an infinite loop allowed, shouldn't strong fairness guarantee that we eventually take that `sData` step out of the initial state?"

Let's recall what strong fairness means:

"Strong fairness asserts the a step `A` must occur if `A` is repeatedly enabled, even if it is also repeatedly disabled"

i.e., if some step is repeatedly made possible to take, then we'll eventually take it.

But now let's look at the steps that are taking place in your infinite loop:

rData -> aWire -> sData

Those steps take place over and over. And what's the third step there? An `sData` step! So your strong fairness is satisfied! 

We've told the system that if `sData` is repeatedly enabled, then it must eventually be taken. The confusion in your system is that it's enabled _both_ from your initial state, but also after the `aWire` step takes place. It's enabled in two different places along the path of your infinite loop!

So while you personally would like to see that step taken from the initial state, the conditions of strong fairness are perfectly satisfied by that infinite loop. `sData` is repeatedly enabled in that infinite looping behaviour, and the `sData` step is always eventually taken. It always happens to only take the step in one of the two possible places it _could_ take the step, but that doesn't matter to TLA+.

I hope that helps!

Jay P.

[Jay Parlar]

One final comment: I'd be wary of the number of strongly fair labels you've placed in your spec. My understanding is that strong fairness is rarely used, as it's difficult to implement actual systems that satisfy it. It definitely has its place, but it's not common. Placing it on every process and label in your spec is most likely not the correct course of action.

I understand doing it given your initial assumption that "looping forever was prohibited by these strong fairness clauses", but as we've shown, your assumption was incorrect.

I just don't want you or your students to think that the right way to approach these specs is by marking everything as strongly fair.

Jay P.

[david streader]

Many thanks

       Initially I thought that, in order to establish strong fairness  you only  needed to restrict a step when there was a choice between two transitions of the same step.  That is when a step itself was nondeterministic. But I can see that even with deterministic steps  all you need is the exiting step to be some where in the loop then you need  to restrict the step.

       Strong Fairness in TLA+  is quite different from that in process algebras such as Fair Failure semantics. It is interesting that liveness conditions are so hard to verify in TLA+ whereas in process algebras they are, by default, what are normally specified and verified.

Finally I am getting the differences between process algebra and TLA+  

regards david

[david streader]

 My last reply was a little rushed as it was  literally 15mins before giving  a lecture on fairness.  So again many thanks.

You say that strong fairness is rarely used and may be hard to implement. In order to establish certain liveness conditions weak fairness will not suffice and then its strong fairness or some bespoke temporal logic restriction. Consequently I only use strong fairness when I see no viable option.

It is interesting that fairness in TLA+ is defined on the behaviour with regard to a single step. Where as in a world with concurrent components, say your phone and my phone, a step my phone might take could act unfairly in as much as it prevented the execution of another step on my phone. But, the steps on my phone are fair with respect to steps on your phone as my phone can never prevent your phone from performing its steps.  So it would seem that fairness might be better viewed as  a function of more than one step. Then steps on distinct processes by default behave fairly with respect to each other and it is only hard to implement fairness between steps on the same process.

I have to admit that, when I place fairness conditions every where,  I am being influenced by my past experiences formalising concurrent systems. In process algebras  it is decided that every thing is fair or every thing is not fair (largely no distinction is made between strong and weak fairness). In either case, fair or unfair, liveness conditions can be  preserved by selecting the appropriate semantics. Consequently I am unfamiliar with using a fairness condition to establish a liveness property.  

There are many aspects to TLA+ that  work very smoothly but liveness checking in TLA+ I still find a painstaking and error prone task. Hopefully more practice will help.  regards david

[Jay Parlar]

I highly recommend you watch Lamport's videos, esp. lecture 9, as it's the best description of liveness in TLA+ that I've seen http://lamport.azurewebsites.net/video/videos.html

On Friday, 3 May 2019 00:35:04 UTC-4, david streader wrote:

It is interesting that fairness in TLA+ is defined on the behaviour with regard to a single step. Where as in a world with concurrent components, say your phone and my phone, a step my phone might take could act unfairly in as much as it prevented the execution of another step on my phone. But, the steps on my phone are fair with respect to steps on your phone as my phone can never prevent your phone from performing its steps.  So it would seem that fairness might be better viewed as  a function of more than one step. Then steps on distinct processes by default behave fairly with respect to each other and it is only hard to implement fairness between steps on the same process.

Remember that in TLA+, there are no such thing as processes! PlusCal has them, but when it all gets down to TLA+, a process is in the eye of a beholder. You can interpret things however you want. TLA+ is only concerned with the global state of the universe. How you choose to interpret that state is up to you (and the PlusCal translation interprets it in a very specific way).

For your phone example, in TLA+, steps taken on one phone can't prevent another phone from taking a fair action. But if the TLA+ model doesn't have a clean separation between the phones, then you'll see issues.

In particular, fairness in TLA+ is all about whether an _enabled_ action will ever take place. My phone might need your phone to do something in order for my phone to become enabled (like waiting for your phone to send a response to my phone). But if we mark my phone's action as strongly fair, and the action is repeatedly enabled, then my phone will eventually take the step.

What we saw with your spec though was more akin to _both_ phones being able to take the _exact same action_, with no distinction made between which phone is taking it.

 

I have to admit that, when I place fairness conditions every where,  I am being influenced by my past experiences formalising concurrent systems. In process algebras  it is decided that every thing is fair or every thing is not fair (largely no distinction is made between strong and weak fairness). In either case, fair or unfair, liveness conditions can be  preserved by selecting the appropriate semantics. Consequently I am unfamiliar with using a fairness condition to establish a liveness property.  

I'll recommend again that you watch Lamport's videos. The same information is available in other sources (Specifying Systems, The Hyperbook), but the videos are my favourite source. Liveness/fairness is definitely the trickiest concept in TLA+, and I found it worth putting in the extra time to really learn it well.

Jay P.

 

[Leslie Lamport]

I don't understand what you mean by fairness.  You come from
the world of process algebra, and I expect that the word means
something different there.  So, let me explain what fairness means.
I'll describe it in terms of TLA+, but the concepts are
language-independent.  They apply to any language in which a
specification is something that is true or false on an individual
behavior, where a behavior is a sequence of states and/or actions.
The last I heard, which was quite a while ago, process algebras are
not such languages.

The meaning of a TLA+ temporal formula is a predicate on behaviors,
which are infinite sequences of states.  Any such predicate can be
written as the conjunction of a safety property and a liveness
property.  A safety property is one that is true for a behavior iff
it's true for every finite prefix of the behavior, where a finite
sequence of states is defined to satisfy a property iff the behavior
obtained by stuttering its final state forever satisfies the property.
A liveness property is one such that any finite sequence of states can
be completed to a behavior that satisfies the property.  If S is a
safety property and L is a liveness property, we say that L is a
FAIRNESS PROPERTY FOR S if any finite sequence of states that
satisfies S can be completed to a behavior that satisfies S /\ L. A
spec written with such a fairness condition is called MACHINE CLOSED.
(More precisely, the pair (S, L) is called machine closed.)  Specs
that are not machine closed are weird, because the liveness property L
disallows finite behaviors that satisfy S. We usually want to avoid
them.  

In TLA+ and in many other spec languages, safety properties and
liveness properties are specified separately.  In many languages,
safety is specified by some sort of code--just as PlusCal does.  In
TLA+ it's expressed by a formula of the form Init /\ [][Next]_vars.
In many languages, liveness is specified by putting weak and/or strong
fairness conditions on actions.  The reason we call WF and SF fairness
conditions is that the conjunction of formulas WF_vars(A) and/or
SF_vars(A) for subactions A of Next is a fairness condition for Init
/\ [][Next]_vars.  A SUBACTION A of Next is an action such that, from
every reachable state, an A step is a Next step.  Most practical
languages allow you to add weak/strong fairness conditions only to
particular subactions of Next.  Effectively, they write the next-state
relation as the union of some particular subactions and can add
fairness conditions only to those subactions.  PlusCal is such a
language.  As has been observed on this group, this restriction can
make it hard to write a desired fairness condition in PlusCal.  I
believe the same is true for any method that adds fairness conditions
in this way.  At best, they require you to rewrite the safety part of
the spec in a less natural way to express the desired fairness
property.  At worst, they can't express it.  TLA+ doesn't have this
restriction, because you can write a WF or SF condition on any
subaction of Next.  I have never had any trouble writing a fairness
condition that I wanted in TLA+.

There are rare situations in which you want to write a spec that is
not machine closed.  You can do that easily in TLA+ with WF and SF
formulas applied to actions that are NOT subactions of Next.  (I've
done that in a paper called "A Lazy Caching Proof in TLA".)  Moreover,
writing a proof that one spec implements another can require adding an
auxiliary variable that produces a spec that's not machine closed.
Any language that allows you to add fairness conditions only to
subactions of the next-state action won't let you write such a spec.

Now that I have explained what fairness means, perhaps you will be
able to explain what you mean by "fairness might be better viewed as a

function of more than one step."

Leslie