Abstract
Tools for systems analysis often combine different memoryintensive data structures, such as BDDs, tuple sets, and symbolic expressions. When separate packages are used to manipulate these structures, their conflicting resource needs can reduce overall performance despite the individual efficiency of each. Factotum is a software system for implementing symbolic computing systems on DAG-based structures that critically rely on sharing of equivalent subterms. It provides an subterm sharing facility that is automatic and systematic, analogously to the way that automatic memory management is provided by a garbage collector. It also provides a high-level programming interface suitable for use in multithreaded applications. We describe both the theoretical underpinnings and practical aspects of Factotum, show some examples, and report on some recent experiments.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
André Arnold, Didier Bégay, and Paul Crubillé. Construction and Analysis of Transition Systems with MEG. Number 3 in AMAST Series in Computing. World Scientific Publishers, 1994.
B. Akers. Binary decision diagrams. IEEE Transactions on Computers, 27(6):509–516, 1978.
Andrew Appel. Garbage collection can be faster than stack allocation. Information Processing Letters, 25(4), 1987.
R. Bryant. Graph based algorithms for boolean fonction manipulation. IEEE Transactions on Computers, 35(8):677–691, 1986.
The CGC copying garbage collector. At ftp://ftp.labri.u-bordeaux.fr/, September 1997. Part of the eqc equational programming project.
Leslie Paul Chew. An improved algorithm for computing with equations. In 21st Annual Symposium on Foundations of Computer Science, 1980.
Christoph Hoffmann and Michael J. O'Donnell. Pattern matching in trees. Journal of the ACM, pages 68–95, 1982.
John Hughes. Lazy memo functions. In Functional Programming Languages and Computer Architectures. Springer-Verlag, 1985.
Per-Ake Larson. Dynamic hash tables. Communications of the ACM, 31(4):446–457, April 1988.
Nicolas Magnier. Recalculs dans les systèmes de réécriture et programmation équationnelle. Technical Report 974-94, Laboratoire Bordelais de Recherche en Informatique, 1994.
J. McCarthy. Recursive functions of symbolic expressions and their computation by machine. Communications of the ACM, 3(4):185–195, 1960.
D. Mitchie. ‘Memo’ functions and machine learning. Nature, pages 19–22, 1968.
Renaud Paquay. Implementation du logiciel de vérification de modèle MEC avec les arbrés partagés. Master's Thesis, University Notre-Dame de la Paix, Namur, Belgium, 1996.
A. Rauzy. An introduction to binary decision diagrams and some of their applications to risk assessment. In O. Roux, editor, Actes de l'école d'été, Modélisation et Vérification de Processus Parallèles, MOVEP'96, 1996. Also Technical Report 1121-96, Laboratoire Bordelais de Recherche en Informatique.
Antoine Rauzy and Marc-Michel Corsini. First experiments with Toupie. Technical Report 581-93, Laboratoire Bordelais de Recherche en Informatique, 1993.
I. V. Ramakrishnan and R. Verma. Nonoblivious normalization algorithms for nonlinear systems. In Proceedings of the International Conference on Automata, Languages, and Programming, 1990.
David J. Sherman. Lazy directed congruence closure. Technical Report 90-028, University of Chicago Department of Computer Science, 1990.
David J. Sherman. Run-time and Compile-time Improvements to Equational Programs. PhD thesis, University of Chicago, Chicago, Illinois, 1994.
David J. Sherman. Factotum: Automatic and systematic sharing support for symbolic computation. Technical Report 1174-97, Laboratoire Bordelais de Recherche en Informatique, September 1997.
David J. Sherman. On referential transparency in the presence of uniform sharing. Technical Report 1179-97, Laboratoire Bordelais de Recherche en Informatique, October 1997.
Robert Strandh. A dynamic hash library. Available at ftp://ftp.labri.u-bordeaux.fr/, March 1992. Based on Larson, CACM 31(4).
Rakesh M. Verma. A theory of using history for equational systems with applications. Journal of the ACM, 42(5):984–1020, 1995.
Paul R. Wilson. Garbage collection. ACM Computing Surveys, 1995. Available at file://ftp.cs.utexas.edu/pub/garbage/bigsurv.ps.
Paul R. Wilson, Mark S. Johnstone, Michael Neely, and David Boles. Dynamic storage allocation: A survey and critical review. Technical report, University of Texas, 1995. Available at file://ftp.cs.utexas.edu/pub/garbage/allocsurv.ps.
D. Zampunieris and B. Le Charlier. Efficient handling of large sets of tuples with sharing trees. In Proceedings of Data Compression Conference, DCC'95, October 1995. Also Research Paper RP-94-004, Facultés Universitaires Notre-Dame de la Paix, Namur, Belgium.
Didier Zampuniéris and Baudouin Le Charlier. An efficient algorithm to compute the synchronized product. In Int'l Workshop MASCOTS, 1995.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sherman, D.J., Magnier, N. (1998). Factotum: Automatic and systematic sharing support for systems analyzers. In: Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1998. Lecture Notes in Computer Science, vol 1384. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054176
Download citation
DOI: https://doi.org/10.1007/BFb0054176
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64356-2
Online ISBN: 978-3-540-69753-4
eBook Packages: Springer Book Archive