Comparing DySy with Daikon

DySy is a tool for dynamic 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.

DySy

For now, see our ICSE 2008 paper

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.

Cannot resolve file macro, invalid file name or id. 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 Cannot resolve file macro, invalid file name or id.
--std-visibility 316 Cannot resolve file macro, invalid file name or id.
--omit_from_output 0r 316 Cannot resolve file macro, invalid file name or id.
--std-visibility --omit_from_output 0r 316 Cannot resolve file macro, invalid file name or id.
--std-visibility --suppress_redundant 316 Cannot resolve file macro, invalid file name or id.
--std-visibility --omit_from_output 0r --suppress_redundant 316 Cannot resolve file macro, invalid file name or id.

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 Cannot resolve file macro, invalid file name or id.:
  • 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 (Cannot resolve file macro, invalid file name or id.). But note that we have not yet tried to instrument our JDK to improve DynComp precision as described in the Daikon manual.

Last edited Oct 23, 2008 at 5:44 PM by csallner, version 1

Comments

No comments yet.