CMU 15-671Models of Software SystemsFall 1995
Shared Memory Model
Garlan & Wing Handout 13 30 October 1995
This handout addresses the question ``How do you model a shared memory model of concurrency with state machines?''
Let's consider the simple example from the Concurrency handout. We have a single shared integer variable x, initialized to 0, and two processes, P and Q, each of which executes the same code:
x := 1
x := x + 1
We have these interleavings:
 | | |
 |  | |
|
| |  |
|
| | |
 |  | |
plus all three symmetric cases. Here is part of the state transition diagram:
where each statement labels a state transition arrow and the current value of x labels each node. Note two things:
First, having an arrow (indicated as a dashed line in the diagram) from ** to its predecessor rather than to a new node with the same label would be wrong because we would introduce a loop, and thus an infinite trace (one we do not expect for the behavior of this example). It's wrong because the nodes labeled x = 1 are really different. The x = 1 node with * next to it corresponds to the state we get to after P does its first action but Q has not done anything yet. The x = 1 node with ** next to it corresponds to the state after P has completed and Q has done its first action. Thus, we need to keep track of what P and Q have done already. Thus, the state transition diagram is missing some information-- because although the two nodes are labeled the same they represent different states in the computation. Thus, we need to keep track of this missing information. In general, we need to keep track of where P and Q are in their respective code sequences.
The obvious and natural way to keep track of this information is to model explicitly the program counter of each concurrent process in our system. Thus, as part of each state in our state machine model we include a program counter for each process. As part of the effect of each state transition, exactly one of the program counters gets incremented.
Second, just as we now have a way to distinguish between nodes that look similar, we need a way to distinguish between state transitions that look similar. As we have already been doing informally, we simply tag each statement with the name of the process that executes it.