A Parallel Completion Procedure for Term Rewriting Systems

      Katherine A. Yelick and Stephen J. Garland

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.