Parallel search in program synthesis

• US 11,194,800 B2
• Filed: 04/26/2018
• Issued: 12/07/2021
• Est. Priority Date: 04/26/2018
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Inventors: Gulwani, Sumit, Udupa, Abhishek, Vollmer, Michael
• Primary Examiner(s): Kindred, Alford W
• Assistant Examiner(s): Bui, Tiffany Thuy
• Application Number:
  US15/963,590
• Publication Number:
  US 20190332704A1
• Time in Patent Office: 1,321 Days
• CPC Class Codes: G06F 16/24532 of parallel queries
• CPC Class Codes: G06F 2209/5017 Task decomposition
• CPC Class Codes: G06F 9/5027 the resource being a machine, e.g. CPUs, Servers, Terminals
• CPC Class Codes: G06F 9/5038 considering the execution order of a plurality of tasks, e.g. taking priority or time dependency constraints into consideration scheduling strategies G06F9/4881 and subgroups
• CPC Class Codes: G06N 20/00 Machine learning
• CPC Class Codes: G06N 3/08 Learning methods
• CPC Class Codes: G06N 5/01 Dynamic search techniques; Heuristics; Dynamic trees; Branch-and-bound

Abstract

Systems, methods, and computer-executable instructions for parallel searching in program synthesis. A task to synthesize in a domain specific language (DSL) is received. The task is synthesized. Synthesizing the task includes generating sub-goals based on the task. The synthesized task includes a subset of the sub-goals. An estimated completion time for each of the sub-goals is expressed using the DSL is determined. The sub-goals are scheduled based on the estimated completion time. Some of the sub-goals are scheduled to be executed in parallel. The sub-goals are solved based on the scheduling to synthesize the task in the DSL. An elapsed real time to complete the synthesizing the task is reduced compared to scheduling the sub-goals in an order based on sub-goal generation.

Claims

1. A method for parallel scheduling in program synthesis, the method comprising operations performed using an electronic processor, the operations comprising:

receiving a task to synthesize in a domain specific language (DSL);

synthesizing the task, wherein synthesizing of the task comprises;

generating a plurality of independently executable multilevel sub-goals based on the task, wherein the synthesized task comprises a solved subset of the plurality of the sub-goals;

determining an estimated completion time for each of the plurality of sub-goals, wherein the estimated completion time is provided by a predictor trained using a plurality of training tasks in the DSL, wherein determining the estimated completion time for each of the plurality of sub-goals comprises serializing each of the plurality of subgoals, and wherein each of the plurality of sub-goals is expressed using the DSL;

scheduling the plurality of the sub-goals based on the estimated completion time, wherein at least two of the plurality of the sub-goals are scheduled to be executed in parallel; and

solving the plurality of sub-goals based on the scheduling to synthesize the task in the DSL, wherein an elapsed real time to complete the synthesizing the task is reduced compared to scheduling the sub-goals in an order based on sub-goal generation.

2. The method of claim 1, further comprising determining an estimated memory usage of each of the plurality of sub-goals, wherein scheduling the plurality of sub-goals is based on the estimate memory usage.

3. The method of claim 1, further comprising training the predictor using the plurality of training tasks in the DSL.

4. The method of claim 3, wherein training the predictor comprises:

for each of the plurality of training tasks;

generating a plurality of sub-tasks;

executing each of the plurality of sub-tasks, wherein an completion time is recorded; and

storing, for each of the plurality of sub-tasks, a representation of the sub-task and the completion time.

5. The method of claim 4, wherein the predictor is a neural network and the training trains the neural network to estimate the estimated completion time of a sub-task.

6. The method of claim 1, wherein the some of the plurality of the sub-goals are scheduled to be executed in parallel are assigned to different central processing units.

7. The method of claim 1, wherein the some of the plurality of the sub-goals are scheduled to be executed in parallel are assigned to different processing cores of a central processing unit.

8. The method of claim 1, wherein receiving a task to synthesize comprises receiving a specification for the task.

9. A system for parallel scheduling of sub-goals, the system comprising:

an electronic processor configured to receive a task to synthesize in a domain specific language (DSL);

a computer-readable storage medium storing computer-executable instructions for execution by the electronic processor to implement;

a parallelized synthesizer configured to synthesize the task, wherein to synthesize the task the parallelized synthesizer is configured to;

generate a plurality of independently executable multilevel sub-goals based on the task, wherein the synthesized task comprises a subset of the plurality of the sub-goals; and

determine an estimated completion time for each of the plurality of sub-goals, wherein the estimated completion time is provided by a predictor trained using a plurality of training tasks in the DSL, wherein determining the estimated completion time for each of the plurality of sub-goals comprises serializing each of the plurality of subgoals, and wherein each of the plurality of sub-goals is expressed using the DSL; and

a scheduler configured to schedule the plurality of the sub-goals based on the estimated completion time, wherein some of the plurality of the sub-goals are scheduled to be executed in parallel on computing resources, and wherein an elapsed real time to complete the task synthesis is reduced compared to the sub-goals executed in an order based on sub-goal generation.

10. The system of claim 9, further comprising computing resources configured to solve the plurality of sub-goals based on the scheduling to synthesize the task in the DSL.

11. The system of claim 9, wherein the parallelized synthesizer is further configured to determine an estimated memory usage of each of the plurality of sub-goals, wherein the scheduler is configured to use the estimate memory usage to schedule the plurality of sub-goals.

12. The system of claim 9, wherein the electronic processor is further configured to

train the machine learning model on a plurality of training tasks in the DSL.

13. The system of claim 12, wherein to train the machine learning model, the electronic processor predictor is configured to:

for each of the plurality of training tasks;

generate a plurality of sub-tasks;

execute each of the plurality of sub-tasks, wherein an completion time is recorded; and

store, for each of the plurality of sub-tasks, a representation of the sub-task and the completion time.

14. A computer-readable storage medium storing computer-executable instructions for parallel scheduling of sub-goals, the stored instructions comprising:

instructions to receive a task to synthesize in a domain specific language (DSL);

instructions to synthesize the task, wherein the instructions to synthesize the task comprise;

instructions to generate a plurality of independently executable multilevel sub-goals based on the task, wherein the synthesized task comprises a subset of the plurality of the sub-goals; and

instructions to determine an estimated completion time for each of the plurality of sub-goals, wherein the estimated completion time is provided by a predictor trained using a plurality of training tasks in the DSL, wherein determining the estimated completion time for each of the plurality of sub-goals comprises serializing each of the plurality of subgoals, and wherein each of the plurality of sub-goals is expressed using the DSL; and

instructions to schedule the plurality of the sub-goals based on the estimated completion time, wherein some of the plurality of the sub-goals are scheduled to be executed in parallel on computing resources, and wherein an elapsed real time to complete the task synthesis is reduced compared to the sub-goals executed in an order based on sub-goal generation.

15. The computer-readable storage medium of claim 14, further comprising instructions to solve the plurality of sub-goals based on the scheduling to synthesize the task in the DSL.

16. The computer-readable storage medium of claim 14, further comprising instructions to determine an estimated memory usage of each of the plurality of sub-goals, wherein estimated memory is used to schedule the plurality of sub-goals.

17. The computer-readable storage medium of claim 14, wherein the instructions further comprise:

instructions to train the machine learning model on a plurality of training tasks in the DSL.