Title
On the Existence of Delay-Insensitive Fair Arbiters: Trace Theory and its Limitations.
Abstract
This paper considers the existence and formal specification of delay-insensitive fair arbiters. We show that the exact notion of fairness used is of critical importance because certain common notions are not delay-insensitive when used across independent interfaces. We further show that for the relevant notions of fairness, the existing trace theory of finite traces lacks the expressive power to specify a delay-insensitive fair arbiter (i.e. the specification of such a fair arbiter is also satisfied by an unfair arbiter). Based on this we extend trace theory to include infinite traces, and show by example the importance of including liveness in such a theory. The extended theory is sufficiently expressive to distinguish fair arbiters from unfair ones, and we use it to exhibit a delay-insensitive fair arbiter, thus establishing their existence. In addition our extended theory generalizes the existing trace theory by introducing a composition operator (C) that at once generalizes the existing operators and obviates the composability restrictions used by previous authors. Finally our extended theory introduces wire modules as an abstraction to capture the important role that transmission media properties play in circuit behavior.
Year
DOI
Venue
1986
10.1007/BF01660033
Distributed computing
Keywords
Field
DocType
composition operator,satisfiability,expressive power,formal specification
Arbiter,Abstraction,Petroleum engineering,Formal specification,Theoretical computer science,Composition operator,Operator (computer programming),Engineering,Trace theory,Composability,Distributed computing,Liveness
Journal
Volume
Issue
ISSN
1
4
1432-0452
Citations 
PageRank 
References 
11
8.28
3
Authors
1
Name
Order
Citations
PageRank
David L. Black113429.13