Benchmarking C Software Verifiers With LDV Tools » History » Revision 14
Revision 13 (Pavel Shved, 11/25/2010 08:45 PM) → Revision 14/19 (Pavel Shved, 11/26/2010 05:31 PM)
h1. Benchmarking C Software Verifiers With LDV Tools 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. 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. So one of the goals of LDV program is to build a framework that helps us in answering such questions, as: * Which configuration of a verifier works faster on a test driver set? * Which verifier checks more drivers within a given time limit? * How would it affect verification, if we supply verifier with more memory? 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. h2. Visualization and comparison Here''s a sample experiment. We used a test set with some interesting "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/. "CPAchecker":http://cpachecker.sosy-lab.org/ with different time limits. Here are the results: results !http://forge.ispras.ru/attachments/524/bench1.png! !http://forge.ispras.ru/attachments/518/bench1.png! From this table we could see that LBE is generally faster than SBE. (actually, this table doesn''t show us anything interesting. LBE verified more drivers (@Ok@ columnt), I''ll re-run tests with different configurations and nevertheless it spent less time re-create the table to do it (see @Time OK@ to do this). LBE version also ran out of memory more. demonstrate that results can be useful). Now let''s see the how many degradations or improvements of LBE over CBE in detail. were there. We click First, select some test runs to compare (hitting radio button near the "basis", and checking some to set the task we compare against (we pick the "worse" one), and check box near the task we want to compare, and it): !http://forge.ispras.ru/attachments/519/bench2.png! And press the "Compare tasks" button at to get to the top of the page. comparison page: !http://forge.ispras.ru/attachments/525/bench1a.png! !http://forge.ispras.ru/attachments/520/bench3.png! We get to a comparison page, which shows how LBE improved over SBE. We Here we can see that our "basis" configuration dominates all others. Indeed, some of the drivers that were Unknown to SBE checking, are detected as Safe or Unsafe in LBE, so LBE is an improvement. However, we notice, that there were degradations: a driver with an error in it is the "basis" configuration are not detected by SBE, but not be LBE (see the red circle): !http://forge.ispras.ru/attachments/526/bench2.png! We click the number to see what the driver was that: !http://forge.ispras.ru/attachments/529/bench3.png! Then we click the "left-hand" (LBE) ellipsis to see what the problem there is: !http://forge.ispras.ru/attachments/528/bench4.png! So it seems that LBE verification of that particular driver exceedes the memory limit for CPAchecker. We searched in the logs for a "message.ko", that had numbers "68_1" anymore, and 2.6.31.6 near it (see file @test_logs@ in your working dir), and found the command line are "Unknown" for CPAchecker verifying this driver. other configurations we selected. 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. h2. How to use LDV for benchmarking 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 smoothly change command line options, configuration files, vary time and memory limits. Currently, only BLAST and CPAchecker verifiers are supported. However, developing a convenient way to plug in other verifiers is on our roadmap.