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

*From*: Leslie Lamport <tlaplus.ll@xxxxxxxxx>*Date*: Fri, 3 May 2019 18:29:02 -0700 (PDT)*References*: <1fa1392c-0ec5-4d9e-b339-f7d1617c5117@googlegroups.com> <8147e0fe-bd5c-4653-8523-ef729b528834@googlegroups.com> <af589ad5-3cf3-4899-8be3-0c74d139b1d8@googlegroups.com> <a0489306-2ba7-4dbe-a7f5-ee1be6faaff3@googlegroups.com> <75179b6a-2163-410d-b143-984fafa4533c@googlegroups.com> <afad3d13-2732-45a4-884e-5c6cb40d9ba7@googlegroups.com> <3a801542-110a-4aa1-b2c2-f83191fcf5cc@googlegroups.com> <86588945-287d-48fd-9232-65fcb96753b2@googlegroups.com> <9d99b580-580c-4504-bbc7-a6b081a0f0c2@googlegroups.com>

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

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

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.

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

able to explain what you mean by "fairness might be better viewed as a

function of more than one step."

Leslie

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.

**References**:**[tlaplus] problems debugging liveness errors.***From:*david streader

**[tlaplus] problems debugging liveness errors.***From:*Jay Parlar

**[tlaplus] Re: problems debugging liveness errors.***From:*david streader

**[tlaplus] Re: problems debugging liveness errors.***From:*Jay Parlar

**[tlaplus] Re: problems debugging liveness errors.***From:*david streader

**[tlaplus] Re: problems debugging liveness errors.***From:*Jay Parlar

**[tlaplus] Re: problems debugging liveness errors.***From:*Jay Parlar

**[tlaplus] Re: problems debugging liveness errors.***From:*david streader

**[tlaplus] Re: problems debugging liveness errors.***From:*david streader

- Prev by Date:
**[tlaplus] A minor thing in Video course 6 (TwoPhase Commit)** - Next by Date:
**Re: [tlaplus] university courses using TLA+?** - Previous by thread:
**[tlaplus] Re: problems debugging liveness errors.** - Next by thread:
**[tlaplus] Dealing with a `pc` variable in refinement?** - Index(es):