IBM
Contents Index Previous Next



Validating Systems with External C Code


the SDL Suite allows the usage of external C code together with an SDL system and this is also true for the Explorer. In many cases it is possible to directly use the Explorer on a system that uses external C code. However, due to the special requirements of state space exploration, some restrictions must hold for the external C code, and some modifications may have to be done to the external code to make it functions properly with the Explorer.

To be able to perform a state space exploration it must be possible for the Explorer to make a complete copy of a system state, including all data structures that are implemented directly in C code. The Explorer must also be able to modify each copy of a system state separately. This has some implications:

If there are variables in C code, this will not be detected by the explorer. It may appear as if the Explorer works, but the variables defined in C code will not be copied when the Explorer copies a system state. When the value of a variable is changed by an action performed in one system state, this value will change the value for all system states that the Explorer currently handles. This implies e.g. that when the Explorer backtracks during an automatic exploration to test more possible successors of a particular system state, the values of variables defined in C may be different from the values they had the previous time the system state was visited and the state space exploration will not be correct.

In order to be able to copy a system state, the Explorer must have exact information about the sort of all data areas in the system to be able to copy e.g. pointer-based data structures correctly. One consequence of this is that the Explorer cannot support the C union sort if the union may contain pointer-based sorts, since the Explorer cannot know the current sort of the union and thus cannot deduce whether to treat the union as a pointer or not. SDL PIds are also treated specially in the Explorer and can also not be part of a C union.

Pointers are frequently used in C code and when used together with the SDL Suite they are treated as the (nonstandard) SDL type Ref. The Explorer handles the Ref types in a particular way (see Validating Systems That Use the Ref Generator) and the restrictions on variables of this sort also applies to the usage of C pointers in data type in external C code.

When using dynamic memory allocation in extern C code some special additions are needed for the Explorer to work properly. This is needed since the Explorer keeps a list of all dynamically allocated data areas as part of each system state. If an external C function allocates memory, the Explorer must be informed about the data area that was allocated, and the same holds when a C function releases memory. This is accomplished by calling two functions from the C code:

extern void UserMalloc (void *data);
extern void UserFree (void *data);

UserMalloc should be called when a data area has been allocated, and UserFree should be called immediately before the data area is released. Both functions should have a pointer to the data area as parameter.

The purpose of UserMalloc is to insert a new element into the list of dynamically allocated data areas that is maintained by the Explorer. Note that there is no need to tell the Explorer what sort of data was allocated or its size. This is handled automatically by the Explorer simply by finding the SDL entity (e.g. a variable) that points at the data area and assuming that the sort and size given by this entity is correct. If no SDL entity can be found that points to the data area, this is considered to be an error and a Explorer report is generated.

The purpose of the UserFree function is to inform the Explorer that a data area has been released, and thus should be removed from the list of dynamically allocated data areas.

There exists a special C macro XVALIDATOR_LIB that can be used to check in external C files if the code is compiled together with the Explorer kernel. It is thus possible to only include the calls to UserMalloc/UserFree when the C code is compiled together with the Explorer using this macro, as in the following example:

...
v = malloc( 10 );
#ifdef XVALIDATOR_LIB
UserMalloc( (void *)v );
#endif 

http://www.ibm.com/rational
Contents Index Previous Next