A fine-grained parallel completion procedure

ABSTRACT

We present a parallel Knuth-Bendix completion algorithm where the inner loop, deriving the consequences of adding a new rule to the system, is multi-threaded. The selection of the best new rule in the outer loop, and hence the completion strategy, is exactly the same as for the sequential algorithm. Our implementation, which is within the PARSAC-2 parallel symbolic computation system, exhibits good parallel speedups on a standard multi-processor workstation.

REFERENCES

• 1: Jürgen Avenhaus , Jörg Denzinger, Distributing Equational Theorem Proving, Proceedings of the 5th International Conference on Rewriting Techniques and Applications, p.62-76, June 16-18, 1993
• 2: L. Bachmair , Nachum Dershowitz, Critical pair criteria for completion, Journal of Symbolic Computation, v.6 n.1, p.1-18, August 1988 [doi>10.1016/S0747-7171(88)80018-X]
• 3: Buchberger, Collins, Encarnaci6n, Hong, Johnson, Krandick, Loos, Mandache, Neubacher, and Vielhaber. Saclib user's guide, 1993. On-line software documentation.
• 4: B. Buchberger and R. Loos. Algebraic simplification. In Computer Algebra, pages 14-43. Springer-Verlag, 1982.
• 5: Reinhard Bündgen, Completion of integral polynomials by AC-term completion, Proceedings of the 1991 international symposium on Symbolic and algebraic computation, p.70-78, July 15-17, 1991, Bonn, West Germany [doi>10.1145/120694.120704]
• 6: Reinhard Bündgen, Simulating Buchberger's algorithm by Knuth-Bendix completion, Proceedings of the 4th international conference on Rewriting techniques and applications, p.386-397, March 1991, Como, Italy
• 7: Reinhard Bündgen, Buchberger's Algorithm: The Term Rewriter's Point of View (Extended Abstract), Proceedings of the 19th International Colloquium on Automata, Languages and Programming, p.380-391, July 13-17, 1992
• 8: Reinhard Bündgen, Reduce the Redex -> ReDuX, Proceedings of the 5th International Conference on Rewriting Techniques and Applications, p.446-450, June 16-18, 1993
• 9: R. Bfindgen, M. G5bel, and W. Kiichlin. Experiments with multi-threaded Knuth-Bendix completion. Technical Report 94-05, Wilhelm-Schickard-Institut, Universit~t Tiibingen, D-72076 Tfibingen, 1994.
• 10: Soumen Chakrabarti , Katherine Yelick, Implementing an irregular application on a distributed memory multiprocessor, ACM SIGPLAN Notices, v.28 n.7, p.169-178, July 1993
• 11: J. Christian, Fast Knuth-Bendix completion, Proceedings of the 3rd international conference on Rewriting Techniques and Applications, p.551-555, January 1989
• 12: E. C. Cooper and R. P. Draves. C threads. Technical Report CMU-CS-88-154, Computer Science Department, Carnegie Mellon University, Pittsburgh, PA 15213, June 1988.
• 13: Nachum Dershowitz, Termination of rewriting, Journal of Symbolic Computation, v.3 n.1-2, p.69-116, Feb./April 1987 [doi>10.1016/S0747-7171(87)80022-6]
• 14: Nachum Dershowitz , Jean-Pierre Jouannaud, Rewrite systems, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 15: Nachum Dershowitz , Naomi Lindenstrauss, An Abstract Concurrent Machine for Rewriting, Proceedings of the Second International Conference on Algebraic and Logic Programming, p.318-331, October 01-03, 1990
• 16: J. W. Klop, Term rewriting systems, Handbook of logic in computer science (vol. 2): background: computational structures, Oxford University Press, Inc., New York, NY, 1993
• 17: D. E. Knuth and P. B. Bendix. Simple word problems in universal algebra. In J. Leech, editor, Computational Problems in Abstract Algebra. Pergamon Press, 1970. (Proc. of a conference held in Oxford, England, 1967).
• 18: W. Kiichlin. An implementation and investigation of the Knuth-Bendix completion algorithm. Master's thesis, Informatik I, Universit~t Karlsruhe, D-7500 Karlsruhe, W-Germany, 1982. (Reprinted as Report 17/82.).
• 19: Wolfgang Küchlin, Some reduction strategies for algebraic term rewriting, ACM SIGSAM Bulletin, v.16 n.4, p.13-23, November 1982 [doi>10.1145/1089310.1089315]
• 20: W. Kiichlin. A generalized Knuth-Bendix algorithm. Technical Report 86-01, Mathematics, Swiss Federal Institute of Technology (ETH), CH-8092 Zfirich, Switzerland, Jan. 1986.
• 21: Wolfgang Kuechlin, PARSAC-2: A Parallel SAC-2 Based on Threads, Proceedings of the 8th International Symposium on Applied Algebra, Algebraic Algorithms and Error-Correcting Codes, p.341-353, August 20-24, 1990
• 22: Wolfgang Küchlin, On the multi-threaded computation of integral polynomial greatest common divisors, Proceedings of the 1991 international symposium on Symbolic and algebraic computation, p.333-342, July 15-17, 1991, Bonn, West Germany [doi>10.1145/120694.120747]
• 23: Wolfgang Küchlin, The S-Threads Environment for Parallel Symbolic Computation, Proceedings of the Second International Workshop on Computer Algebra and Parallelism, p.1-18, May 09-11, 1990
• 24: W. W. Kfichlin and N. J. Nevin. On multi-threaded list-processing and garbage collection, in Proc. Third IEEE Syrup. on Parallel and Distributed Processing, pages 894-897, Dallas, TX, Dec. 1991. IEEE Press.
• 25: W. W. Kfichlin and J. A. Ward. Experiments with virtual C Threads. In Proc. Fourth IEEE Symp. on Parallel and Distributed Processing, pages 50-55, Dallas, TX, Dec. 1992. IEEE Press.
• 26: H. Melenk and W. Neun. Parallel polynomial operations in the large Buchberger algorithm. In J. Della Dora and J. Fitch, editors, Computer Algebra and Parallelism, Computational Mathematics and Applications, pages 143-158, London, 1989. Academic Press. (Proc. CAP'88, Grenoble, France, June 1988).
• 27: David A. Plaisted, Equational reasoning and term rewriting systems, Handbook of logic in artificial intelligence and logic programming (vol. 1), Oxford University Press, Inc., New York, NY, 1993
• 28: R. Ramesh , I. V. Ramakrishnan, Optimal speedups for parallel pattern matching in trees, on Rewriting techniques and applications, p.274-285, May 1987, Bordeaux, France
• 29: Wolfgang Schreiner , Hoon Hong, The Design of the PACLIB Kernel for Parallel Algebraic Computation, Proceedings of the Second International ACPC Conference on Parallel Computation, p.204-218, October 04-06, 1993
• 30: Stephen A. Schwab, Extended parallelism in the Gro¨bner basis algorithm, International Journal of Parallel Programming, v.21 n.1, p.39-66, Feb. 1992 [doi>10.1007/BF01379314]
• 31: John K. Slaney , Ewing L. Lusk, Parallelizing the closure computation in automated deduction, Proceedings of the tenth international conference on Automated deduction, p.28-39, July 1990, Kaiserslautern, Germany
• 32: M. Sperber. Merk: A generator for preprocessors. Master's thesis, Universit/it Tiibingen, 1994.
• 33: Mark E. Stickel, A note on leftmost innermost term reduction, ACM SIGSAM Bulletin, v.17 n.3-4, p.19-20, August-November 1983 [doi>10.1145/1089338.1089340]
• 34: Andrew S. Tanenbaum, Modern operating systems, Prentice-Hall, Inc., Upper Saddle River, NJ, 1992
• 35: Jean-Philippe Vidal, The computation of Gröbner bases on a shared memory multiprocessor, Proceedings of the International Symposium on Design and Implementation of Symbolic Computation Systems, p.81-90, April 10-12, 1990
• 36: M. Weiser , A. Demers , C. Hauser, The portable common runtime approach to interoperability, Proceedings of the twelfth ACM symposium on Operating systems principles, p.114-122, November 1989
• 37: Katherine A. Yelick , Stephen J. Garland, A Parallel Completion Procedure for Term Rewriting Systems, Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, p.109-123, June 15-18, 1992

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.2 Algorithms
          Subjects: Algebraic algorithms

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation
          Subjects: Parallelism and concurrency
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.2 Grammars and Other Rewriting Systems
          Subjects: Parallel rewriting systems (e.g., developmental systems, L-systems)

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION

General Terms:
Algorithms