[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: problems debugging liveness errors.

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

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."


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+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.