Information Technology Reference
In-Depth Information
This \solution" makes the problem worse. The above code will usually work,
but it may fail occasionally when the scheduler does just the right (or wrong)
thing. We have created a Heisenbug that will cause the program to occasionally
fail in ways that may be really hard to reproduce (e.g., probably only when the
grader is looking at it or when the CEO is demonstrating the prototype to an
important investor!).
We now present solution 2 of 3.
2
Solution 2.
In the above solution, we had to check the note before setting it, which led
to the possibility of bad interleavings where one roommate had already made a
decision to buy milk before notifying the other roommate of that decision. If we
use two variables for the notes, a roommate can create a note before checking
the other note and the milk and making a decision to buy. For example, we can
do the following:
Path A
Path B
noteA=1;
//leavenote
if(noteB==0){
//ifnonote**A1**
if(milk==0){
//ifnomilk**A2**
milk++;
//buymilk **A3**
noteB=1;
//leavenote
if(noteA==0){
//ifnonote**B1**
if(milk==0){
//ifnomilk **B2**
milk++;
//buymilk **B3**
}
}
//
**B4**
}
noteA=0;
//removenoteA
}
//
**B5**
noteB=0;
//removenote
If the first thread executes the Path A code and the second thread executes
the Path B code, this protocol is safe; by having each thread write a note (\I
might buy milk") before deciding to buy milk, we ensure that we can never
heave both threads buy milk.
Although this intuition is solid, proving safety without enumerating all pos-
sible interleavings requires a bit of care.
Safety Proof. Assume for the sake of contradiction that the algorithm is not
safe|both A and B buy milk. Consider the state of the two variables (
noteB,
milk
) when thread A is at the line marked A1 at the moment when the atomic
load of
noteB
from shared memory to A's register occurs. There are three cases
to consider:
Case 1: (
1,*
). Impossible because this state contradicts the assumption
that thread A buys milk and reaches
A3
.
Case 2: (
0,
> 0). Impossible because in this simple program the prop-
erty
milk
>
0
is a stable property |once it becomes true, it remains true
Denition: stable property
forever. Thus, if
milk
>
0
is true when A is at
A1
, A's test at line
A2
will
fail, and A will not buy milk, contradicting our assumption.
2
The odds that this one will work also seem low, don't they?
