Lecture 9
Arbiters
9.1
Introduction
An arbiter
circuit controls the exclusive access of one out of a number possibly competing
processes to a shared resource. The circuit has one
binary incoming line INj from each
process #j , and one binary outgoing line OUTj
to each process #j.
The
up-transition of INj is denoted Rj (request), its down-transition is denoted Dj (done). Similarly, the up- and
down-transitions of OUTj are denoted Gj (grant) and Aj (ack), respectively.
The various
line changes are interpreted as follows.
(1) R1
: process #1 requests access (to the shared resource)
(2) G1
: the resource is free and access is granted
(3) D1
: process #1 releases the resource
(4) A1 : access withdrawn.
We expect an
arbiter circuit to satisfy the following requirements.
(1) Mutual Exclusion.
Only one process may have access to the shared resource.
(2) Grants only on
Request.
(3) Fairness.
Any request by a process is eventually
granted.
9.2
The RGDA Arbiter
We now
consider a two-process arbiter, referred to as RGDA arbiter. For an informal
description and a graphical representation, see [EDIS]/rgda-arbiter.
9.4
Verification
Let us now check
whether the requirements formulated in Section 9.1 are indeed satisfied.
We have to
show that event G1 (“the resource is granted to process #1”) may be followed by
event G2 only if event D1 (“release of resource by process #1”) intervenes. Similarly, D2 must intervene, should G2
be followed by G1.
One way of
showing that this requirement is indeed satisfied, is as follows. We consider arb\{R1,R2,A1,A2}. The outcome
becomes:
(*[G1;D1] || *[G2;D2]) || *[G1;D1
[] G2;D2] .
One easily
verifies that the above expression reduces to
*[G1;D1 [ ] G2;D2],
since *[P [] Q] is evidently a subsystem of *P || *Q .
This clearly
shows that the mutual exclusion requirement is satisfied.
To show that a
grant Gi (i=1,2) always follows a request Ri,
we may simply hide (i.e., replace by ‘i’) in the
above representation of RGDA all events, except Ri
and Gi, and proceed as above. The outcome will be
that Ri and Gi indeed alternate.
Fairness
However, the
above arbiter is not fair! Namely process #1 may hold on to the resource
forever, although process #2 has requested it. Indeed, the following infinite
event sequence is feasible:
R1;G1;R2;D1;A1; (R1;G1;D1;A1;)∞
where ∞ denotes “repeat forever”
9.5 Exercises
Exercise Ex9.1 Look at the RGD Arbiter also specified within the
[EDIS]-document. Prepare a BLA description. Verify this arbiter,
similar to the above Section 9.4.
Exercise
Ex9.2 Apply CADP to verify the
RGDA arbiter.
Exercise Ex9.3 Extend the RGDA arbiter to one where 3 processes
share a single resource. Prepare a documentation consisting of BLA and proper LOTOS descriptions as
well as the relevant verification.
9.6
Further
A “nacking” arbiter is an improved
version of the above RGDA-arbiter. To find out more, see [EDIS].
A quite simple specification and verification of an arbiter
can be found in [Sta94].
9.7
References
[EDIS]
http://edis.win.tue.nl/sys
[Sta94] J.Staunstrup, A Formal Approach to Hardware Design,
Kluwer Academic Publ.,
1994.
9.8
Solution of Ex9.2
Below is a
LOTOS-file representing the RGDA arbiter.
specification arb[R1,G1,D1,A1,R2,G2,D2,A2]:noexit
behaviour
arb[R1,G1,D1,A1,R2,G2,D2,A2[
where
process arb[R1,G1,D1,A1,R2,G2,D2,A2]:noexit: =
(cy[R1,G1,D1,A1]|||cy[R2,G2,D2,A2])|[G1,D1,G2,D2]|
mex[G1,D1,G2,D2]
endproc
process cy[R,G,D,A]:noexit:=
R;G;D;A;cy[R,G,D,A]
endproc
process mex[G1,D1,G2,D2]:noexit:=
G1;D1;mex[G1,D1,G2,D2]
[]
G2;D2;mex[G1,D1,G2,D2]
endproc
endspec
To verify this
arbiter, use CADP to implement the approach of Section 9.4.