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

# Mutual-Exclusion Element

## Specifications

### Informal

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

### XDI

Schematic diagram for a Mutual-Exclusion Element:

[Zoom|FIG]

XDI state graph for a Mutual-Exclusion Element:

[Zoom|FIG]

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

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
]

```

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
]
[{r0},{a0}]
[{r1},{a1}]

```

This comparison shows that this specification is correct.

## Properties

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.

## Implementations

### DI Decompositions

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

No information available.