Next: General Index, Previous: Troubleshooting, Up: Top [Contents][Index]
The Daikon invariant detector is named after an Asian radish. “Daikon” is pronounced like the combination of the two one-syllable English words “die-con”.
More information on Daikon can be found in the Daikon Developer Manual (see Introduction in Daikon Developer Manual). For instance, the Daikon Developer Manual indicates how to extend Daikon with new invariants, new derived variables, and front ends for new languages. It also contains information about the implementation and about debugging flags.
| • History | ||
| • License | ||
| • Mailing lists | ||
| • Credits | ||
| • Citing Daikon |
This manual describes Daikon version 5.8.18, released June 23, 2023. A more detailed list of revisions since mid-2001 can be found in file doc/CHANGELOG.md in the distribution; this section gives a high-level view of the package’s history.
There have been four major releases of Daikon, with different features and capabilities. User experiences and technical papers should be judged based on the version of Daikon current at the time of use.
Daikon 1 was written in the Python programming language in 1998. It included front ends for C, Java, and Lisp. The C front end was extremely limited and failed to operate correctly on all C programs: sometimes it suffered a segmentation fault while instrumenting a target program, and even when that did not happen, sometimes the instrumented program segmentation-faulted while running. The Lisp front end operated correctly on all Lisp programs, but only instrumented certain common constructs, leaving other language features uninstrumented. The Java front end was reasonably reliable. The Lisp front end instrumented procedure entries, exits, and loop heads; the C front ends instrumented only procedure entries and exits; and the Java front end instrumented program points for object invariants as well as procedure entries and exits. Daikon 1 and its Lisp front end were only removed from Daikon version control repository in November 2010, though they had long been obsolete.
Daikon 2 was a complete rewrite in the Java programming language and was the first version to contain a substantive manual. Daikon 2 uses the same source-based Java front end as did Daikon 1, though with certain enhancements. Its C front end was rewritten from scratch; it instruments only procedure entries and exits. A front end also exists for the Input Output Automaton programming language, but is not included in the Daikon distribution.
Daikon 3 is a redesign of the invariant detection engine to work incrementally — that is, to examine each sample (execution of a program point) once, then discard it. By contrast, Daikon 1 and Daikon 2 made multiple passes over the data. This simplified their algorithms but required storing all the data in memory at once, which was prohibitive, particularly since data trace files may be gigabytes in size. Daikon 3 also introduces the idea of a dataflow hierarchy, a way to relate and connect program points based on their variables.
Daikon 4 includes new binary front ends for Java and for C. These front ends make Daikon much easier to use. Daikon 4 makes .decls files optional; program point declarations are permitted to appear in .dtrace files. Daikon 4 is released under more liberal licensing conditions that place no restrictions on use.
Daikon 5 adds a new front end (Celeriac) for .NET languages (C#, F#, and Visual Basic). The underlying Valgrind was updated and much work done to ensure Daikon works properly on the latest versions of Linux. The Chicory front end for Java was modified to support Java 7. Daikon releases were moved from MIT to the University of Washington. The bug tracker was moved to Google Code, and mailing lists moved to Google Groups.
Next: Mailing lists, Previous: History, Up: Details [Contents][Index]
Copyright © 1998-2022
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the “Software”), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
The names and trademarks of copyright holders may not be used in advertising or publicity pertaining to the software without specific prior permission. Title to copyright in this software and any associated documentation will at all times remain with the copyright holders.
THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NON INFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
| • Library licenses | ||
| • Front end licenses |
Next: Front end licenses, Up: License [Contents][Index]
| • getopt license | ||
| • JUnit license |
Next: JUnit license, Up: Library licenses [Contents][Index]
Daikon uses the Java port of the GNU getopt library, which is copyright 1998 Aaron M. Renn. The getopt library is free software, and may be redistributed or modified under the terms of the GNU Library General Public License version 2. A copy of this license is included with the Daikon distribution as the file doc/gnu-gpl-2.txt.
Previous: getopt license, Up: Library licenses [Contents][Index]
Daikon’s unit tests use the JUnit testing framework, which is governed
by the Common Public License, version 1.0. JUnit is provided on an
“as is” basis, without warranties or conditions of any kind, either
express or implied including, without limitation, any warranties or
conditions of title, non-infringement, merchantability or fitness for
a particular purpose. Neither the Daikon developers nor the authors of
the JUnit framework shall have any liability for any direct, indirect,
incidental, special, exemplary, or consequential damages (including
without limitation lost profits), however caused and on any theory of
liability, whether in contract, strict liability, or tort (including
negligence or otherwise) arising in any way out of the use or
distribution of JUnit or the exercise of any rights granted in
the Common Public License, even if advised of the possibility of such
damages. Those portions of JUnit that appear in the Daikon
distribution may be redistributed under the same terms as Daikon
itself; this offer is made by the Daikon developers exclusively and
not by any other party. The Common Public License is included with the
Daikon distribution as the file java/junit/cpl-v10.html.
Previous: Library licenses, Up: License [Contents][Index]
Note that the front ends discussed in this manual are separate programs, and some are made available under different licenses. Because the front ends are separate programs not derived from the Daikon invariant detection tool, you are neither required nor entitled to use the Daikon invariant detector itself under these other licenses.
| • dfepl license | ||
| • Kvasir license | ||
| • Celeriac license |
Next: Kvasir license, Up: Front end licenses [Contents][Index]
The Daikon Perl front end dfepl may be used and distributed under the
regular Daikon license or, at your option, either the GNU General
Public License or the Perl Artistic License (that is, under the same
terms as Perl itself).
Next: Celeriac license, Previous: dfepl license, Up: Front end licenses [Contents][Index]
The Daikon C/C++ front end Kvasir is based in part on the Valgrind
dynamic program supervision framework, copyright 2000-2004
Julian Seward, the Sparrow Valgrind tool, copyright 2002
Nicholas Nethercote, the MemCheck Valgrind tool,
copyright 2000-2004 Julian Seward, the
readelf program of the GNU Binutils, copyright 1998-2003 the Free
Software Foundation, Inc., the GNU C Library, copyright 1995, 1996,
1997, 2000 the Free Software Foundation, Inc., and the Diet libc,
copyright Felix von Leitner et al. Kvasir is free software; you can
redistribute it and/or modify it under the terms of the GNU General
Public License as published by the Free Software Foundation; either
version 2 of the License, or (at your option) any later version.
Kvasir is distributed in the hope that it will be useful, but WITHOUT
ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
for more details. You should have received a copy of the GNU General
Public License along with Kvasir, in the file kvasir/COPYING;
if not, write to the
Free Software Foundation, Inc., 51 Franklin St., Fifth Floor, Boston, MA
02110-1301, USA.
Previous: Kvasir license, Up: Front end licenses [Contents][Index]
The Daikon .NET front end Celeriac is Copyright (c) 2012 by Kellen Donohue. Portions of Celeriac are covered by the Microsoft Public License, this is at the top of every such file. Otherwise the following license is in effect:
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NON-INFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
The following mailing lists (and their archives) are available:
A low-volume, announcement-only list. For example, announcements of new releases are sent to this list. To subscribe, visit https://groups.google.com/forum/#!forum/daikon-announce.
A moderated list for the community of Daikon users. Use it to share tips and successes, and to get help with questions or problems (after checking the documentation). To subscribe, visit https://groups.google.com/forum/#!forum/daikon-discuss.
This list goes to the Daikon maintainers. Use it for questions about the Daikon and Kvasir source code. Use the issue tracker (https://github.com/codespecs/daikon/issues) for bug reports and feature requests. If you are an active contributor to Daikon, you may send mail to the list asking to be added to the list.
Do not send the same message to multiple mailing lists. Doing so is antisocial: it causes confusion and extra work. If you do so, your question will not be answered.
Next: Citing Daikon, Previous: Mailing lists, Up: Details [Contents][Index]
The following individuals have contributed to Daikon: Alan Donovan, Alan Dunn, Alexandru Salcianu, Allen Liu, Antonio Garcia-Dominguez, Benjamin Morse, Brian Demsky, Carlos Pacheco, Cemal Akcaba, Charles Tam, Charlie Garrett, Chen Xiao, Danny Dig, Darko Marinov, David Cok, David McArthur, David Notkin, Derek Rayside, Dieter von Holten, Emily Marcus, Eric Fellheimer, Eric Spishak, Florian Gross, Florian S. Gross, Forrest Coward, Galen Pickard, Greg Jay, Greg Sullivan, Gustavo Santos, Iuliu Vasilescu, Jaime Quinonez, Jake Cockrell, James Anderson, Javier Thaine, Jeff Perkins, Jeff Yuan, Jelani Nelson, Jeremy Nimmer, Jonathan Burke, Josh Kataoka, Kathryn Shih, Kellen Donohue, Konstantin Weitz, Laure Thompson, Lee Lin, Mark Roberts, Massimiliano Menarini, Matthew Tschantz, Melissa Hao, Michael Ernst, Michael Harder, Nii Dodoo, Philip Guo, Robert Rudd, Ryan Newton, Samir Meghani, Sandra Loosemore, Stephen Garland, Stephen McCamant, Sung Kim, Suzanne Millstein, Tao Xie, Tatyana Nikolova, Todd Schiller, Toh Ne Win, Vikash Mansinghka, Vincent Hellendoorn, Weitian Xing, Werner Dietl, William Griswold, Yoav Zibin, Yuriy Brun.
Craig Kaplan carved the Daikon logo.
The feedback of Daikon users has been very valuable. We are particularly grateful to B. Thomas Adler, Rich Angros, Tadashi Araragi, Seung Mo Cho, Christoph Csallner, Dorothy Curtis, Juan Pablo Galeotti, Diego Garbervetsky, Mangala Gowri, Madeline Hardojo, Engelbert Hubbers, Nadya Kuzmina, Scott McMaster, Charles O’Donnell, Alex Orso, Rodric Rabbah, Manos Renieris, Rosie Wacha.
Many others have also been generous with their feedback, for which we are also grateful.
If your name has been inadvertently omitted from this section, please let us know so we can correct the oversight.
Financial support has been provided by: National Science Foundation (NSF), Defense Advanced Research Projects Agency (DARPA), ABB, Edison Design Group, IBM, NTT, MIT Oxygen Project, Raytheon, Toshiba.
If you wish to cite Daikon in a publication, we recommend that you reference one of the scholarly papers listed at http://plse.cs.washington.edu/daikon/pubs/#invariant-detection in lieu of, or in addition to, referencing this manual and the Daikon website (http://plse.cs.washington.edu/daikon/).