Mutual-Exclusion Element

Specifications

Informal

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'.

XDI

Specification in XDI model.

Verdect

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 ]
   ]|
end

DI Algebra

Specification in DI Algebra:

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

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

Specification in DI Algebra:

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

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

Properties

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.

Implementations

1. A Mutual-Exclusion Element can be implemented with an RGDA Arbiter, two Toggles, and two Merges (equ):
   
   
   [Zoom|FIG]
   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

Generalizations

No information available

Miscellaneous

References

Last modified at Fri Nov 20 10:11:40 1998