In multithreaded programs,
a partial order of events is defined by access to shared resources. An example of
a shared resource is a lock.
Suppose that each shared resource R is associated with a usage count ucR that
is initially 0. View R as a unary function symbol, and assume that each access (e.g.
read or write) to R generates a resource usage event R(ucR) and causes the usage
count ucR to be incremented by one.
Nowsuppose that there are multiple agents and each agentAgenerates a sequence
of events (eA
1 , eA
2 , . . .). Say that an event eA
i happens immediately before an event
eB
j , if one of the following two conditions holds:
1. A and B are the same agent and j = i + 1.
2. A and B are distinct agents, eA
i is a resource usage event R(k), and eB
j is a
resource usage event R(k + 1) for some shared resource R.
Figure 16.7 illustrates events of a concurrent system with two agents A1 and
A2. The sequence of events of an agent is shown as labeled dots along the corresponding
horizontal line. An arrow from event x to event y indicates that x happens
immediately before y.
Advanced Topics 273
A1
a R(0) b R(1) c R(4) d
A2
e R(2) f R(3) g
Figure 16.7. Example of a partial order of events of two agents A1 and A2.
An event x happens before an event z if either x happens immediately before z
or if there is an event y such that x happens before y and y happens before z.
Pages:
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360