| << Chapter < Page | Chapter >> Page > |
All the traces of a Promela program start at the same initial state . Any variables not explicitly initialized by the code areset to particular known values: zero, for numbers; and false, for booleans.(Compare to a C program, where two traces of the same program might each start from a different state.)And we've just seen that different traces may end in different states,or they may sometimes end in the same state while having taken different paths to reach that end state.Finally, if we look closely at all the possible traces, we see thatoften, several different traces might happen to pass through the same intermediate state.By combining the traces at these common states, we can depict the entire state space a map of all the conceivable executions of our program!
The above is the state space of the Tiny First Program's code . The states are shown with the value of the only variable's value,plus the program point of each process. The edges are shown only as arrows, as the change in line numbersindicates which statement's and thread's execution each represents.
The possible traces are then all the different paths in the state space.State spaces are primarily helpful for understanding how to verify concurrent programs, and will be used mostly in the next section .
xspin by the "Run" menu's option to
"View Spin Automaton for each Proctype".Also, the state numbering of this per-process form is reported
by SPIN's output of traces.There is a close relation between the two forms, as
the whole system is intuitively some sort ofcross-product
of the individual processes.We now modify the previous example. The two assignment statements have each been broken up into threestatements. These three simulate a typical sequence of machine-level instructions in a load/store style architecture.This is a way to model that level of atomicity within Promela.
1 /* A variable shared between all processes. */
2 show int bal = 0;3
4 active proctype deposit()5 {
6 show int new_bal;7
8 new_bal = bal;9 new_bal++;
10 bal = new_bal;11 }
1213 active proctype withdraw()
14 {15 show int new_bal;
1617 new_bal = bal;
18 new_bal--;19 bal = new_bal;
20 }
Here, each process has its own local variable named
new_bal .
Note that we can also have SPIN
show local variables in the
"Message Sequence Chart" window.Run this code as described in the previous example.
Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|