Nacking Arbiter

Specifications

Informal

A Nacking Arbiter has two input terminals (r_0 and r_1) and four output terminals (a_0, n_0, a_1, and n_1). For each i in {0, 1}, the signals cycle through either r_i a_i r_i a_i or r_i n_i.

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

XDI

Schematic diagram for a Nacking Arbiter:

[Zoom|FIG]

XDI state graph for a Nacking Arbiter:

[Zoom|FIG]

Specification in XDI model.

The state graph of a Nacking Arbiter is rather more complicated than that of most other systems. It is best compared to the state graph of a Mutual-Exclusion Element, which lacks the nack outputs but is otherwise very similar. We have used the same numbering scheme for both state graphs. It appears that states 1, 3, 4, 5, 7, 11, 12, and 14 have been split into related but distinct states.

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.

Verdect

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

Also available through this link

DI Algebra

Specification in DI Algebra.

Properties

XDI Report.

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.

Implementations

DI Decompositions

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]

Using Boolean Gates

No information available

Using Transistors