Fairness

0 Introduction.- 0.1 Motivation and Background.- 0.2 A Taxonomy of Fairness Concepts.- 0.3 The Language of Guarded Commands (GC).- 0.3.1 A partial-correctness proof system for GC.- 1 Termination and Well-Foundedness.- 1.0 Overview.- 1.1 Termination Proofs for Deterministic Programs.- 1.2 Termination Proofs for Nondeterministic Programs.- 2 The Method of Helpful Directions.- 2.0 Introduction to Fair Termination.- 2.1 Ordinal Directed Choice of Helpful Directions.- 2.1.1 A proof rule for unconditionally-fair termination.- 2.1.2 Weakly-fair termination.- 2.1.3 Strongly-fair termination.- 2.2 State Directed Choice of Helpful Directions.- 2.2.1 Unconditionally-fair termination.- 2.2.2 Weakly-fair and strongly-fair termination.- 2.3 Inter-reducibility of the Two Methods.- 2.4 Relativized Fair Termination.- 3 The Method of Explicit Scheduler.- 3.0 Overview.- 3.0.1 Random assignments.- 3.1 Unconditionally-Fair Termination.- 3.2 Weak and Strong Fairness: n Guards.- 3.2.1 Examples for strong fairness.- 3.2.2 Alternative transformations.- 3.3 All-Levels Fairness.- 3.4 Comparing Explicit Scheduler with Helpful Directions.- 3.5 More on Fairness and Random Assignments.- 4 Extension and Generalizations of Fairness.- 4.0 Overview.- 4.1 Equifairness.- 4.1.1 Unconditional equifairness.- 4.1.2 Strong equifairness.- 4.2 Generalized Fairness.- 4.3 Extreme Fairness.- 4.3.0 Overview.- 4.3.1 Proof rules for extremely-fair termination.- 4.4 An Analysis of Predicate-Reachability Fairness.- 5 Fair Termination of Concurrent Processes.- 5.1 Overview.- 5.2 Fairness and Communicating Processes.- 5.2.1 The CSP sublanguage for communicating processes.- 5.2.2 Serialized semantics and overlapping semantics.- 5.2.3 Relativized fair termination in the serialized semantics.- 5.2.4 Proofs for the overlapping semantics.- 5.3 Fairness in Shared-Variables Concurrency.- 5.3.0 Overview.- 5.3.1 The shared-variables language SVL.- 5.3.2 Explicit scheduling of shared-variables concurrent programs.- 5.3.2.1 Unconditional fairness for synchronization-free programs.- 5.3.2.2 Explicit scheduling for weak and strong fairness in shared-variables programs.- 5.3.2.3 Proving fair termination of shared-variables programs.- 6 Syntactic Expressibility.- 6.0 Overview.- 6.1 Fixedpoints of Monotone Transformations.- 6.2 The Assertion Language L?.- 6.3 The Weakest Precondition for Fair Termination.- 6.4 Syntactic Completeness of the SFT Rule.- 6.5 The Ordinal Size for Fair-Termination Proofs.- 7 Fairness in Temporal Logic.- 7.0 Overview.- 7.1 Linear-Time Temporal-Logic (LTL).- 7.1.1 The temporal semantics of programs.- 7.1.1.1 Shared variables.- 7.1.1.2 Message passing.- 7.2 Branching-Time Temporal-Logics (BTL).- 7.2.0 Overview.- 8 The Functional Approach.- 8.0 Overview.- 8.1 CCS.- 8.2 Fairness and CCS.- 8.3 Weak and Strong Fairness in CCS.- 8.3.1 Weakly fair CCS.- 8.3.2 Strongly fair CCS.- 8.4 A Metric Characterization of CCS Fairness.- 8.4.1 Overview.- 8.4.2 The basic tools.- 8.4.3 A metric characterization of D and D?.- 8.5 Finite Delay Operators.- References.- List of Proof Rules.- Author Index.