This action is enabled if m is an outstanding request, and the granted credits
do not exceed the requested credits.
Accepting states
It is useful to identify those states where no requests are pending. From the clients
point of view, these are states where the server is stable; that is, the server is not
processing a request. All accepting traces of the credits model program have to end
in an accepting state.
State invariants
An important property of the credits algorithm is that the client must not starve. In
other words, it should never be the case that the client runs out of credits and cannot
send further requests. This does not mean that the server always has to grant at
least one credit to the client in every response. It may be that the client has pending
requests that will eventually grant the client more credits. Thus, the state invariant
is that if there are no pending requests then the window must be nonempty.
Exploration
A natural question that arises here is whether the model program in Figure 14.1 has
any unsafe states, that is, states reachable from the initial state that violate the state
invariant. If this is the case then the model program should be amended.
To explore the credits model program, we use a finite state machine (FSM)
model program that restricts the credits model program to a finite set of states (see
Advanced Topics 229
FSM(0, AcceptingStates(0),
Transitions(t(0,ReqSetup(0,0),0), t(0,ReqSetup(0,1),0),
t(0,ResSetup(0,0),0), t(0,ResSetup(0,1),0)),
Vocabulary("ReqWork", "ResWork"))
Figure 14.
Pages:
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306