Run-time algorithm specialization: Difference between revisions

Revision as of 19:08, 28 August 2009

Latest revision as of 09:47, 18 May 2025

(13 intermediate revisions by 10 users not shown)

Line 1:

{{no footnotes|date=November 2023}}

In [[computer science]], '''run-time algorithm specialisationspecialization''' 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 <math>\mathit{alg}(A,B)</math> in a situation where a value of <math>A</math> ''is fixed for potentially many different values of'' <math>B</math>. In order to do this efficiently, we can try to find a specialisationspecialization of <math>\mathit{alg}</math> for every fixed <math>A</math>, i.e., such an algorithm <math>\mathit{alg}_A</math>, that executing <math>\mathit{alg}_A(B)</math> is equivalent to executing <math>\mathit{alg}(A,B)</math>.

The specialisedspecialized algorithm may be more efficient than the generic one, since it can ''exploit some particular properties'' of the fixed value <math>A</math>. Typically, <math>\mathit{alg}_A(B)</math> can avoid some operations that <math>\mathit{alg}(A,B)</math> would have to perform, if they are known to be redundant for this particular parameter <math>A</math>.

In particular, we can often identify some tests that are true or false for <math>A</math>, unroll loops and recursion, etc.

== Difference from partial evaluation ==

The key difference between run-time specialisationspecialization and partial evaluation is that the values of <math>A</math> on which <math>\mathit{alg}</math> is specialised are not known statically, so the ''specialisationspecialization 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 <math>\mathit{alg}</math>. We only have to ''imagine'' <math>\mathit{alg}</math> ''when we program'' the specialisationspecialization procedure.

All we need is a concrete representation of the specialisedspecialized version <math>\mathit{alg}_A</math>. This also means that we cannot use any universal methods for specialisingspecializing algorithms, which is usually the case with partial evaluation. Instead, we have to program a specialisationspecialization procedure for every particular algorithm <math>\mathit{alg}</math>. An important advantage of doing so is that we can use some powerful ''ad hoc'' tricks exploiting peculiarities of <math>\mathit{alg}</math> and the representation of <math>A</math> and <math>B</math>, which are beyond the reach of any universal specialisationspecialization methods.

==SpecialisationSpecialization with compilation==

The specialisedspecialized algorithm has to be represented in a form that can be interpreted.

In many situations, usually when <math>\mathit{alg}_A(B)</math> is to be computed on many values <math>B</math> in a row, we can write <math>\mathit{alg}_A</math> as a code of a special [[abstract machine]], and we often say that <math>A</math> 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.

In many situations, usually when <math>\mathit{alg}_A(B)</math> is to be computed on many values of <math>B</math> in a row, we can write <math>\mathit{alg}_A</math> can be written as amachine code ofinstructions for a special [[abstract machine]], and weit oftenis typically saysaid that <math>A</math> is ''compiled''. The code itself can then be additionally optimized 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.

The instructions of the abstract machine can usually be represented as [[Record (computer science)|record]]s. One field of such a record, an ''instruction identifier'' (or ''instruction tag''), would identify the instruction type, e.g. an [[Integer (computer science)|integer]] field may be used, with particular integer values corresponding to particular instructions. Other fields may be used for storing additional parameters of the instruction, e.g. a [[Pointer (computer programming)|pointer]] field may point to another instruction representing a label, if the semantics of the instruction require a jump. All instructions of the code can be stored in a traversable [[data structure]] such as an [[Array (data type)|array]], [[linked list]], or [[Tree (abstract data type)|tree]].

Interpretation is done by fetching instructions in some order, identifying their type

and executing the actions associated with this type.

In [[C (programming language)|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 <math>i</math> in the <math>i</math>-th cell of a special array. One can exploit this

by taking values for instruction tags from a small interval of integers.

''Interpretation'' is(or done''execution'') proceeds by fetching instructions in some order, identifying their type, and executing the actions associated with said type.

==Data-and-algorithm specialisation==

In many programming languages, such as [[C (programming language)|C]] and [[C++]], a simple [[Switch statement|<code>switch</code> statement]] may be used to associate actions with different instruction identifiers. Modern compilers usually compile a <code>switch</code> statement with constant (e.g. integer) labels from a narrow range by storing the address of the statement corresponding to a value <math>i</math> in the <math>i</math>-th cell of a special array, as a means of efficient optimisation. This can be exploited by taking values for instruction identifiers from a small interval of values.

There are situations when many instances of <math>A</math> are intended for long-term storage and the calls of <math>\mathit{alg}(A,B)</math> occur with different <math>B</math> in an unpredicatable order.

==Data-and-algorithm specialisationspecialization==

There are situations when many instances of <math>A</math> are intended for long-term storage and the calls of <math>\mathit{alg}(A,B)</math> occur with different <math>B</math> in an unpredicatableunpredictable order.

For example, we may have to check <math>\mathit{alg}(A_1,B_1)</math> first, then <math>\mathit{alg}(A_2,B_2)</math>, then <math>\mathit{alg}(A_1,B_3)</math>, and so on.

In such circumstances, full-scale specialisationspecialization with compilation may not be suitable due to excessive memory usage.

However, we can sometimes find a compact specialisedspecialized representation <math>A^{\prime}</math>

for every <math>A</math>, that can be stored with, or instead of, <math>A</math>.

We also define a variant <math>\mathit{alg}^{\prime}</math> that works on this representation

Line 47 ⟶ 44:

==References==

* [https://doi.org/10.1007%2FBF00881918 A. Voronkov, "The Anatomy of Vampire: Implementing Bottom-Up Procedures with Code Trees", ''Journal of Automated Reasoning'', 15(2), 1995] (''original idea'')

==Further reading==

* A. Riazanov and [[Andrei Voronkov|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, [http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.57.8542 Efficient Instance Retrieval with Standard and Relational Path Indexing], [[Information and Computation]], 199(1-2), 2005 (''contains another illustration of the method'')

* A. Riazanov and A. Voronkov, [http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.57.8542 Efficient Instance Retrieval with Standard and Relational Path Indexing], Information and Computation, 199(1-2), 2005 (''contains another illustration of the method'')

* A. Riazanov, [http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.4.2624 "Implementing an Efficient Theorem Prover"], PhD thesis, The University of Manchester, 2003 (''contains the most comprehensive description of the method and many examples'')

[[Category:Algorithms]]

[[Category:Software performance optimization]]