Benchmarking C Software Verifiers With LDV Tools » History » Revision 3
Revision 2 (Pavel Shved, 11/24/2010 07:43 PM) → Revision 3/19 (Pavel Shved, 11/24/2010 08:08 PM)
h1. Benchmarking C Software Verifiers With LDV Tools The core component of Linux Driver Verification tools is verification tool for C language. Static analysis of driver sources with instrumented environment models and rules are eventually passed to such a 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 find! 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 should also be explored. So one of the goals of LDV program is to build a framework that aids 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. h2. Visualization and comparison Here''s a sample experiment. We used assembled a test set with some "interesting" drivers (fixed and unfixed versions of those, in which we used to find bugs), which is included this test set being in default the standard shipment of LDV tools (it''s called @generic@) to @generic@), and run "CPAchecker":http://cpachecker.sosy-lab.org/ with different time limits. Here are the results !http://forge.ispras.ru/attachments/518/bench1.png! From this table we could see that (actually, this table doesn''t show us anything interesting. I''ll re-run tests with different configurations and re-create the table to demonstrate that results can be useful). Now let''s see how many degradations or improvements were there. First, select some test runs to compare (hitting radio button near the "basis"): And press the "Compare tasks" button to get to the comparison page: Here we can see that our "basis" configuration dominates all others. Indeed, some of the drivers that were detected as Safe or Unsafe in the "basis" configuration are not detected anymore, and are "Unknown" for other configurations we selected. h2. How to use LDV for benchmarking