The
happens-before relation is a strict partial order of events. Two events x and y are
incomparable with respect to the happens-before order if neither x happens before
y nor y happens before x.
For example, c happens before d in Figure 16.7. The order is clearly partial; for
example, c and e are incomparable, even though both c and e happen before d.
A sequence of events is a linearization of a given happens-before order of events
if for all events x and y such that x occurs before y in the sequence, either x happens
before y or x and y are incomparable.
For example,
(a,R(0), b,R(1), c, e,R(2), f,R(3), g,R(4), d)
is a linearization of the partial order of events depicted in Figure 16.7.
16.6.1 Multiplexing
Multiplexing is a technique that produces a single sequence of events generated
by multiple agents that is a linearization of the happens-before relation. It relies
on additional assumptions about the IUT. In particular, this technique assumes an
instrumentation of the IUT in such a way that all shared resource usage events are
observed.
The multiplexing algorithm (or multiplexer) works as follows. It consumes events
from multiple incoming event queues, one queue per agent, and outputs the events
in an order that is consistent with the happens-before relation. It is assumed that all
events from an agent are enqueued into the event queue of that agent in the same
order the events occur in that agent.
Pages:
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361