Project

General

Profile

Benchmarking C Software Verifiers With LDV Tools » History » Version 15

Alexey Khoroshilov, 11/26/2010 07:15 PM

1 1 Pavel Shved
h1. Benchmarking C Software Verifiers With LDV Tools
2
3 10 Alexey Khoroshilov
The core component of Linux Driver Verification tools is a verification tool for C language.  Static analysis of driver sources, instrumented with environment models and rules, are eventually passed to such verifier, which performs the most important part of the whole work.
4 1 Pavel Shved
5 13 Pavel Shved
No wonder that the speed and quality of the overall analysis heavily depends on how well and fast the verifier performs.  But the best verifier is yet to be found!  There are several static C verifiers, which perform differently, and without experimenting it''s not clear which one is the best for our purpose.  Moreover, verifiers usually contain a number of tweaks and configuration opportunities, which also are to explore.  
6 1 Pavel Shved
7 10 Alexey Khoroshilov
So one of the goals of LDV program is to build a framework that helps us in answering such questions, as:
8 1 Pavel Shved
9
* Which configuration of a verifier works faster on a test driver set?
10
* Which verifier checks more drivers within a given time limit?
11
* How would it affect verification, if we supply verifier with more memory?
12
 
13 7 Pavel Shved
We developed special components that gather, analyze, visualize and compare statistics of verification of a lot of different drivers.  The drivers can either be automatically fetched from a pre-assembled test set, or could be automatically extracted from the Linux Kernel.
14 2 Pavel Shved
15
h2. Visualization and comparison
16
17 14 Pavel Shved
Here''s a sample experiment.  We used a test set with some interesting drivers (fixed and unfixed versions of those, in which we used to find bugs), which is included in default shipment of LDV tools (it''s called @general@) to run compare SBE and LBE in "CPAchecker":http://cpachecker.sosy-lab.org/.  Here are the results:
18 3 Pavel Shved
19 14 Pavel Shved
!http://forge.ispras.ru/attachments/524/bench1.png!
20 3 Pavel Shved
21 15 Alexey Khoroshilov
From this table we could see that LBE is generally faster than SBE.  LBE verified more drivers (@Ok@ columnt), and nevertheless it spent less time to do it (see @Time OK@ column).  Also you can see that SBE version ran out of memory more often.
22 3 Pavel Shved
23 15 Alexey Khoroshilov
Now let''s see the improvements of LBE over SBE in detail.  We click radio button to set the task we compare against (we pick the "worse" one), and check box near the task we want to compare, and press the "Compare tasks" button at the top of the page.
24 3 Pavel Shved
25 14 Pavel Shved
!http://forge.ispras.ru/attachments/525/bench1a.png!
26 1 Pavel Shved
27 15 Alexey Khoroshilov
We get to a comparison page.  We see that some drivers that were Unknown to SBE, are detected as Safe or Unsafe in LBE, so LBE surpasses SBE.  However, we notice, that there were degradations: a driver with an error in it is detected by SBE, but is not by LBE (see the red circle):
28 1 Pavel Shved
29 14 Pavel Shved
!http://forge.ispras.ru/attachments/526/bench2.png!
30 1 Pavel Shved
31 14 Pavel Shved
We click the number to see what the driver was that:
32 1 Pavel Shved
33 14 Pavel Shved
!http://forge.ispras.ru/attachments/529/bench3.png!
34
35
Then we click the "left-hand" (LBE) ellipsis to see what the problem there is:
36
37
!http://forge.ispras.ru/attachments/528/bench4.png!
38
39 15 Alexey Khoroshilov
So it seems that LBE verification of that particular driver exceeds the memory limit for CPAchecker.  We searched  in the logs for a "message.ko", that had numbers "68_1" and 2.6.31.6 near it (see file @test_logs@ in your working dir), and found the command line for CPAchecker verifying this driver.
40 14 Pavel Shved
41
We could also click the ellipsis at the other side and then proceed to error trace, which would show us where SBE CPAchecker found the bug.  This would help in debugging.
42
43
44
45
46 2 Pavel Shved
h2. How to use LDV for benchmarking
47 5 Pavel Shved
48 15 Alexey Khoroshilov
To use this benchmarking system you should first "download sources":/projects/ldv/wiki/Downloading_and_Building_LDV of LDV tools (we recommend downloading the master branch).  After downloading we recommend you to refer to file @VerifierDevelopersHowTo@ (see source:VerifierDevelopersHowTo).  It will tell you how you should install and use LDV tools in order to specifically address benchmarking verification tools.  You will be able to easily change command line options, configuration files, vary time and memory limits.
49 5 Pavel Shved
50
Currently, only BLAST and CPAchecker verifiers are supported.  However, developing a convenient way to plug in other verifiers is on our roadmap.