New Applications of Program Synthesis by Armando Solar-Lezama
In this content, Armando Solar-Lezama discusses new applications of program synthesis across different eras, from the 1980s to modern views. The synthesis of distributed memory algorithms and scalability in code implementations are explored, showing the potential for synthesizing code ranging from small expressions to larger pieces reliably. The content also delves into sketching a C-like language with holes and assertions for high-level language compiler synthesis and automated tutoring, showcasing the versatility of program synthesis in various contexts.
Uploaded on Mar 03, 2025 | 0 Views
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
New applications of program synthesis Armando Solar-Lezama
Synthesis: 1980s view Complete Formal Specification
Synthesis: modern view ? = {?0 ??} Space of programs ? ? = ?1? ?2 ? ?3? ?4? Reference Implementation Input/Output Examples Test Harnesses ? ? = ??. ?(??)
Example Sketch Spec bit[W] avgSpec(bit[W] x, bit[W] y){ bit[2*W] xx = extend@signed(x, 2*W); bit[2*W] yy = extend@signed(y, 2*W); bit[W] avg(bit[W] x, bit[W] y) implements avgSpec{ return expr@signed({x,y}, 4); } bit[2*W] r = rshift@signed(xx+yy, 1); return (r[0::W]); } expr ::= const | var | expr>>?? | ~expr | expr + expr | expr ^ expr | expr & expr
And 8 seconds later (x & y) + (x ^ y) >> 1 Cool! Now can you synthesize programs with more than 1 line of code?
Synthesis of distributed memory algorithms (SC14) Synthesizer can help with non-trivial distributed memory implementations Scalability of resulting code is comparable with hand-crafted Fortran
So how much can you synthesize? A little more if you are synthesizing from scratch 5 or 6 LOC in one shot But We can synthesize many more if there is independence We can synthesize them within larger pieces of code 2-4K LOC in many cases We can do it very reliably So what can you do if you can synthesize small expressions in a large program?
Sketch C-like language with holes and assertions High-Level Language Compiler Synthesis Solution Graphical programming Automated Tutoring
Sketch C-like language with holes and assertions Synthesis Sub- problems Analysis Tool Synthesis Solution Program Optimization Graphical programming Automated Tutoring Solver Synthesis
Java to SQL Methods SQL Queries ORM libraries Objects Relations Application Database
Java to SQL Methods SQL Queries ORM libraries Objects Relations Application Database
Java to SQL List getUsersWithRoles () { List users = User.getAllUsers(); List roles = Role.getAllRoles(); SELECT * FROM user SELECT * FROM role List results = new ArrayList(); for (User u : users) { for (Role r : roles) { if (u.roleId == r.id) results.add(u); }} return results; } List getUsersWithRoles () { return executeQuery( convert to SELECT u FROM user u, role r WHERE u.roleId == r.id ORDER BY u.roleId, r.id ; }
Join Query 1000K original inferred 100K Page load time (ms) Nested-loop join Hash join! O(n2) O(n) 10K 1K 100 0 20K 40K 60K 80K 100K Number of roles / users in DB PLDI 2013 6/17/2013 15
Real-world Evaluation Wilos (project management application) 62k LOC Operation type # Fragments found 1 # Fragments converted 1 Projection Selection 13 10 Join 7 7 Aggregation 11 10 Total 33 28 6/17/2013 PLDI 2013 16
Real-world Evaluation iTracker (bug tracking system) 61k LOC Operation type # Fragments found # Fragments converted Projection 3 2 Selection 3 2 Join 1 1 Aggregation 9 7 Total 16 12 6/17/2013 PLDI 2013 17
Beyond SQL This is a general idea Synthesis Proof of Equivalence Source Code DSL Program Enable optimization by raising the level of abstraction!
Legacy code to Halide Synthesis Legacy Fortran/C++ Code Stencil DLS (Halide) Proof of Equivalence
Legacy to Halide for (k=y_min-2;k<=y_max+2;k++) { for (j=x_min-2;j<=x_max+2;j++) { post_vol[((x_max+5)*(k-(y_min-2))+(j)-(x_min-2))] =volume[((x_max+4)*(k-(y_min-2))+(j)-(x_min-2))] + vol_flux_y[((x_max+4)*(k+1 -(y_min-2))+(j)-(x_min-2))] - vol_flux_y[((x_max+4)*(k-(y_min-2))+(j)-(x_min-2))]; } } ?,? ??? post_vol[j,k] = volume[j,k] + vol_flux[j,k+1] + vol_flux[j,k]
Speedups Speedups on 24 cores
Example out = 0 for(int i=0; i<n-1; ++i){ out[i+1] = in[i]; } ???,??,?. ??? ??? = ??? 1,? ?? ??? 1 0 ???? How do you prove that the code implies the formula? Induction!
Inductive hypothesis out = 0 for(int i=0; i<n-1; ++i){ out[i+1] = in[i]; } 0 ? ? 1 ? [1,?] ??? ? = ?? ? 1 ? 1,? ??? ? = 0 Also called a loop invariant
Proofs about loops Base case: Invariant holds at step zero Inductive case: If invariant holds at i, it holds at i+1 Invariant Spec
Abstract view Verification conditions Base case: ????????? ?????0 Inductive case: ?????. ????????? ????? ???? ????? ?????????(?????? ????? ) Invariant Spec ?????. ????????? ????? ???? ????? ????(?????)
Invariant Spec out = 0 for(int i=0; i<n-1; ++i){ out[i+1] = in[i]; } 0 ? ? 1 ? [1,?] ??? ? = ?? ? 1 ? 1,? ??? ? = 0 ??? ??? = ??? 1,? ?? ??? 1 0 ? ? 1 ?,?,???,??,??? ???? loopCond ??? = ???? Loop invariant
Problem Base case: ????????? ?????0 Invariant and Spec are unknown! Inductive case: ?????. ????????? ????? ???? ????? ?????????(?????? ????? ) Invariant Spec ?????. ????????? ????? ???? ????? ????(?????)
Synthesis problem Spec ?,? ??? out[j,k] = Expr({in[i+??,j+??]}) ... Invariant ?,? ??? out[j,k] = Expr({in[i+??,j+??]}) ... Find Spec and invariant that satisfy verification conditions
12 hrs It can be slow 18000 14400 Synthesis Time (s) 10800 7200 3600 0 Benchmark Synthesis time with parallel synthesis on 24 cores
But we know how to parallelize it
Moving forward Applications Synthesis as a core tool for a variety of problems Techniques Data driven synthesis Leveraging big code Synthesis for synthesizers
