Databases Reference
In-Depth Information
1 void go_for_drive() {
2 pthread_mutex_lock (&mutex[mutex_lock]);
3 if (num_riders < capacity) {
4
printf ("Bus waiting for trip %d\n", num_trips);
5 pthread_cond_wait (&cond[cond_shuttle_full], &mutex[mutex_lock]);
6 }
7
printf ("Bus drives around Charlottesville\n");
8 sleep (3);
9 pthread_cond_broadcast (&cond[cond_ride_over]);
10 num_riders = 0;
11 num_trips--;
12 pthread_mutex_unlock (&mutex[mutex_lock]);
13 }
FIGURE 8.26: A synchronization bug in one bus implementation.
drives
was
MultiEffect,
. Recall that the regular expression of the
MultiEffect,
pat-
tern is (PSS
)
. The result indicates multiple
drives
events corresponded to
one
wait
event. This led us to find the bug shown in Figure 8.26. At the end of
function
go for drive
, the bus thread releases the lock (line 12). This effectively
allows the passenger threads to compete for the lock (line 2) and to possibly
\get in" the bus before the bus starts waiting for passengers. In most cases,
the bus thread can successfully obtain the lock (line 2) before it has been
filled to capacity (i.e.,
num riders < capacity
on line 3), so it can generate the
wait
event (line 4). However, the bus can be already full when the bus thread
obtains the lock (i.e.,
num riders>capacity
on line 3), in which case it does not
produce the
wait
event. In such situations,
wait
and
drives
do not alternate. One
way to fix this bug would be to use a conditional variable to synchronize the
bus thread and the passenger threads and make sure the bus thread generates
the
wait
event before it broadcasts that condition.
Another difference concerned the property between
drives
and
gets o
.
In seven of the implementations,
drives
and
gets o
satisfied
MultiEffect,
, but
in the other implementation the strictest property satisfied is
CauseFirst
((PP
SS
)
), which meant it was possible for the bus to drive around Char-
lottesville more than once without allowing passengers to get off between these
trips. This turned out to be another bug of missing synchronization between
the bus thread and the passenger threads. As shown in Figure 8.26, the bus
thread broadcasts that the ride is over to all passenger threads after driving
around the city (line 9). Then it should wait for all the passengers to get off
before starting the next trip. If the bus thread runs before any passengers
depart, it will still be full and will begin the next trip. The third difference in
the property between
wait
and
gets o
was caused by the same bug.
8.4.2.2 OpenSSL
Our second experiment considered six versions of OpenSSL [63], a widely
used open source implementation of the Secure Sockets Layer (SSL) specifica-
Search WWH ::
Custom Search