EDIS: Guide | FAQ | New | Search | Bibliography | Index | Feedback

Mutual-Exclusion Element



A Mutual-Exclusion Element is a handshake component with two passive 4-phase handshake ports. The second to third phase intervals do not overlap.

The four phases of a handshake with a Mutual-Exclusion Element can be interpreted as request, grant, done, and acknowledge (of done) respectively. The grant outputs on the ports are mutually exclusive.

When a Mutual-Exclusion Element receives two requests, it will grant exactly one of them (and delay the other). The specification leaves the choice open. Often there is a fairness requirement on this choice: if a choice situation arises `infinitely often' then both requests are granted `infinitely often'.


Schematic diagram for a Mutual-Exclusion Element:


XDI state graph for a Mutual-Exclusion Element:


Specification in XDI model.


Specification in Verdect:

define ME( r0?, a0!, r1?, a1! ) =
   |[  x0, y0, x1, y1 ::
       pref *[ r0?; x0; a0!; r0?; y0; a0! ]
   ||  pref *[ r1?; x1; a1!; r1?; y1; a1! ]
   ||  pref *[ x0; y0 | x1; y1 ]
Also available through this link

DI Algebra

The following specification in DI Algebra is different from the specification given above for the same reasons as for the Nacking Arbiter.

Specification in DI Algebra:

I = { r0, r1 }
O = { a0, a1 }

ME = [ r0? -> a0! ; r0? ; a0! ; ME
     , r1? -> a1! ; r1? ; a1! ; ME

Also available through this link

This is shown by this report. An alternative specification in DI Algebra uses alternations:

Specification in DI Algebra:

I = { r0, r1 }
O = { a0, a1 }

ME = [ r0? -> a0! ; r0? ; a0!; ME
     , r1? -> a1! ; r1? ; a1!; ME

Also available through this link

This comparison shows that this specification is correct.


XDI Report.

The roles of the two ports can be interchanged:
ME(a, b) = ME(b, a)

A Mutual-Exclusion Element is not output deterministic, since there is an output choice in state 5. The output nondeterminism is dynamic.


DI Decompositions

  1. A Mutual-Exclusion Element can be implemented with an RGDA Arbiter, two Toggles, and two Merges (equ):

    The Ludwig verification script of this implementation.
  2. A Mutual-Exclusion Element can be implemented with a Nacking Arbiter and two Merges:
    This implementation is equivalent to the specification if infinite chatter is not considered harmful.

Using Boolean Gates

No information available

Using Transistors

No information available


No information available


No information available.


Last modified at Fri Nov 20 10:11:40 1998
Encyclopaedia of Delay-Insensitive Systems
Copyright © 1995-1998 Tom Verhoeff / Tom.Verhoeff@acm.org