 |
 |
|
|
Some users have reported installation problems on Solaris and (mostly) Linux platforms. These problems are due to incompatibilities between the binaries included in the VeriSoft distribution package and some versions of the libc library (/lib/libc.so). Most frequent problems include:
Error 28 in msgget: No space left on device
this means that your machine has exhausted the memory it has for message queues. Please clean up your machine (with the Unix system calls ipcs and ipcrm -- see first item above) and/or increase the number of message queues allowed on your machine (this is not a VeriSoft problem).
VeriSoft_exp Error: can't get file and line! (timeout 1)
The last process might have terminated abnormally without executing 'exit'.
Diagnosis:
bt
#0 0xffffe405 in ?? ()
#1 0xffffd5b8 in ?? ()
#2 0x00468e5b in semop () from /lib/tls/libc.so.6
Previous frame inner to this frame (corrupt stack?)
This 'corrupt stack' problem appears with some versions of gdb 6.x (and is documented on the web). Fix: use the repair script below to bypass this gdb problem.
g++ -I/home/god/linux/verisoft/bin /home/god/linux/verisoft/bin/verisoft_Linux
_2.x.o -DVERIFY main.cc
In file included from main.cc:8:
/usr/include/stdio.h:300: declaration of `int VS_dont_printf(const char*, ...)
throw ()' throws different exceptions
/home/god/linux/verisoft/bin/verisoft-c++.h:29: than previous declaration `int
VS_dont_printf(const char*, ...)'
The problem is due to interferences between the instrumentation performed by including "verisoft.h" and "verisoft-c++.h" with versions of "stdio.h". Fix: simply include "stdio.h" before "verisoft.h" and "verisoft-c++.h" in the C++ source file (main.cc in the example above). (Thanks to Nils Klarlund for catching this one.)
Please contact us if you experience any other problem. We will do our best to help you (although our resources for supporting VeriSoft are limited).
This problem occurs on versions of Linux where the C library has been compiled with the '-g' option (I guess). To solve it, simply execute the following command as root:
strip /lib/libc-2.1.2.so
(Note: apply strip to whatever C library your C compiler is using -- this may be another version that 2.1.2!) This will get rid of the debugging info (erroneously?) associated to the C library on your machine (in this example, /lib/libc-2.1.2.so).
The distribution package available from this site includes a version of VeriSoft for Solaris and Linux.
Actually, VeriSoft can in principle be compiled to run on any Unix platform, but we discourage its use on other Unix platforms since we have very limited resources for supporting the free version. VeriSoft is not currently available for Windows NT. Please contact the authors (see [Contact us!]) for more information on this topic.
VeriSoft has been used mainly for two types of applications so far (inside Lucent Technologies):
Excellent and tough question. Precisely, the applicability of VeriSoft depends on the amount of nondeterminism in the system being analyzed. Nondeterminism comes from either parallelism or explicit nondeterminism introduced by the user (using the special "VS_toss" operation). Hence, the size of the program is not relevant to determine the scope of this approach. For instance, we have used VeriSoft for analyzing the behavior of (deterministic) software components described by 500,000 lines of C/C++ code without any problem.
In the case of tens of parallel processes, the amount of nondeterminism due to parallelism in the system is probably too large for VeriSoft to be very effective. There are then several alternatives. For instance, one can reduce the number of processes to a smaller, hopefully still realistic, number. Another option is to consider the parallel composition of all the processes as a single "black-box" process (that we assume to be deterministic), and to tell VeriSoft to ignore the inter-process communications and just focus on analyzing the interactions of the whole black-box process with its environment. Both of these suggestions reduce the amount of nondeterminism visible to VeriSoft. Of course, these suggestions may or may not be satisfactory, depending of the goal of the analysis and of the nature of the system being tested.
Given any specific problem, there is usually a way to reduce nondeterminism enough to make an analysis by VeriSoft tractable while still being able to reveal interesting bugs, that would be very hard to reveal using conventional testing techniques. However, this reduction may require a little (or a lot of) ingenuity... (Bold claim heard recently: "Give us any non-trivial concurrent/reactive/real-time software application, VeriSoft and a few weeks, and we guarantee we will find bugs in the application." ;-)
In summary, systematic state-space exploration is simple. Used naively, the chances of getting interesting feed-back from using it might be very small. Used properly, it can be extremely effective.
There are two main approaches for using VeriSoft:
The second approach is the most frequently used when applying VeriSoft to real communications software products.
VeriSoft only provides limited support to analyze Java applications. Specifically, a whole Java virtual machine can only be viewed as a single black-box by VeriSoft -- there is currently no way to monitor the executions and interactions of individual Java threads. Using VeriSoft for analyzing the correctness of a multi-threaded Java application by following the second approach discussed in the previous question can still be very effective (especially if the target platform is a Unix OS since the Java thread scheduler is then mostly deterministic; on Windows platforms, Java thread schedulers are more nondeterministic).
Here is a 'repair script' for the portability problems listed above. Please follow the instructions below carefully.
Copy the file v.tar in your 'verisoft/bin/' directory.
Then 'cd' to that directory and type: 'tar xvf v.tar'
Then type './install-here'
This script should fix these portability problems.