Abstract
We present a parallel completion procedure for term rewriting systems. Despite an extensive literature concerning the well-known sequential Knuth-Bendix completion procedure, little attention has been devoted to designing parallel completion procedures. Because naive parallelizations of sequential procedures lead to over-synchronization and poor performance, we employ a transition-based approach that enables more effective parallelizations. The approach begins with a formulation of the completion procedure as a set of transitions (in the style of Bachmair, Dershowitz, and Hsiang) and proceeds to a highly tuned parallel implementation that runs on a shared memory multiprocessor. The implementation performs well on a number of standard examples.
Both authors were supported in part by the Advanced Research Projects Agency of the Department of Defense, monitored by the Office of Naval Research under contract N00014-89-J-1988, by the National Science Foundation under grant CCR-8910848, and by the Digital Equipment Corporation. K. Yelick was supported in part by AT&T and by the University of California at Berkeley. S. Garland was supported in part by a Fulbright Lectureship.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
M. Abadi and L. Lamport. The existence of refinement mappings. Research Report 29, Digital Equipment Corporation Systems Research Center, Palo Alto, CA, 1988.
L. Bachmair, N. Dershowitz, and J. Hsiang. Orderings for equational proofs. In Proceedings of the Symposium on Logic in Computer Science, pages 346–357. IEEE, 1986.
B. Buchberger. History and basic features of the critical pair/completion procedure. Journal of Symbolic Computation, 3(1&2):3–38, February/April 1987.
N. Dershowitz. Orderings for term-rewriting systems. Theoretical Computer Science, 17:279–301, 1982.
N. Dershowitz. Completion and its applications. In H. Ait-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, volume II: Rewriting Techniques, pages 31–86. Academic Press, New York, 1989.
N. Dershowitz, 1990. Private communication.
N. Dershowitz and N. Lindenstrauss. An abstract machine for concurrent term rewriting. In Proceedings of the Second International Conference on Algebraic and Logic Programming, Berlin. LNCS, October 1990.
D. Detlefs and R. Forgaard. A procedure for automatically proving termination of a set of rewrite rules. In Proceedings of the First International Conference on Rewriting Techniques and Applications, Dijon, France, pages 255–270. LNCS 202, May 1985.
C. Dwork, P. C. Kanellakis, and J. C. Mitchell. On the sequential nature of unification. Journal of Logic Programming, 1:35–50, June 1984.
C. Dwork, P. C. Kanellakis, and L. Stockmeyer. Parallel algorithms for term matching. SIAM Journal of Computing, 17(4):711–731, August 1988.
S. J. Garland and J. V. Guttag. A guide to LP, the Larch Prover. Technical Report 82, Digital Equipment Corporation Systems Research Center, Palo Alto, CA, 1991.
S. J. Garland, J. V. Guttag, and J. L. Horning. Debugging Larch Shared Language specifications. Technical Report 60, Digital Equipment Corporation Systems Research Center, Palo Alto, CA, 1990.
D. E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon, Oxford, 1970.
P. Lescanne. Completion procedures as transition rules + control. In TAPSOFT '89, pages 28–41. LNCS 351, 1989.
P. Lescanne. Orme, an implementation of completion procedures as sets of transition rules. In M. Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction, pages 661–662. LNCS 449, 1990.
U. Martin. Doing algebra with REVE. Technical report, University of Manchester, Manchester, England, 1986.
G. E. Peterson and M. E. Stickel. Complete sets of reductions for some equational theories. J. ACM, 28(2):233–264, Apr. 1981.
C. Ponder. Evaluation of performance enhancements in algebraic manipulation systems. Technical Report UCB/CSD-88/438, Computer Science Division, University of California, Berkeley, CA 94720, 1988.
R. Ramesh and I. Ramakrishnan. Optimal speedups for parallel pattern matching in trees. In Proceedings of the 2nd International Conference on Rewriting Techniques and Applications, Bordeaux, France, pages 274–285. LNCS 256, May 1987.
J. K. Slaney and E. W. Lusk. Parallelizing the closure computation in automated deduction. In Proceedings of the 10th International Conference on Automated Deduction, pages 28–29. LNCS 449, 1990.
R. M. Verma and I. Ramakrishnan. Tight complexity bounds for term matching problems. Information and Computation, 1990.
J.-P. Vidal. The computation of Gröbner bases on shared memory multiprocessors. Technical Report CMU-CS-90-163, School of Computer Science, Carnegie Mellon University, Pittsburg, PA, 1990.
K. A. Yelick. Using Abstraction in Explicitly Parallel Programs. PhD thesis, MIT Laboratory for Computer Science, Cambridge, MA 02139, December 1990. Also appeared as MIT/LCS/TR-507, July 1991.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yelick, K.A., Garland, S.J. (1992). A parallel completion procedure for term rewriting systems. In: Kapur, D. (eds) Automated Deduction—CADE-11. CADE 1992. Lecture Notes in Computer Science, vol 607. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55602-8_159
Download citation
DOI: https://doi.org/10.1007/3-540-55602-8_159
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55602-2
Online ISBN: 978-3-540-47252-0
eBook Packages: Springer Book Archive