Fairness

Fairness for liveness verification

Frédéric Herbreteau, Bordeaux INP/LaBRI (frederic.herbreteau@bordeaux-inp.fr)

Unfair violation of liveness properties

Liveness properties are often violated although we expect them to hold

Example: Each waiting process will eventually enter the critical section (absence of starvation)

Many fairness conditions

• Unconditional fairness every process gets its turn infinitely often
• Strong fairness every process enabled infinitely often gets its turn infinitely often
• Weak fairness every process enabled almost always, gets its turn infinitely often

Exercise: Which condition(s) above eliminate the bad run in the previous slide?

Remark: unconditional $\implies$ strong $\implies$ weak

Example (1/3)

Exercise: Is ‘‘infinitely often b’’ true for executions that are:

• unfair (no extra fairness condition)
• weakly fair w.r.t. $\alpha$ and $\beta$?
• strongly fair w.r.t. $\alpha$ and $\beta$?
• unconditionally fair w.r.t to $\alpha$ and $\beta$?

Example (2/3)

Exercise: Express all three fairness conditions in TL:

• unconditionally fair w.r.t to $\alpha$ and $\beta$
• weakly fair w.r.t. $\alpha$ and $\beta$
• strongly fair w.r.t. $\alpha$ and $\beta$

assuming we have atomic propositions:

• “$en_a$” when action $a$ is enabled,
• and “$a$” when action $a$ occurs.

Example (3/3)

Exercise: Express “infinitely often b” under all three fairness conditions in TL

• unconditionally fair w.r.t to $\alpha$ and $\beta$
• weakly fair w.r.t. $\alpha$ and $\beta$
• strongly fair w.r.t. $\alpha$ and $\beta$

assuming we have atomic propositions:

• “$en_a$” when action $a$ is enabled,
• and “$a$” when action $a$ occurs.