Bounded Fairness

10 years 9 months ago
Bounded Fairness
Abstract. Bounded fairness is a stronger notion than ordinary eventuality-based fairness, one that guarantees occurrence of an event within a fixed number of occurrences of another event. We formalize bounded fairness by introducing a new family of temporal modal operators. The resultant logic is equivalent to temporal logic with the until modality, but more succinct. This logic can be used to specify bounded fairness requirements in a more natural manner than possible with until. It can, for example, relate the frequency of shared resource access of a particular process to other processes that access the resource with mutual exclusion. As applications of bounded fairness, we verify requirements for some standard concurrent programming problems and for a new cache protocol. We also show that Dekker’s mutual exclusion algorithm is fair in the conventional sense, but not bounded fair. Was euer booke containing such vile matter So fairely bound? The most excellent and lamentable traged...
Nachum Dershowitz, D. N. Jayasimha, Seungjoon Park
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Authors Nachum Dershowitz, D. N. Jayasimha, Seungjoon Park
Comments (0)