Comparing DySy with Daikon

DySy is a dynamic symbolic tool for invariant detection. The field of dynamic invariant detection was pioneered by Daikon, by Michael Ernst et al. ("The Daikon dynamic invariant detector"). The following describes our initial attempts of comparing DySy with Daikon. So far, our comparison ignores several interesting questions you may be asking, e.g., regarding scalability.

Daikon

Here we are using Daikon 4.3.5 (which is the most current version as of May 2008). Our Ant script daikon.xml automates the steps of our experiment:
  • Compile the Java source files of the testee and the test case that will exercise the testee.
  • Run the test case and monitor its execution with Daikon's Chicory component, which generates an execution trace.
  • Let Daikon run over the execution trace to infer invariants.
  • Annotate the testee with the inferred invariants with Daikon's Annotate feature.
  • Collect our metrics (which builds on Daikon's feature for printing invariants).
  • Package the test case, annotated testee, and log files into a zip file.

daikon-metrics-16.zip contains the Java sources of our metrics collector (which depends on Daikon 4.3.5), our daikon.xml Ant script, and Daikon's StackAr example. After unpacking, and assuming your Daikon jar is at
\lib\daikon-4.3.5.jar, all you hopefully need to do is:
ant -f daikon.xml

This should automatically generate several files. The file ending in metrics.txt contains our counting of the unique sub-expressions of the invariants and pre- and post-conditions inferred by Daikon.

Basic configuration

We have played around with a few of the basic Daikon parameters. The experiments reported in ICSE 2008 use our default setting, which is also encoded into our daikon.xml file above. Following are the main options, but consult daikon.xml for all the details:
  • Chicory
    • --std-visibility
  • Daikon
    • --omit_from_output 0r

Following are some basic experiments we did with the basic options, but they are by no means exhaustive. For the small StackAr example that comes with Daikon, our different settings did not significantly affect the invariants produced by Daikon. Note that, to use the --suppress_redundant option, you will need to obtain the Simplify automated theorem prover separately. Our default configuration is in bold.

Chicory params Daikon params StackAr unique sub-exprs Download
316 zip
--std-visibility 316 zip
--omit_from_output 0r 316 zip
--std-visibility --omit_from_output 0r 316 zip
--std-visibility --suppress_redundant 316 zip
--std-visibility --omit_from_output 0r --suppress_redundant 316 zip

Daikon and DynComp

The ICSE 2008 paper uses Daikon without Daikon's optional DynComp preprocessing step, which has been described in ISSTA 2006. We have only very preliminary experience with DynComp, using daikon-metrics-17.zip:
  • DynComp
    • --std-visibility
    • --no-jdk
  • Chicory
    • --std-visibility
  • Daikon
    • --omit_from_output 0r

With the configuration, Daikon produces more invariants, and our count of unique sub-expressions increases from 316 to 363 (zip). But note that we have not yet tried to instrument our JDK to improve DynComp precision as described in the Daikon manual.

Last edited Nov 20, 2008 at 10:44 PM by csallner, version 24

Comments

No comments yet.