Go backward to Liveness as TLA Formulas Go up to Top Go forward to Fairness

Fairness

• Arbitrary liveness properties dangerous:
  • Used to express fairness requirements.
  • May unexpectedly add safety properties.
  • Add: always eventually (x=0).
  • Consequence: x never changes!
  • Solution: express liveness by fairness.
• Fairness:
  • If operation possible, program must eventually execute it.
• Weak fairness:
  • Operation must be executed if it remains possible to do so for long enough time.
  • (eventually executed) or (eventually impossible)
• Strong fairness:
  • Operation must be executed if it is often enough possible to do so.
  • (eventually executed) or (eventually always impossible)