\subsection{Multi-core}\label{subsec:multi}

For decades now,
the computing power of CPUs increased steadily.
Laws of nature seem to limit the speed of instruction execution
on an electronic device,
but the computing power is still increasing because
of CPUs containing increasing numbers of computing units (cores) 
that operate in parallel.
It is  a challenge for software 
to match the increased hardware capabilities.

The Termination Competition community realized that
and encourages participating provers to employ parallelism.
The execution service for the competition runs on a 16 core machine,
and the prover can use 1 minute ``wall clock'' time per problem.
In other words, using only one of the cores
(as a classical single threaded program would do)
is wasting 15/16 of the available resources.

Several termination provers indeed employed parallelism,
among them {\sf AProVE} and {\sf Matchbox}.
The basic idea is that branches of the proof search tree
are explored in parallel. E.g., {\sf Matchbox} is looking
for standard and arctic matrix interpretations
for the original and the reversed string rewriting system,
all at the same time.
The execution of each node in the search tree involves
the production of a constraint system,
its treatment by an external solver,
and reading back the results.

While the external solver processes will be handled
by the operating system, the production of their input
seems more of a challenge, as this has to be done
in the prover properly. Parallelism must therefore
be handled by the run time environment of the implementation 
language of the prover: e.g., the Java virtual machine for
{\sf AProVE}, and the Glasgow Haskell runtime for {\sf Matchbox}.

This does not seem to scale so easily,
and a particular obstacle (for {\sf Matchbox}) seems to be
the current ``stop the world'' mode of memory management 
(allocation  and garbage collection).
It is hoped that there will be progress 
in models for conceptually high level parallelism
with efficient run-time implementations,
so that a low-level ``parallelizing rewrite''
of termination provers can be avoided.

Another way of avoiding programming efforts is to keep
a single-threaded control structure for the termination prover,
but rely on constraint solvers that exploit parallelism.
Constructing such solvers is an area of ongoing research 
in the SAT and SMT community,
but the publically available constraint solvers
do not seem to reflect this at the moment.

