Code generation by matching and satisfiability search
First Claim
1. A method for producing, for a target computer architecture and a program fragment, a near-optimal code sequence for executing the program fragment on the target computer, comprising:
- repeatedly invoking an automatic theorem prover for plural cycle budgets todetermine a minimum cycle budget that is the lowest of any cycle budget K for which a formalized mathematical conjecture that no code sequence for the target computer architecture executes the program fragment within the cycle budget K is unprovable by the automatic theorem prover, andextract the near optimal code sequence from a counterexample implicit in the failed proof of the formalized mathematical conjecture for the minimum cycle budget.
2 Assignments
0 Petitions
Accused Products
Abstract
A tool and method for automatically producing near-optimal code sequences are particularly useful for generating near-optimal code sequences in inner loops, crucial subroutines, and device drivers. As a novel functional and architectural strategy, the invention contemplates applying technologies that would be normally in automatic theorem proving to the problem of automatic code generation. The aspect of the automatic theorem proving is realized by matching followed by planning with satisfiability search. Notably also, the present invention targets a goal-oriented, cycle budget limited code sequence in producing the near-optimal code sequence.
14 Citations
43 Claims
-
1. A method for producing, for a target computer architecture and a program fragment, a near-optimal code sequence for executing the program fragment on the target computer, comprising:
repeatedly invoking an automatic theorem prover for plural cycle budgets to determine a minimum cycle budget that is the lowest of any cycle budget K for which a formalized mathematical conjecture that no code sequence for the target computer architecture executes the program fragment within the cycle budget K is unprovable by the automatic theorem prover, and extract the near optimal code sequence from a counterexample implicit in the failed proof of the formalized mathematical conjecture for the minimum cycle budget. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8, 18)
-
9. A method for producing, for a target computer architecture and a program fragment, a near-optimal code sequence for executing the program fragment on the target computer, comprising:
-
repeatedly invoking an automatic theorem prover to prove unsatisfiable a formalized mathematical conjecture that, for a cycle budget K, no code sequence for the target computer architecture executes the program fragment within that cycle budget K, wherein if the proof fails, a K-cycled program computing the program fragment is embedded in the failed proof, wherein the near-optimal code sequence is found, and the invocation need not be repeated, when it is established that both the K-cycled program computes the program fragment and a cycle budget K−
1 is insufficient in that the cycle budget K is minimum, the K-cycled program being extracted as the near-optimal code sequence, andwherein, if the near-optimal code sequence is not found in a present invocation, for a next revocation of the automatic theorem prover if the proof succeeds the cycle budget K is doubled (K;
=K*2) and if the proof fails the cycle budget is bisected (K;
=K/2) and a new K-cycled program computing the program fragment that is embedded in the failed proof is extracted. - View Dependent Claims (10, 11, 12, 13, 14, 15, 16, 17, 19)
-
-
20. A method for automatic generation of a near-optimal code sequence for execution on a computer, comprising:
applying automatic theorem-proving to a code sequence generator, including introducing a multi-assignment to the code sequence generator, producing, by the code sequence generator based on the multi-assignment, a number of possible plans for creating the near-optimal code sequence, and performing, by the code sequence generator, planning with a satisfiability search to select an optimal plan from among the possible plans for automatically producing the near-optimal code sequence, wherein performing the planning with the satisfiability search is repeated a plurality of times for plural machine cycle budgets to find the optimal plan associated with a predetermined machine cycle budget. - View Dependent Claims (21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 37)
-
33. A code sequence generation tool for automatic generation of a near-optimal code sequence executable on a computer, comprising:
-
an input capable of receiving a multi-assignment; a matcher responsive to the multi-assignment and producing, via matching of the multi-assignment and facts regarding operators computable in the computer, a number of possible plans for creating the near-optimal code sequence; and a planner configured to select via a satisfiability search an optimal plan from among the possible plans produced by the matcher, the optimal plan corresponding to the near-optimal code sequence, wherein the code sequence generation tool is configured to invoke the matcher and the planner thereby implementing automatic theorem-proving for automatically generating the near-optimal code sequence. - View Dependent Claims (34, 35, 38)
-
-
36. A code sequence generation tool for automatic generation of a near-optimal code sequence executable on a computer, comprising:
-
an input capable of receiving a multi-assignment; matching means responsive to the multi-assignment and producing, via matching of the multi-assignment and facts regarding operators computable in the computer, a number of possible plans for creating the near-optimal code sequence; and planning means configured to select via a satisfiability search an optimal plan from among the possible plans produced by the matching means, the optimal plan corresponding to the near-optimal code sequence, wherein the code sequence generation tool is configured to invoke the matching means and the planning means thereby implementing automatic theorem-proving for automatically generating the near-optimal code sequence. - View Dependent Claims (39)
-
-
40. A method of producing a near-optimal code sequence for at least a fragment of a program executable on a computer comprising:
-
inputting expressions corresponding to the fragment of the program to a computer-executable code sequence generator; generating, by the code sequence generator based on the input expressions and facts regarding operators computable in the computer, a data structure representing plural ways of computing the expressions; and performing a satisfiability search by the code sequence generator to select one of the ways as an optimal solution associated with a minimum machine cycle budget, the optimal solution corresponding to the near-optimal code sequence. - View Dependent Claims (41)
-
-
42. A computer-readable medium embodying computer program code configured to cause a computer to generate a near-optimal code sequence for at least a fragment of a program, comprising:
-
inputting expressions corresponding to the fragment of the program to a code sequence generator; generating, by the code sequence generator based on the input expressions and facts regarding operators computable in a computer, a data structure representing plural ways of computing the expressions; and performing a satisfiability search by the code sequence generator to select one of the ways as an optimal solution associated with a minimum machine cycle budget, the optimal solution corresponding to the near-optimal code sequence. - View Dependent Claims (43)
-
Specification