| << Chapter < Page | Chapter >> Page > |
Assume we have two concurrent threads/processes, each with
simple straight-line code and sharing a global variable
x .
Assume that each individual statement is atomic.
1 thread0:
2 {3 x=0
4 x=x+15 }
6 thread1:7 {
8 x=09 x=x+1
10 x=x+211 }
Without using SPIN,
give one trace illustrating each of the possible final valuesof
x .
There are three possible final values of
x :
1, 3, 4.
Answer the previous exercise, except with different atomicity.
Assume that each variable lookup, variable assignment, andaddition are atomic, as in a typical machine language.
Specifically, use the following code:
1 thread0:
2 {3 x = 0
4 r0 = x5 r0 += 1
6 x = r07 }
8 thread1:9 {
10 x = 011 r1 = x
12 r1 += 113 x = r1
14 r1 = x15 r1 += 2
16 x = r117 }
The values 1, 3, and 4 are possible as before. It should be clear that values greater than 4 are impossible,since at most a total of 4 can ever be added. Similarly, values less than 1 are impossible, since at least1 is added after the last variable lookup. So, we're left with the question of whether 2 is a possible result.It is, and one possible trace is given.
Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|