Run-time algorithm specialisation

From Wikipedia, the free encyclopedia

In computer science, run-time algorithm specialisation is a methodology for creating efficient algorithms for costly computation tasks of certain kinds. The methodology originates in the field of automated theorem proving and, more specifically, in the Vampire theorem prover project.

The idea is inspired by the use of partial evaluation in optimising program translation. Many core operations in theorem provers exhibit the following pattern. Suppose that we need to execute some algorithm $a l g (A, B)$ in a situation where a value of $A$ is fixed for potentially many different values of $B$ . In order to do this efficiently, we can try to find a specialisation of $a l g$ for every fixed $A$ , i.e., such an algorithm $a l g A$ , that executing $a l g A (B)$ is equivalent to executing $a l g (A, B)$ .

The specialised algorithm may be more efficient than the generic one, since it can exploit some particular properties of the fixed value $A$ . Typically, $a l g A (B)$ can avoid some operations that $a l g (A, B)$ would have to perform, if they are known to be redundant for this particular parameter $A$ . In particular, we can often identify some tests that are true or false for $A$ , unroll loops and recursion, etc.

The key difference between run-time specialisation and partial evaluation is that the values of $A$ on which $a l g$ is specialised are not known statically, so the specialisation takes place at run-time.

There is also an important technical difference. Partial evaluation is applied to algorithms explicitly represented as codes in some programming language. At run-time, we do not need any concrete representation of $a l g$ . We only have to imagine $a l g$ when we program the specialisation procedure. All we need is a concrete representation of the specialised version $a l g A$ . This also means that we cannot use any universal methods for specialising algorithms, which is usually the case with partial evaluation. Instead, we have to program a specialisation procedure for every particular algorithm $a l g$ . An important advantage of doing so is that we can use some powerful ad hoc tricks exploiting peculiarities of $a l g$ and the representation of $A$ and $B$ , which are beyond the reach of any universal specialisation methods.

1 Specialisation with compilation
2 Data-and-algorithm specialisation
3 See also
4 Reading list

[edit] Specialisation with compilation

The specialised algorithm has to be represented in a form that can be interpreted. In many situations, usually when $a l g A (B)$ is to be computed on many values $B$ in a row, we can write $a l g A$ as a code of a special abstract machine, and we often say that $A$ is compiled. Then the code itself can be additionally optimised by answer-preserving transformations that rely only on the semantics of instructions of the abstract machine.

Instructions of the abstract machine can usually be represented as records. One field of such a record stores an integer tag that identifies the instruction type, other fields may be used for storing additional Parameters of the instruction, for example a pointer to another instruction representing a label, if the semantics of the instruction requires a jump. All instructions of a code can be stored in an array, or list, or tree.

Interpretation is done by fetching instructions in some order, identifying their type and executing the actions associated with this type. In C or C++ we can use a switch statement to associate some actions with different instruction tags. Modern compilers usually compile a switch statement with integer labels from a narrow range rather efficiently by storing the address of the statement corresponding to a value $i$ in the $i$ -th cell of a special array. One can exploit this by taking values for instruction tags from a small interval of integers.

[edit] Data-and-algorithm specialisation

There are situations when many instances of $A$ are intended for long-term storage and the calls of $a l g (A, B)$ occur with different $B$ in an unpredicatable order. For example, we may have to check $a l g (A 1, B 1)$ first, then $a l g (A 2, B 2)$ , then $a l g (A 1, B 3)$ , and so on. In such circumstances, full-scale specialisation with compilation may not be suitable due to excessive memory usage. However, we can sometimes find a compact specialised representation $A^{\prime}$ for every $A$ , that can be stored with, or instead of, $A$ . We also define a variant $\mathit{alg}^{\prime}$ that works on this representation and any call to $a l g (A, B)$ is replaced by $\mathit{alg}^{\prime}(A^{\prime},B)$ , intended to do the same job faster.

[edit] See also

Psyco, a specializing run-time compiler for Python
multi-stage programming

[edit] Reading list

This article does not cite any references or sources. (January 2007)
Please help improve this article by adding citations to reliable sources. Unverifiable material may be challenged and removed.

A. Voronkov, "The Anatomy of Vampire: Implementing Bottom-Up Procedures with Code Trees", Journal of Automated Reasoning, 15(2), 1995 (original idea)

A. Riazanov and A. Voronkov, "Efficient Checking of Term Ordering Constraints", Proc. IJCAR 2004, Lecture Notes in Artificial Intelligence 3097, 2004 (compact but self-contained illustration of the method)

A. Riazanov and A. Voronkov, Efficient Instance Retrieval with Standard and Relational Path Indexing, Information and Computation, 199(1-2), 2005 (contains another illustration of the method)

A. Riazanov, "Implementing an Efficient Theorem Prover", PhD thesis, The University of Manchester, 2003 (contains the most comprehensive description of the method and many examples)