We begin with a brief explanation of the need for a tool that can trap concurrency related errors, followed by an overview of Modex's basic mode of operation. The main theme introduced here, and that will return throughout this document, is the definition of a Modex verification test harness, which we will just refer to as a test harness from here on. The working of Modex is determined by the test harness definition. Learning to use Modex, therefore, means learning to design and debug relatively simple test harness descriptions.

• Introduction
  • Some Limitations
  • Overview
• How Modex Works
  • Process Communication
  • Checking Assertions
  • Using Temporal Logic
  • Defining Abstractions
• Trouble-Shooting
  • Tracking down what happens
  • Setting Up a Test-Harness
  • Vacuity Checking
• Overview of Test-Harness Commands
  • %F, %X, %L, %H, %D, %B, %C, %P, %O, %Q %R %T %G
• Synopsis of All Modex Test Harness Commands
• References

There are many techniques for evaluating code quality and for reducing the number of residual bugs: manual code walkthroughs, peer review, static source code analysis, and of course plain old unit and integration testing. There is no question that these methods work: they catch bugs, yet they are not perfect. Especially for multi-threaded code, conventional testing techniques have restrictions that limit the number of bugs that they can catch. This is sometimes called the quality ceiling that is imposed by standard testing techniques.

To test a piece of code, either in isolation or in a given context, a tester usually creates a test harness: special instrumentation that is used to efficiently and reproducibly adminster a series of tests and to evaluate the results. At least, this is the intent. The keyword here is reproducibility, and this is precisely what makes it hard to set up a reliable test harness for a concurrent, or multi-threaded, system with conventional techniques.

How can one get a logically or physically distributed system to perform reproducibly, even in the presence of errors? A distributed system typically consists of a number of asynchronously executing processes or threads. The details of the process executions are determined by schedulers. Typically there is one independent process scheduler per host computer in the system. A tester can try to setup a test harness to verify that for any given input the system as a whole will generate the required output, but there is not always a deterministic relation between inputs and outputs in a system like this. The behavior can depend on subtle timings and non-reprodicible interleavings of events. It is hard to tell, at a sufficiently low level of granularity, precisely how process executions are interleaved in time. Yet this knowledge can be of critical importance in tracking down race conditions and timing errors. This is the fundamental problem of limited observability in conventional testing.

A related problem is that even if the tester could know exactly how the process executions had to be interleaved in time to reproduce an error scenario, it is in general not possible to enforce such a schedule in a direct execution. This is the second fundamental problem in conventional testing: limited controllability. In a standard test environment, limited controllability and observability restrict the testers ability to thoroughly exsysterce a system. As a result, some of the most difficult to diagnose bugs can slip through the testing phase and hide as residual defects in production code, with at least the potential of striking at the least opportune moment.

In this document we explore an alternative way of checking distributed systems software that tries to avoid the limitations of conventional testing. We start with a simple example.

	int shared = 0;
	int *ptr;

	void
	thread1(void)
	{       int tmp;
	        ptr = &shared;
	        tmp = shared;
	        tmp++;
	        shared = tmp;
	}

	void
	thread2(void)
	{       int tmp;
	        if (ptr)
	        {       tmp = shared;
	                tmp++;
	                shared = tmp;
	                assert(shared == 1);
	        }
	}

	FIGURE 1. A Simple Threads Example (threads.c)

If we submit this piece of code to a front-end script for the Modex tool, called verify, which uses the small test harness file shown in Figure 3 that we will discuss shortly, the output is as shown in Figure 2. Modex generates an execution trace through the code, showing a columnated interleaving of the statements that are executed by the two threads, leading to an assertion violation: clear proof that such a violation is possible.

	$ verify threads.c
	Extract Model:
	==============
	...
	Compile and Run:
	================
	...
	pan:1: c_code line 24 precondition false: (now.shared==1) (at depth 8)
	...
	Error Found:
	============
	1: thread1(0):[ now.ptr=&(now.shared); ]
	2:              thread2(1):[ now.ptr ]
	3: thread1(0):[ Pthread1->tmp=now.shared; ]
	4: thread1(0):[ Pthread1->tmp++; ]
	5: thread1(0):[ now.shared=Pthread1->tmp; ]
	6:              thread2(1):[ Pthread1->tmp=now.shared; ]
	7:              thread2(1):[ Pthread1->tmp++; ]
	8:              thread2(1):[ now.shared=Pthread1->tmp; ]
	pan: precondition false: (now.shared==1)
	...
	$
	
	FIGURE 2. Sample Analysis of the Threads Example

A few other points are worth observing. First note that the statements that appear in the trace look different than in the original code. Local data in thread1, for instance, is prefixed with a structure reference Pthread1->, or Pthread2->, and global data is prefixed with now.. The names of the threads also have a number added to them in parentheses. The number is the process number (the pid) that Modex assigns to the concurrent process threads. The offending sequence is printed by a program pan that is generated, compiled, and invoked by Modex to perform its test for this code. The reasons for all these peculiarities will become clear shortly.

Modex can determine reliably if there is any system execution that could cause the failure of assertions that are part of the program text. There are three basic types of assertions that can be checked, of which the one from the threads program is the most basic one (and the one that most programmers are familiar with already). More details on these and the other types of assertions can be found in the section on Checking Assertions.

There are also other types of properties that Modex can check for all code that it instruments for a check. These include:

• Indexing errors for statically allocated arrays.
• Pointer dereferencing errors (null pointers).
• The existence of non-progress cycles (starvation loops or live-locks)
• The existence of reachable system deadlocks (invalid terminations).
• Violations of general properties expressed in temporal logic.

Some Limitations

The Modex system targets the verification of multi-threaded software systems, written in the C programming language. In some cases it can be also used for checking basic computational properties of sequential code, but that's not where its strength lies. It would, for instance, not be very good at checking that a square-root routine always functions as advertised, or that a sorting algorithm is implemented correctly. It is, however, very good at diagnosing a broad class of concurrency related problems, including race conditions and system deadlocks.

It is possible to link seperately compiled code into a Modex test harness. These code segments can define system routines and test drivers that can be employed as atomic modules in the test system. The most thorough types of checks that Modex can do, however, rely on its ability to convert C code into verification models. There is currently no support for model extraction from code written in languages other than C.

Modex uses the logic model checker Spin as a background tool to perform the actual verifications. Spin generates an application specific verifier from either hand-written models or from the models produced by Modex. Modex then compiles this code in te background with a regular C-compiler and executes it to find the bugs.

Although detailed knowledge of model-checking techniques is not required to use Modex, some knowledge of model checking tools can be helpful in setting up more complex tests or in diagnosing problems. The user who is familiar with the use of Spin can be at an advantage here. The principles of model checking, and the standard use of Spin is described elsewhere (see for instance [H97] in the reference section).

Function calls in the C code are modeled in a particular way that can impose a restriction in uncommon cases. One syntactic restriction that may disappear at some cases is that the model extractor does not always know how to deal with function calls that appear deep inside the conditional expression of an if, while, or for loop. In those cases you can help the model extractor by moving the function call before the test, for instance as in:

	before:  if (f()) { ... }
	after:   tmp = f(); if (tmp) { ... }

Overview

• process control,
• inter-process communications, and
• the tracking of state information.

For complex applications, the setup of a Modex test can sometimes be simplified if the source code is given a preferred structure. We discuss that structure in the next part of this document and present an example.

Next, we present some guidance in troubleshooting test harness definitions, explaining in more detail what Modex does and how all the pieces fit together.

We conclude with a reference section, reviewing the main components of a test harness definition, covering all commands and controls that can be used.

• user-defined test-drivers,
• native source code fragments (used as is without model extraction), and
• instrumented source code fragments, extracted from from the source code.

• It allows Modex to insert extra assertions into the code that can trap common types of errors, such as out-of-bound array indexing and null-pointer dereferencing.
• It allows the model checker that is used in the background (Spin) to control the interleaving of asynchronous process executions in such a way that relevant interleaving patterns can be enforced systematically and checked.

The level of granularity at which test instrumentation is performed is under user control, giving the user considerable freedom in determining the scope and thoroughness of a system test.

The models Modex can extract from user-selected portions of the source code are largely functional replicas of the original code, represented in the language of the model checker that is used in the background. For more advanced use, Modex allows for the definition of optional filters that can be used to simplify or abstract the version of the code that is going to be checked, for instance by systematically suppressing details that are not relevant to the test at hand. By suppressing detail, the complexity of a check can be reduced.

By defining abstractions as filters, the version of the code that is verified can be tuned without the need for modification of the original source. The modifications are made during the model extraction process, leaving the original source code untouched. Almost all changes that might be needed to perform a verification can be defined through user-defined filters, which can be defined in the test harness and automatically applied during model extractions.

Process control operations include, for instance, process or thread instantiation, suspenstion, and termination. In the threads example that we saw before there were no explicit thread control operations. Through definitions in the test harness the user can determine how many threads there are, which code fragments they execute, when they are suspended and released, how they interact, and when they terminate.

The strength of Modex lies in its support for model extraction and for defining a reproducible test environment for concurrent code, including all the required process control operations. As noted, though, not all of the source code of an application will generally need to be instrumented. In typical cases, verification models are extracted from only a small piece of an application. The remainder of the code can be linked to the generated test system and executed as is.

By choosing which parts of an application are instrumented and which parts are run without instrumentation, the user can trade-off the scope and cost of checks. As a rule of thumb: purely deterministic, and sequentially executing code, that contains no access to shared data, no interprocess communications, and no process or thread control actions, need not be instrumented and can be run as is. Other code should be instrumented through model extraction. The latter is often a relatively small portion of an application, and it can often be made even smaller by structuring the code in a canonical way.

	$ cat threads.prx
	%X -x
	$
	
	FIGURE 3. Complete Configuration File for the Threads Example.

In this case, the specification contains just one command, identified by a command prefix. A command prefix always starts with a percent sign (%) in the left margin, and is followed by a unique letter. There are about ten such commands predefined. Only one appears in this example.

%X is a single-line command, with the parameter to the command placed on the same line as the command name itself. There are also multi-line commands, where the details for the command follow on separate lines. We discuss examples of those later.

%X

Identifies one or more functions in the target C-source file from which Modex should extract a model to be used as part of the verification context being build. The %X command can take a number of different parameters that determine the precise way in which model extraction will be performed. The -x parameter used here tells Modex to extract models from all functions that appear in the target C-source file. By default the functions are extracted from a C source file that has the same basename as the test harness file.

The Modex test harness is used to specify the details of a system test. All the test harness specifications are stored in a single configuration file with suffix .prx, with each command in that file dealing with a different aspect of the verification context.

The test harness defines which processes should be part of the verification, how they interact, and what code they execute. In a typical work-flow, the user starts with some fairly basic assumptions about the test system, and refines it step by step into a more sophisticated test harness, guided by the responses from the model extractor, the model checker, and the C compiler. Each of the background tools is invoked at various points in the process to verify the validity of the code that is being generated.

A test harness generally defines:

• Which processes are part of the test system, and where their definition is to be obtained: from source code via the model extraction engine, from user-defined test drivers expressed in the specification language of the model checker (Promela), or from un-instrumented C code.

• How these processes communicate: Typically we will replace the generic process communication mechanism from the source code with a special purpose mechanism that is used within the test harness. It would, for instance, needlessly introduce processing overhead if the processes were to communicate via socket connections over a real network. A more efficient test can be created by replacing that mechanism with an internal mechanism for passing data through shared buffers. The user can choose here to define the send and receive operations directly in C, or to use the builtin message passing primitives from the model checker.

• Which data objects together define the control state of the system under test. State information typically includes any data object that must persist across different calls of the event processing loop (or its equivalent). Temporary data, or unchanging configuration data, typically does not contain persistent state information. When model extraction is used, Modex can determine which data objects hold state information, and include them in the test system. For code that is outside the pervue of the model extractor, though, it is the user's reserponsibility to identify the relevant data objects and to setup tracking for these in the test harness.

We now take a closer look at some of these issues with the help of examples. We start with a closer look at process control: a central issue in any verification.

The determination of the number of concurrent processes, the code they execute, and their point of instantiation, can be decided in a segment of a test harness that we have not discussed yet: a so-called %P segment.

In the simple threads example from before, two concurrent processes were generated by Modex, one for each routine that appeared in the source code, and both are by default included in the test. In general, we may need more control in determining which processes are part of the test system and what code they execute. In many cases, the code to be executed will be found in the source code of the application, but rarely will all of the source code of an application be required for a meaningful test. Some code can be stubbed, for instance if it interacts with remote systems or processes, or relies on hardware interfaces. We can replace such code with our own test drivers that simulate the possible responses in a controlled manner. Other code fragments may perform routine computational functions that do not involve concurrency or externally visible operations. Such code need not be under the control of Modex, but can be invoked from external code via procedure calls. Modex needs to control only the main threads of concurrency and to monitor possible process interactions.

A %P segment of the test harness, if present, can include declarations of processes that are not defined in the source code itself, e.g. as test drivers that simulate parts of the environment in which the system is to be tested. Such test drivers can simulate, for instance, user input, file system operations, hardware responses. Through the systematic use of user-defined test drivers we can decouple the test system from components over which a tester would otherwise have no direct control In this way we can make all system tests we perform fully reproducible. This process is often closing the system to its environment, to build a standalone test system. The big advantage of specifying test drivers in a %P segment is that we can directly exploit non-determinism, by using Spin's meta-language.

A %P segment does not include definitions for parts of the source code that are to be used in their original form. If, for instance, a call on function that is defined in the original source appears within a test driver, then the assumption is that this fragment of source code will be linked with the test system. We will describe later how this can be done.

	int x, y;

	int
	lock(int Pid)
	{
		x = Pid;
		if (y != 0 && y != Pid)
			return 0;	/* fail */
		y = Pid;
		if (x != Pid)
			return 0;	/* fail */
		return 1;		/* success */
	}

	void
	unlock()
	{	x = 0;
		y = 0;	/* reset */
	}

	FIGURE 4. Flawed Mutual Exclusion Algorithm, file mutex.c

As a small example of the development of a test harness, let us look at the, flawed, algorithm for setting and releasing mutual exclusion locks, shown in Figure 4. No code is shown for user processes that might try to use the lock and unlock routine from this example yet. We need these to exercise the code in any type of test of course, including a formal verification. We have the option of defining the test routines completely inside the .prx configuration file, or we can add them to the C code, and extract models from them as before. We can, for instance, add the following test code to file mutex.c.

	int cnt;
	
	void
	user(int Pid)
	{
		while (1)
		{	lock(Pid);
			cnt++;
			assert(cnt == 1);
			cnt--;
			unlock();
		}
	}

To define the configuration to be verified we clearly have to extract models from the three relevant functions lock, unlock, and user, but they each now plays a different role in the verification. The user function is meant to be executed as a thread of execution. We can extract it directly as an active process, but then we don't have an opportunity to pass it a parameter, which is important here. We can get around this by extracting the user function as a so-called passive proctype, which can then be instantiated separately. We do so with an %X -p command. The other two functions must be represented as instrumented (extended) functions, which we do with %X -e commands. To start up the two threads for the user function we now use a %P segment. This leads us to the test harness specification shown in Figure 5.

	%X -p user
	%X -e lock
	%X -e unlock
	%P
	init {
		atomic {
			run p_user(1)	// the promela process names are
			run p_user(2)	// the function names with prefix p_
		}
	}
	%%

	FIGURE 5. Confuguration File mutex.prx

The syntax used in a %P segment is that of the specification language of the model checker Spin (ProMeLa or Process Meta-Language). The %P segment defines two thread instantiations of the user function (which is generated as a proctype named p_user), passing a different non-zero parameter value to each one.

If we run the verification, the model checker reports quickly that the assertion can be violated, meaning that the lock and unlock routines are indeed unreliable. The model checker generates an example execution, with one possible interleaving of the process executions that leads to this error. The first sequence found is not necessarily also the shortest. If we want to find a short sequence we can add an additional (multi-line) command in the configuration file:

	%G
	shortest: 1
	%%

	$ verify mutex.c
	...
	                user(1):[ now.x=Pp_user->Pid; ]
	                user(1):[else]
	user(0):[ now.x=Pp_user->Pid; ]
	user(0):[else]
	                user(1):[ now.y=Pp_user->Pid; ]
	                user(1):[ (now.x!=Pp_user->Pid) ]
	user(0):[ now.y=Pp_user->Pid; ]
	user(0):[else]
	                user(1):[ now.x=now.y=0; ]
	                user(1):[ now.x=Pp_user->Pid; ]
	                user(1):[else]
	                user(1):[ now.y=Pp_user->Pid; ]
	                user(1):[else]
	                user(1):[cnt = (cnt+1)]
	user(0):[cnt = (cnt+1)]
	pan: error: assertion violated (cnt==1) (at depth 16)
	$

	FIGURE 6. Verification of mutex.c

Process Communication

	typedef struct Msg Msg;
	struct Msg {
		short seq;	/* sequence number  */
		char  *cont;	/* message contents */
	};
	
	void
	abp_sender()
	{	Msg m, ack;
	
		m.seq = 0;
		ack.seq = 0;
	
		for (;;)
		{	if (ack.seq == m.seq)
			{	if (fetch_data(&m.cont))
				{	m.seq = 1 - m.seq;
				} else
				{	break;	/* no more data: done */
			}	}
			send(m);
			receive(&ack);
		}
	}
	
	void
	abp_receiver()
	{	Msg m, ack;
		short expect = 1;
	
		for (;;)
		{	receive(&m);	/* get new msg */
			ack.seq  = m.seq;
			send(ack);
			if (m.seq == expect)
			{	store_data(m.cont);
				expect = 1 - expect;
		}	}
	}


	FIGURE 7. Alternating Bit Protocol

The receiver performs a simple check on the validity of the incoming messages, and if the check is passed it stores the data. The receiver acknowledges all messages received, valid or invalid, by returning an empty message with a copy of the sequence number from the incoming message back to the sender. The sender will only fetch a new message to send when it receives the correct acknowledgment, otherwise it resends the last message. The sender also will get things started, which we arrange for by making it seem as if it has the correct acknowledgement from an earlier message.

	%F abp.c
	%X -L abp_snd.lut -a abp_sender
	%X -L abp_rcv.lut -a abp_receiver
	%L abp_snd
	Declare	bit	s	abp_sender
	fetch_data(...	true
	send(m)		c_code { Pp_abp_sender->s = Pp_abp_sender->m.seq; }; \
			qr!s
	receive(...	qs?s; \
			c_code { Pp_abp_sender->ack.seq = Pp_abp_sender->s; }
	%%
	%L abp_rcv
	Declare	bit	s	abp_receiver
	store_data(...	skip
	send(ack)	c_code { Pp_abp_receiver->s = Pp_abp_receiver->ack.seq; }; \
			qs!s
	receive(...	qr?s; \
			c_code { Pp_abp_receiver->m.seq = Pp_abp_receiver->s; }
	%%
	%P
	chan qs = [0] of { bit };
	chan qr = [0] of { bit };
	%%

	FIGURE 8. Test Harness for Sender and Receiver

A test harness we'll discuss for this application is shown in Figure 8. It is a little bit more involved than the earlier examples, mainly to illustrate some of the additional capabilities there are in Modex to influence the model extraction process. The initial part is now familiar. We start with an %F command to identify the source file used. If the code for the sender and the receiver would be located in different files, we'd have to identify each one with a separate %F command that immediately precedes the corresponding %X commands. We have two %X commands here, one for the sender and one for the receiver, and we specify a dedicated lookup table for each one.

We define the two %L segments, one for each process. In this case this isn't really needed, but the example shows how it is done.

We now want to map the send and receive operations into Promela equivalents, using a variable of type bit to store the sequence number. So the first thing to do is to declare that extra variable, that does not appear in the source code, as a modeling variable with a Declare statement. We do so in each of the two lookup tables. Next, we tackle the semantics of the fetch_data routine. For this verification attempt we assume that there will be an infinite stream of data to be transmitted, meaning that the fetch_data routine always returns a non-zero result (true). The working of the protocol itself furthermore is independent of the actual data that is being transmitted as payload in the messages, so we can ignore the generation and consumption of this payload data in the test framework. In the lookup table for the receiver, therefore, we can also replace the call on store_data with skip. The use of sequence numbers, however, is important and must be preserved.

A more interesting part of this test harness is the representation of the send and receive operations in the two processes. Long entries in the lookup table can be split across multiple lines, like macro definitions in C, by using a backslash as a continuation character at the end of a line. The send operations can be represented in C, in Promela, or some combination. Here we're using a combination of both, to illustrate how this works.

Two Promela channels are declared in a %P segment of the test harness (the P stands for Promela code). The channels are declared as rendezvous channels with a zero capacity. Using synchronous channels is often attractive in model checking applications, because it generally reduces the complexity of a verification. Since we can abstract from data contents, each message is given just one field of type bit, to store the sequence number. We can send and receive via these channels with the Promela primitives q!s and q?s, respectively, where q is the channel and s is the sequence number sent or received.

Now we have to resolve the problem that the data to be sent is in a C data structure that may not be representable in Promela (actually, in this case it can be represented with a structure definition in Promela, but in general this is not always the case). So, we copy the data from a C data object into a Promela data object with a c_code statement, and vice versa. Within c_code statements, the references to state variables have to be prefixed with either now. or Pp_procname->. In the case of the sender the prefix becomes Pp_abp_sender-> for both the Promela object and the C structure reference.

Finally, the definition of what a Msg structure is must be made known to the verifier as well, because the send and receive routines rely on it. We do so here with a %D segment, as shown.

There are several things we could check for this implementation of the alternating bit protocol at this point. We could formally demonstrate the above observation about the required initial trigger for the transmission. We could check if it is possible for this system to reach a state from which no data will ever be accepted again, wether the system still has hidden deadlock or hangup states, etc. These features are best understood in the domain of model checking, so we will not discuss them in more detail here.

Checking Assertions

Modex supports three types of assertions that the user can add to code: basic assertions, response assertions, and precedence assertions.

• A basic assertion has the form assert(expression). Modex will check that the expression evaluates to true whenever the assertion statement is reached, in all feasible system executions.
• A response assertion has the form assert_r(expression). For a response assertion Modex checks that the expression evaluates to true within a finite number of steps after the assertion statement is reached, in all feasible system executions. The expression is required to become true in all system executions.
• A precedence assertion has the form assert_p(expression1, expression2) For this type of assertion Modex checks that expression1 is true each time this assertion is reached and remains true at least until expression2 becomes true. The second expression, however, is not required to become true.

For example, if the source code contains a statement

	assert(x > y);

	assert_r(x > y);

	assert_p(x < 10, x > y);

Using Temporal Logic

Defining Abstractions

Abstractions are always defined at the statement level, which means that you cannot directly define control-flow abstractions with this method. This, however, does not appear to be a restriction, and it has the benefit of significantly simplifying the model extraction process and the definition of abstractions. What abstractions are used is completely up to the user and is not restricted by the model extractor. For guidance and inspiration, check the set of examples of test harness definitions that comes with the standard Modex distribution.

The model extractor starts by preprocessing each C source file that is mentioned in a test harness %F command. It calls the standard C preprocessor to do this. Since this is usually the first action that is executed, it is also the first thing that can fail. It can fail, for instance, if there are missing compiler directives, missing header files, syntax-errors in the C code, etc. The errors are often reported as appearing in a file with the extension .I which is intermediate version of the source file that is generated by the model extractor. As a rule, first make sure that you can compile the C sources with the regular C compiler, before trying to extract models from them. The model extractor is a little more forgiving for certain types of omissions or errors, but it too has its limits of course.

The result of a successful preprocessing step is placed in a temporary file with extension .M, where future calls on the model extractor will look for it. (An intermediate version with extension .I is removed more quickly.)

Next, the model extractor will parse the preprocessed file to prepare for model extraction. Errors can be reported in this phase as well. The most common causes will be missing type declarations (caused by missing header files), syntax errors, etc. Missing information can be provided in %D segments. The extractor by default will try to ignore system header files, to avoid trapping lots of unnecessary data and declarations. In most cases this works well, but in some cases there are critical type declarations in the system header files that must be picked up. In those cases the model extractor can be forced to read and interpret all header files by calling it with option -z.

If all is well, the model extractor will generate a number of files with portions of the extracted code. The main file among these is a file with extension .drv (driver). Another file has extension .cln which is a script to cleanup (remove) all temporary files that were generated. The third file used has the extension .run, and it contains a script that can be executed to perform the actual verification. If the model extractor is invoked with the argument -run then this script will be called automatically as soon as the model extraction is completed.

Executing the run script will first cause another call on the preprocessor, this time to process the generated Promela code. This will expand the contents of the .drv file, and everything it refers to, into a single file named model. This will generally be the best place to look at what the model extractor actually generated from the test harness and the source files.

Next, the model checker Spin called with the file model as its input. Clearly, Spin too can generate error reports if the code it finds is not to its liking. Causes could be bad entries in the lookup tables, missing declarations, missing Import commands in the test harness, etc. If it succeeds in parsing the model, Spin generates the verifier in a set of C source files named pan.[chmbpt].

The pan.c file is now compiled with the standard C compiler. Again, errors can now reveal themselves if, for instance, the encapsulated C code is incorrect, if there are missing declarations etc. If you are familiar with the code in the pan files, looking at the data structures that are generated for each process and for the global state vector can sometimes be helpful in tracking down the cause of errors. In virtually all cases, though, errors uncovered in this step come down to omissions or mis-statements in the test harness, so ultimately this is where the errors will have to be repaired.

If compilation succeeds, we are not quite out of the woods yet. Also the execution of the model checking code can fail, with memory errors or core dumps. Bad code from the original source files, or bad replacement code from the lookup tables, will generally be the cause, which can be tracked down with standard debugging techniques.

Tracking Down What Happens

	void
	main(void)
	{
		printf("hello world\n"); /* shows up in pan.m */
	}

	FIGURE 10. Hello World

	%F hello.c
	%X -x
	%L
	printf(...	keep
	%%
	%H
	struct A { int foobar_t; };	/* shows up in dummy.M, but not in model */
	%%
	%D
	typedef struct d_part {
		int d_1;
		char d_2;
	} d_part;		/* shows up in pan.c before pan.h */
	%%
	%C
	State c_part;		/* shows up in pan.c after pan.h */
	%%
	%P
	int p_part;		/* shows up in pan.h inside state vector */
	%%

	FIGURE 11. Dummy Test Harness for Hello World Example

To make it easier to see how the final model is composed, invoke Modex with the special -Y debugging command, which preserves all intermediate files so that we can inspect them.

	$ modex -Y hello.c

	$ cat model

	c_decl {
		typedef d_part {
	 		int d_1;
	 		char d_2;
		} d_part;
	}

	c_code {
		State c_part;
	}

	int p_part;

	active proctype main( )
	{
	     printf("hello world\n");
	}
	$

The %X -x command in the test harness selects target main for model extraction. The %L segment contains just one command, which is meant to override the default treatment of printf statements. Unless otherwise defined, the model extractor uses the default conversions shown in Figure 12.

	open(... 		comment
	close(... 		comment
	fflush(... 		comment
	exit(... 		comment
	fprintf(... 		comment
	printf(... 		comment
	write(... 		comment
	fgets(... 		warn
	fscanf(... 		warn
	read(... 		warn
	connect(... 		warn
	socket(... 		warn
	gethostbyname(... 	warn
	getprotobyname(...	warn

	FIGURE 12. Default Conversion Rules

Most POSIX file operations, except those that read data, are converted into comments. Operations that retrieve data from a file must be treated with some care, since their effect is not necessarily reversible, and modifies potentially relevant state information. The use of these operations within a procedure that is to be instrumented by the model checker will generate a warning.

In this case we want the printf statement preserved so that we can see where it ends up in the model checking code.

Spin takes the model generated by Modex and turns it into a C program. That program consists of the following set of files:

	pan.h, which contains all header information, and data declarations,
	pan.c, which contains the model checking procedures,
	pan.m, which contains the code generated for each transition in the system,
	pan.b, which records how the effect of each transition can be undone,
	pan.t, which records the control flow structure for all generated process types.
	pan.p, which contains code for supporting multi-core model checking runs

%H The declaration of the typedef, given in the %H segment of the test harness, would at first seem to have disappeared, since it does not show up literally in any of the pan.? source files. It does appear in another file that is automatically created in the directory where the hello world example is stored though. This intermediate file has the extension .M, and contains the output of the preprocessing phase for the target source file.

If there are multiple target source files, then the results of preprocessing each file will be stored in a separate .M file. The model extractor will not extract its model from the original .c file, but from the intermediate .M file that is created after all relevant include files are inlined and all macros are expanded. Before the model extractor starts, it always checks if there is already an .M file in the directory that is more recent than the .c file. If so, the model extractor will skip the preprocessing step and move straight on to the processing of the .M file. This can sometimes also have undesired consequences, for instance if a file that is included into the original source file is updated. The update may then be invisible to the model extractor, which will continue to work with the previously produced .M file, missing the update. If this happens, you can force the update by removing the .M file manually.

Our declaration for struct A appears at the top of the file dummy.M together with any other entries that could be specified in an %H segment (such a macro definitions). No preprocessing is done on these entries: they are copied literally into the .M file. In this case, the structure declaration would allow us to use declarations of this type elsewhere. This is not used here, so the declaration does not show up in the model itself. We can also use entries in the %H segment to rename data objects with macro definitions, etc. We can in this way make small changes to the original source code of an application without having to directly modify that code. The %H segment gives us a way to add small overrides into the code through definitions that are recorded in the test harness.

%D The declaration of the data d_part from the %D segment of the trial test harness is turned into a c_decl statement that will next show up in the main file pan.c before the point where the pan.h header file is included. This therefore gives us a way to introduce data types that can be refered to from within the state vector.

%H vs %D Declarations that are placed in the %H segment modify the source code of the application before model extraction takes place. Declarations placed in %D, %C, and %P segments modify the target code of the model checker after model extraction takes place.

%D vs %C The declaration of c_part from the %C segment is turned into a global c_code fragment, that shows up in the pan.c file after the point where pan.h is included. This gives us a way to refer to the state vector (State) itself, or to any other items that are included in the pan.h file, both in declarations and in C procedure definitions. From their relative placement in the code, the %D segment of the test harness is the logical place for data Declarations, while the %C segment is the logical place for defining the body of C functions that are to become part of the verification system.

%P The declaration of the integer p_part, finally, become part of the generic model that is produced, and shows up inside the state vector itself, which is defined in the file pan.h. Note that the %P segment introduces Promela code, and therefore the declaration of p_part is treated as a global Promela object that is automatically declared as such, and that could be refered to from within C procedures under the extended name now.p_part.

Setting Up a Test-Harness

The most challenging part of working with Modex is often in the initial definition of a test harness. Once the test harness is set up, there is relatively little maintenance to be done and things progress very fast.

When starting from scratch for a new software application, there are some guidelines that can be followed about the best way to proceed from step to step. Below we will walk you through a series of manual steps that can be made from the command line to reproduce the main processing steps that Modex normally performs automatically in sequence. This is just for trouble-shooting purposes, or perhaps to explain in more detail all that happens behind the screen in a session with Modex.

To successfully complete a software test with Modex, we have to setup the test harness to take us passed a series of hurdles. Each step in the process can in principle fail, and generate an error message. By eliminating the causes of each error reported one by one, we can converge quickly on a usable test harness description. Below we discuss the main steps taken by Modex in a little more detail.

Note that all steps below can be executed automatically by Modex if you pass it the runtime option -run.

Step 1

Step 2

	$ modex -Y -k check.prx

	#ifdef MODEX
		some declarations to satisfy the modex parser
	#endif

We generally need to select and redefine only a small fraction of the entries in the default %L segments that are generated to setup a check, so do not be discouraged if this initial listing is long. The main purpose of the listing is to provide us with a precise spelling of the left-hand side entries from the source statements for which we may want to introduce a conversion rule in the mapping tables.

Step 3

	$ modex check.prx

Step 4

	$ spin -a model		# using a reasonably recent version of spin

Step 5

	$ gcc -o pan pan.c

Step 6

	$ ./pan

Step 7

By default the search it limited to a depth of 10,000 steps. To set a different depth-limit, say a shorter one of only 100 steps, you can use

	$ pan -m100

	$ gcc -DBITSTATE -o pan pan.c

	$ ./pan -w20
	$ ./pan -w22
	$ ./pan -w24

	http://spinroot.com/spin/Man/

	./pan -C

Vacuity Checking

Just as a quick indication of which commands are most important, we can look at some statistics from the definition of the Modex test harness definitions for the 25 challenge problems in the concurrency category of the TACAS 2012 model checking contest. All problems can be handled by Modex and verified based only on the C source code provided. The number of times that each of the ten available commands is used in all 25 test harness files combined is as follows:

     68 %X
     25 %F
     21 %L
     16 %H
      6 %C
      5 %O
      4 %P
      2 %D
      1 %G
      0 %Q
      0 %R # was added in 2014
      0 %T # was added in 2013

When the model extractor encounters a named %L command it will first try to open a file with the name that follows %L. If this fails then the name is used to identify the lookup table contents that follows on the following lines, up to a %% closing symbol. A single line %L command, refering to a named file, is also considered to be a named lookup table, where the prefix of the file name serves as the reference.

We have already seen some examples of many of the test harness commands, but we have not used not all ten. We will review all commands below and give a synopsis of their intended use, and possible parameters. We will do so in the most likely order in which these commands would be used in a test harness. The order can help structure a test harness specification, but is otherwise not strictly important. There is just one exception to this rule where order does matter: an %X command always refers to the last preceding %F command. A test harness file therefore usually begins with an %F command.

%F

%X

Valid Parameters to an %X Command

Options -a, -e, and -xe can optionally be followed by a small integer number that specifies how many instantiations of the process should be created. For instance,

	%X -a3 foo

The -x option does not take an argument, since it targets all functions found in the current source file. The remaining option flags take exactly one function name as an argument. Each option flag can be preceded by a -L option that specifies a named mapfile that is to be used for this extraction.

The recommended format is to group options that relate to the same target of a model extraction command on the same command line. For instance:

	%X -L map1 -a p1
	%X -L map2 -n p2

Valid %G Options

%L

There can be any number of mapping tables, but only one unnamed one, and only one for each unique name used. The main purpose of a mapping table is to define conversions from statements or conditions that appear in the source text, into abstracted versions that are used in the model. There is a predefined conversion that simply encapsulates each statement in a Promela c_code fragment and each condition in a Promela c_expr statement, while adjusting all variable references for the imported data. A user-defined conversion is therefore only needed when the default isn't adequate.

A conversion rule can be used to suppress pieces of code that are outside the check, to simplify or abstract pieces of code, or to lift certain operations up to the level of the test harness, overriding the builtin functionality of the application itself. This would, for instance, be done if the real application environment is replaced with a set of test drivers that simulate all the behaviors of interest of that environment in a controlled way. Send and receive operations are typically replaced with test artifacts in this way, process control and thread control operations similarly are usually replaced with model specific equivalents.

There are also a small number of special commands that can be used within a mapping table. These special commands are summarized below.

		Lookup Table - 7 Special Commands

	Constant zero	one

	Include shared.lut

• first the name of a data object, then
• the type of that object and finally
• the scope of that object.

	Declare struct rlV5IFDB	ifdb_11	Global
	Declare int		number	main

• the name of a data object that appears in the source file, and
• the scope of that object.

	Import	ifdb_11	Global
	Import	number	main

• first is either they keyword hidden or the type of a data object.
• The second argument is the name of the data object.

	NonState V_State	*tossinfo
	NonState char		dummy[64]
	NonState hidden		a[]

• The first argument is a text-string that is to be replaced with
• the second argument after all other mapping table commands have been applied.

	Substitute   c_code { mutex_unlock(&(now.m_busy)); }   m_busy = 0

• The first argument is a pointer to a data object that is declared externally to the code managed by the model checker (i.e., code that will be linked with the model checker to perform an executable for the test system).
• The second argument defines the size of that object.

	Track  &heap	sizeof(heap)

All other entries in a mapping table that do not match the above special commands are interpreted as conversion rules. A conversion rules always consists of two parts, separated by one or more tabs. The left hand side of the rule specifies the source text to be replaced, and the right hand side defines the replacement text of that piece of source code in the extracted model.

There are a few short-hands that can be used on the right-hand side of a conversion rule. The available short-hands are summarized below.

	Predefined Mapping Keywords in Lookup Tables

There is an additional type of pattern that can be used on the left-hand side of a conversion rule. Any text-string that ends in three dots is understood to be a prefix of a code fragment, and it will match any statement or expression that begins with the string before the three dots. For instance:

	printf(...	warn

If multiple matches are possible, the first match encountered in the scanning of the mapping tables will take effect. A named mapping table is always scanned first. A default unnamed table is scanned last.

%H

%D

%B

%C

%P

%O

	%O ipc_stubs.o Downlink.o

%Q

	%Q -DCPU=SIMSPARCSOLARIS -DFSW_UNIT_TEST -IWind

%R

	%R -a

%T

	%T sed 's;goto ERROR;assert(0);'

	%T sed 's;goto ERROR;assert(0);' | sed 's;pthread_exit.*;;'

%G

    Command	  Meaning

    Single-Line Commands:
    --------------------
    %F fname	  Set target C source filename, fname, for subsequent model extractions via %X commands

    %X -x	  Extract all procedures from the target C-source file
    %X -xe	  Extract all functions as extended proctypes from the target C-source file
		  Optionally: -xeN for N parallel instantiations
    %X -a pname	  Extract procedure pname as an active proctype
		  Optionally: -aN for N parallel instantiations
    %X -i pname	  Extract procedure pname as an inline definition
    %X -p pname	  Extract procedure pname as a passive proctype
    %X -e pname	  Extract as instrumented function (with instrumented calls)
    %X -f pname   Like -e, but with the function executing atomically
    %X -E pname	  Extract procedure as an instrumented passive proctype
    %X -n pname	  Extract procedure pname without proctype encapsulation
    %X -L mapname Define a map to be used in subsequent model extractions
    
    %O		Define compilation directives and external C-files
    		for compilation of the verifier, e.g., %O -DVECTORSZ=2048
    
    %Q		Define directives for preprocessing source from which
    		models are to be extracted, e.g., %Q "-Dshort=int"

    %R		Define runtime flags for the verification phase, e.g., %R -a

    %T		Preprocessing command for the source. Typically a sed-command.
    		e.g., %T sed 's;foo;bar;g'

    Multi-Line Commands (concluded with a %% on a single line):
    ----------------------------------------------------------
    %L		Define a conversion/mapping table to be used in model extraction via %X commands

    %H		Define optional header information for generated code
		(Can also be used as a single-line command, when given a filename with the details
		e.g., as in %H "filename.h")
    
    %D		Declare C data types used in the generated code (w. optional single-line format, see %H)
    
    %C		Introduce arbitrary C code into the model (w. optional single-line format, see %H)

    %P		Define process infrastructure in Spin modeling language (w. optional single-line format, see %H)
        	The part of the model defined here precedes all other extracted parts in the final code.

    %A  	Same as %P, except the part of the model defined here is placed after all other parts.

    %G		Possible parameter settings, with their default values:

    		maxdepth: 1000	# Limit search depth for model checking to 1000 steps.
    		memlim:    350	# Limit memory use for model checking runs to 350 Mbytes
    		loops:       0	# Do no search for accept cycles (0 or 1)
    		np_loops:    0	# Do not search for non-progress cycles (0 or 1)
    		noend:       1	# Do not search for invalid endstates (0 or 1)
    		asserts:     1	# Search for assertion violations (0 or 1)
    		shortest:    0	# Not necessarily the shortest possible error (0 or 1)
    		quality:     3	# Set a medium search coverage (range 1..10);
    				# 1 gives maximal speed, 10 gives maximal coverage
    		exhaustive:  0	# do not/do force exhaustive search coverage (0 or 1)
    		io_only:     0	# List all operations in MSCs, not just i/o (0 or 1)
    		use_vals:    0	# Do not display parameter values in MSCs (0 or 1)
    		zflag:       0	# Do not process system header files when preprocessing
    				# source files for model extraction (0 or 1).

[HS99a] G.J. Holzmann and M.H. Smith, "A practical method for the verification of event-driven software," Proc. Intern. Conf. on Software Engineering, May 1999, Los Angeles, CA., pp. 597-607. (PDF)

[HS99b] G.J. Holzmann, and M.H. Smith, "Software model checking: extracting verification models from source code," Software Testing, Verification and Reliability, Vol. 11, No. 2, June 2001, pp. 65-79. (PDF)

[H00] G.J. Holzmann, "Lecture Notes on Software Model Checking," NATO Summerschool, Aug. 2000, Marktoberdorf, Germany. (PDF)

[HS00] G.J. Holzmann, and M.H. Smith, "Automating software feature verification," Bell Labs Technical Journal, Vol. 5, No. 2, April-June 2000, pp. 72-87. (PDF)

[H00] G.J. Holzmann, "Logic Verification of ANSI-C Code with Spin," Spin Workshop, Stanford University, CA., Aug-Sept. 2000, Springer Verlag, Lecture Notes in Computer Science, Vol. 1885, pp. 131-147. (PDF)

[H01] G.J. Holzmann, "From Code to Models," Proc. 2nd International Conference on Concurrency to System Design, Newcastle, U.K., IEEE Computer Society Press, June 2001, pp. 3-10. (PDF)

[H04] G.J. Holzmann, "The Spin Model Checker - Primer and Reference Manual," Addison-Wesley, 2004. (URL)