Run-time algorithm specialization: Difference between revisions

Revision as of 17:17, 1 September 2009

Latest revision as of 09:47, 18 May 2025

(10 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 ==

Line 17 ⟶ 18:

The specialized 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 optimized 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.

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

In [[C (programming language)|C]] or C++ we can use a '''switch''' statement to associate

some actions with different instruction tags.

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 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, as a means of efficient optimisation. OneThis can exploitbe thisexploited by taking values for instruction identifiers from a small interval of values.

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

==Data-and-algorithm specialization==

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]]