1. Home
  2. Model checking concurrent
  3. Model checking concurrent
  4. Modeling concurrent processes

0.3 Modeling concurrent processes  (Page 2/21)

<< Chapter < Page
  Model checking concurrent     Page 2 / 21
Chapter >> Page >

After loading or typing a program, it's always a good idea to check your typing. In the "Run" menu, use "Run Syntax Check".It will report and highlight the first syntax error, if any.

Before the first run, you need to specify some parameters, even if those are the defaults.From the "Run" menu, select the "Set Simulation Parameters" option. Change the "Display Mode" defaults, by making sure that the"MSC" and "Data Values" panels are each selected, as well as each featureunder the "Data Values" panel. Use the "Start" button to start the run.This opens three new windows. From the "Simulation Output" window, you can choose to single-step therun or let it finish. For now, choose "Run". The body of this window displays each step taken.Throughout the run, the "Data Values" window displays the values of variables. The "Message Sequence Chart" displays changesto each process and variable. Each column represents a separate process or variable, and the verticalaxis represents time. For now, the only changes to processes arewhen they stop.

Each process gets a unique process identifier number, starting with 0. These are displayed in the output of the various windows. Later , we will see how to access these IDs from within the Promela program.

For additional runs, from the "Run" menu of the main window, you can select"(Re)Run Simulation". However, each run will be identical, because it makes the same choicesfor interleaving. To vary runs, or traces , change the "Seed Value" in thesimulation options. Also, be sure to try the "Interactive" simulation style, where you make each choice in the interleaving.

Each xspin run opens several new windows, without closing the old ones.The easiest way to close the windows for a run is to use the "Cancel" button in the "Simulation Output" window.
Experiment with the other display modes in the simulation options to see what else is available.
Running a basic simulation is one of the few things which is easier in spin than xspin , since you don't need to setany of the simulation parameters: prompt>spin filename .pml
State
A snapshot of the entire program. In Promela, this is an assignment to all the program's variables,both global and local, plus the program counter, or line number, of each process.In other languages, the state also includes information such as each process' stack contents.
Trace
A sequencepossibly infiniteof successive states, corresponding to one particular run of a program.

How many traces are possible for the previous example's code ? Does each end with the same value for bal ?

The two possible traces for the above program.

Did you see each one using SPIN? Each trace ends with bal equal to 0, as expected.

There are some minor differences between SPIN's behavior and the somewhat simplified conceptual behavior that we aredescribing;see the following list
  • SPIN adds an extra transition and state at the end of each process. You can think of the transitionas the process exiting, but it doesn't change any of the variables' values.We omit this, except for one homework exercise .
  • Marking variables with show introduces transitions and states to display their changing values. We have omitted these.
  • Finally, as a minor presentational detail, SPIN doesn't report the start state of a trace like we do.
<< Chapter < Page Page > Chapter >>

Read also:

Get Jobilize Job Search Mobile App in your pocket Now!

Get it on Google Play Download on the App Store Now




Source:  OpenStax, Model checking concurrent programs. OpenStax CNX. Oct 27, 2005 Download for free at http://cnx.org/content/col10294/1.3
Google Play and the Google Play logo are trademarks of Google Inc.

Notification Switch

Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?

Ask