| << Chapter < Page | Chapter >> Page > |
We will model concurrency in two ways. First, we will use Promela, a language with C-like syntax.It is not a fully featured programming language, and is not intended for general computation. Instead, Promela(PROcess MEta-LAnguage) programs are intended to be simplifications or models of real-world systems, for use inverification. SPIN (Simple Promela INterpreter) is the tool for executing and verifying programs written in Promela.Second, we will use a simple state-based transition system that will help in understanding the specification and verification of Promelaprograms.
Here, we introduce Promela, SPIN, and the state-based transition system through a series of examples.For the moment, we will use SPIN merely as an interpreter, to run of Promela programs.In the next section , we will introduce the verification featuresof SPIN. ( Reference manuals and download/install instructions are available via the SPIN homepage, spinroot.com .)
We start with a series of examples illustrating race conditions.
1 /* A variable shared between all processes. */
2 show int bal = 0;3
4 active proctype deposit()5 {
6 bal++;7 }
89 active proctype withdraw()
10 {11 bal--;
12 }
We have two threads, one running
deposit and one running
withdraw .
The
proctype keyword specifies
that the following is code for a thread/process, while the
active keyword specifies that
the thread is started immediately when we start the program.Variables declared outside the body of a
proctype are shared.
The keyword
show before a
variable declaration will directSPIN to display the value as it changes.
Here, the two processes of
deposit and
withdraw can interleave
arbitrarily. Regardless, with this very simple example,we will always get the same result balance.
To run the code, we use SPIN. We'll describe how to use the
program
xspin , which uses
a graphical interface.More specifically, these instructions are for UNIX version 4.1.3.
The PC and Mac versions are identical, except for how to startthe program. For details, see the program's
README .
Ask your local system administrator where the program is installedon your computer.
spin .
It is more difficult to use interactively, but is appropriatefor use non-interactive use, such as with scripts.
For its options, see the manual pages for
spin and the related
pan .
xspin is just a graphical front-end to
spin .
The underlying
spin commands and output
are displayed atthe bottom of the main
xspin window.
These can be ignored.xspin or
spin from Rice University's Owlnet, first type
setenv PATH /home/comp607/bin:$PATH .Within SPIN, you'll work with a Promela program.
If you already have a Promela program saved, you can open it withthe "File" menu's "Open" option.
Alternatively, start SPIN with the Promela program's filename:
xspin
filename .pml (The conventional suffix for Promela programs is
.pml .)
Either of these loads the Promela code into an editor window,where it can be modified.
To create a new program, you can type into this window, or you cancopy and past it from another editor.
Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|