The first *r_i* signal of each cycle can be interpreted as a
*request* (to access a critical section).
The remaining three signals in a cycle *r_i a_i r_i a_i*
can be interpreted as *grant*, *done*, and *acknowledge*
(of done), respectively.
The grant outputs are mutually exclusive.
After request *r_i* the cycle is closed with *n_i*,
interpreted as *nack* (negative acknowledge),
when the other party has already been granted.

When a *Nacking Arbiter* receives two requests,
it will grant exactly one of them (and nack 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'.

[Zoom|FIG]

XDI state graph for a

[Zoom|FIG]

The state graph of a

In state 5, there is a choice between granting one of the two requesting parties and nacking the other. Once the nack arrives at the environment, subsequent requests by the nacked party are always nacked, also if the grant did not yet arrive at the environment (there is no more choice). This gives rise to states 1', 4', 5', and 5''.

The distinction between states 4 and 4'', and also between 5 and 5''' is
in the *n*_1 arrows.
The difference between states 5 and 5''' is that an *n*_1 signal
in state 5''' may still be a response to an earlier request
when the resource was not available.
Similarly,
the distinction between states 1 and 1'', and also between 5 and 5'''' is
in the *n*_0 arrows.

The distinction between states 12 and 12' is in the *n*_0 arrows.
The distinction between states 7 and 7' is in the *n*_1 arrows.
The difference between states 14 and 14' is explained by the fact
that the last party to have had `access to the critical section'
certainly cannot be nacked upon a subsequent request;
the other party might.

Specification in Verdect:

define NAK( r0?, a0!, n0!, r1?, a1!, n1! ) = |[ x0, x1, y0, y1, z0, z1 :: pref *[ r0?; (x0; a0!; r0?; y0; a0! | z0; n0!) ] || pref *[ r1?; (x1; a1!; r1?; y1; a1! | z1; n1!) ] || pref *[ x0; *[z1]; y0 | x1; *[z0]; y1 ] ]| endAlso available through this link

The roles of the subscripts 0 and 1 can be interchanged

A *Nacking Arbiter* is not output deterministic,
since there is an output choice in states 5, and 5''', 5''''.
The output nondeterminism is dynamic.

- According to
Josephs90b the*Nacking Arbiter*specified by the algebraic expression above can be implemented by a state machine using a sequencing component S, an I-Wire, six Forks and five Merges, see figure 1a; component S can be decomposed further into a Sequencer (Seq), an mxn-Decision Call and a 3-Merge, see figure 1b. (*NOT equ*):

[Zoom|FIG]

*No information available*

*No information available*

*No information available*

*No information available*

Copyright © 1995-1998 Tom Verhoeff / Tom.Verhoeff@acm.org