| << Chapter < Page | Chapter >> Page > |
How many possible traces does this code allow? (Try it in SPIN!)
This code has 70 possible traces many more than the previous version. Even with such a smallprogram, it is too cumbersome to try to list them all. This is a fundamental reason why it is so hard for humansto debug a concurrent program, since it involves understanding all the possible ways threads can interact.Once we start using SPIN as a verifier, letting it enumerate these as a part of verification will be oneof the benefits of automation. Later, we will verify this specific example .
More importantly, what is the result of the computation,
bal at the end?
It can be 0, as expected, but it can also be 1 or -1!
These new possibilities are the result of traces such as thefollowing:
In particular, after one process has updated and printed the global variable, the other process can update it based upon the original un-updated value .
Each of the previous two exercises could be very easily answered, if you were given the program's state space.Draw the state space.
deposit and
withdraw line numbers
and the values of
bal ,
deposit 's
new_bal , and
withdraw 's
new_bal , respectively.Whew! See how much larger this is than the state space of simpler version of this program .
Making the atomicity more fine-grained increases the possibility of concurrency problems. We will use this idea in many of theexamples in this module, because we want to ensure that we can handle even the hard problems. The particular code sequence used inthe previous example is also one of the shortest with a race condition.
In Promela, initialization of a variable and assigning to a variable have subtly different semantics.This is illustrated by this variation on the previous example .
1 /* A variable shared between all processes. */
2 show int bal = 0;3
4 active proctype deposit()5 {
6 show int new_bal = bal;7
8 new_bal++;9 bal = new_bal;
10 }11
12 active proctype withdraw()13 {
14 show int new_bal = bal;15
16 new_bal--;17 bal = new_bal;
18 }
In Promela, initializing variables is part of starting a process.
Thus, all variables of all active processes are initialized(defaulting to 0) before any other statements are executed.
Here, each copy of
new_bal starts
with the value 0, so
bal always
ends with either the value 1 or -1, but never 0.
deposit and
withdraw line numbers
and the values of
bal ,
deposit 's
new_bal , and
withdraw 's
new_bal , respectively.
Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|