MODEX -- EXAMPLES -- November 2012
==================================

To execute the example applications in this directory
you need to have the commands 'modex' and 'spin'
in your search path, plus the usual bevy of
Unix/Linux tools (such as rm, mv, cp, and gcc).

The directory contains some small examples of C source
files with matching Modex test harness definitions.

The first three examples illustrate how we can often do
a full verification of non-trivial multi-threaded code
(meaning, it would take you a while to find the bug with
standard tests, or by manually inspecting the code).
The .prx files contain just a single %X -x command:

	bounds.c	bounds.prx
	pointers.c	pointers.prx
	threads.c	threads.prx

The next example shows a somewhat larger test harness file,
using  %C, %D and %P segments:

	sape1.c		sape1.prx

Here's how we can write that same test harness with
filename references on the same commands.
Note also that this version uses an %F command to point
to the right C source file, which has a basename here that
differs from the basename of the .prx file:

	sape1.c		sape0.prx	// note sape0.prx, not sape1.prx

The next example illustrates the use of %X -n commands
to extract just the body of a function and then place it in
a context that is defined in a Promela (%P) segment.
It also shows the use of explicit data Import commands that
override the default of simply importing all local and global
data objects.

	mutex.c		mutex.prx

Compare this version of the mutex.prx and mutex.c files with the
version shown in http://spinroot.com/modex/MANUAL.html
which shows how to do the verification more directly with just C code.

The next example is an implementation of a double-ended queue, using
a double-word compare and swap instruction (DCAS) for protection.

	dcas.[ch]	dcas.prx

The verification quickly finds a counter-example.

The last few examples show a more elaborate use of conversion
(lookup) tablea defined in %L segments:

	sw_race.c	sw_race.prx
	susp_lock.c	susp_lock.prx
	prod_cons.c	prod_cons.prx	// correct
	prod_cons2.c	prod_cons2.prx	// correct

All except the last two examples produce counter-examples when
verified with modex.

======== Running the Examples ========

To execute a test, you can execute

	../Scripts/verify bounds.prx

or, after you copy the verify script into /usr/local/bin or
your home bin ~/bin (anywhere within your shell search path),
simply:

	verify bounds.prx

You can also directly call modex and type the command:

	modex -run bounds.prx

which performs all steps up to the verification, but does not
replay the error trail if one is found.

At the end of a run you can cleanup all files created with:

	verify clean

The verify script tries to execute a series of commands to perform
the verification, until an error is encountered, or the script completes.
These steps are:

	modex bounds.c		# generate necessary files
	sh _modex_.run		# compile and execute
	sh _modex_.cln		# clean up

_modex_.run and _modex_.cln are also shell scripts,
generated by modex.  the first does something like:

	gcc -E -P _modex_*.drv > model
	spin -a model		# generate the verifier
	gcc ... -o pan pan.c	# compile it
	pan -n ...		# run it
	pan -C			# replay error, if any

Most steps, except _modex_.run, execute quickly.
The run command can take longer because it requires compilations
and the verification itself.
Note that replaying the error trail is always done with
the executable pan itself and not with spin, because of
the use of embedded c-code.

Updated, November 2012
