Elamur Research⌕
☰
home / papers / 2008 / Program Synthesis by Sketching

Program Synthesis by Sketching

Paper · 2008 · Armando Solar-Lezama

Summary

Automatic program synthesis promises code generated from high-level specifications, but efficient implementations need both algorithmic insight, which only humans supply well, and tedious low-level details, which suit a machine. Earlier systems tried to combine the two through meta-programming or theorem-prover-style interaction, and both force programmers to learn unfamiliar formalisms. This thesis proposes sketching instead. The programmer writes an ordinary partial program, a "sketch," that fixes the overall structure and marks the missing details as holes. The synthesizer then fills those holes.

The engine is a SAT-based inductive synthesizer that can find a correct completion from only a handful of test inputs. It is embedded in counterexample guided inductive synthesis (CEGIS): a validator checks each candidate against the specification and returns failing inputs as new tests. With some extensions, the same sequential synthesizer also handles concurrent programs, because all concurrency reasoning is left to an off-the-shelf checker. A domain-specific layer for stencil computations reduces stencil sketches to simpler problems that CEGIS can solve. Together, the results show that synthesis can be made practical for everyday programming.

Key points

  • Sketch language and CEGIS. The Sketch language expresses programmer intent as code with holes. CEGIS alternates between inductive synthesis and validation until the candidate meets the specification.
  • Sequential results. Benchmarks range from bit-level ciphers to linked data structure manipulations. The system produced a complete optimized AES implementation, and its performance was compared against a QBF-based approach.
  • Concurrent results. Within minutes, the concurrency-aware version synthesized the details of a fine-grained locking concurrent set, a sense-reversing barrier and a dining philosophers solution.
  • Stencil domain. Stencil-specific knowledge was used to build a MultiGrid solver for partial differential equations that incorporates several difficult implementation strategies from the literature.
  • Tools and context. The pipeline relies heavily on ABC, a circuit analysis tool by Brayton and Mishchenko. The thesis was advised by Rastislav Bodik and published as UC Berkeley technical report UCB/EECS-2008-177.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Fields, topics and concepts

📚 Shelf 1The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 works

🧭 Topics 1Research subjects and languages the work is about.Code & programming languages · 194 works

Cite

Cite as Armando Solar-Lezama. 2008. Program Synthesis by Sketching. PhD thesis, UC Berkeley (EECS-2008-177).

The paper itself, not this page. BibTeX from the library's record of the work.

@inproceedings{solarlezama2008program,
  title = {{Program Synthesis by Sketching}},
  author = {Armando Solar-Lezama},
  booktitle = {PhD thesis, UC Berkeley (EECS-2008-177)},
  year = {2008},
  url = {https://www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-177.pdf}
}

References

71 references, 0 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. W. Ackermann. Solvable cases of the decision problem . Studies in Logic and the Foundations. of Mathematics. North-Holland 1954. find
  2. D. Amit, N. Rinetzky, M. Sagiv, and E. Yahav. Comparison under abstraction for verifying linearizability. In In 19th International Conference on Computer Aided Veri-cation (CAV) , 2007. find
  3. S. E. Anderson. Bit twiddling hacks, 1997-2005. http://www-graphics.stanford.edu/ se-ander/bithacks.html. ↗
  4. D. Andre and S. Russell. Programmable reinforcement learning agents. Advances in Neural Information Processing Systems , 13, 2001. MIT Press. find
  5. D. Angluin and C. H. Smith. Inductive inference: Theory and methods. ACM Comput. Surv. , 15(3):237269, 1983. find
  6. D. H. Bailey, E. Barszcz, J. T. Barton, D. S. Browning, R. L. Carter, D. Dagum, R. A. Fatoohi, P. O. Frederickson, T. A. Lasinski, R. S. Schreiber, H. D. Simon, V. Venkatakrishnan, and S. K. Weeratunga. The nas parallel benchmarks. The International Journal of Supercomputer Applications , 5(3):6373… find
  7. T. Ball and S. K. Rajamani. The slam project: debugging system software via static analysis. In POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , pages 13, New York, NY, USA, 2002. ACM. find
  8. Y. Bar-David and G. Taubenfeld. Automatic discovery of mutual exclusion algorithms. In PODC '03: Proceedings of the twenty-second annual symposium on Principles of distributed computing , pages 305305, New York, NY, USA, 2003. ACM. find
  9. L. Beckman, A. Haraldson, O. Oskarsson, and E. Sandewall. A partial evaluator, and its use as a programming tool. Articial Intelligence , 7:319357, 1976. find
  10. M. Bickford, C. Kreitz, R. V. Renesse, and R. Constable. An experiment in formal design using meta-properties. In In Proc. DISCEX-II ’01: The 2nd DARPA Information Survivability Conference and Exposition. IEEE , 2001. find
  11. A. Biere. Resolve and expand. In Proceedings of the 7th Intl. Conf. on Theory and Applications of Satisability Testing (SAT'04) , 2005. find
  12. J. Bilmes, K. Asanovic, C.-W. Chin, and J. Demmel. Optimizing matrix multiply using phipac: A portable, high-performance, ansi c coding methodology. In International Conference on Supercomputing , pages 340347, 1997. find
  13. W. L. Briggs, V. E. Henson, and S. F. McCormick. A Multigrid Tutorial . SIAM, 2000. find
  14. R. E. Bryant, S. German, and M. N. Velev. Processor verication using ecient reductions of the logic of uninterpreted functions to propositional logic. ACM Transactions on Computational Logic , 2(1):141, January 2001. find
  15. R. E. Bryant, D. Kroening, J. Ouaknine, S. A. Seshia, O. Strichman, and B. Brady. Deciding bit-vector arithmetic with abstraction. In Proc. TACAS 2007 , March 2007. find
  16. M. A. Bulyonkov. Polyvariant mixed computation for analyzer programs. Acta Informatica , 21(5), December 1984. find
  17. M. Burstein, D. Mcdermott, D. R. Smith, and S. J. Westfold. Derivation of glue code for agent interoperation. In In Proc. 4th Int’l. Conf. on Autonomous Agents , pages 277284. ACM Press, 2000. find
  18. E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction renement for symbolic model checking. J. ACM , 50(5):752794, 2003. find
  19. E. Clarke, D. Kroening, and K. Yorav. Behavioral consistency of C and Verilog programs using bounded model checking. In DAC , pages 368371, May 2003. find
  20. E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs, Workshop , pages 5271, London, UK, 1982. Springer-Verlag. find
  21. E. M. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In Proc. 10 th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) , 2004. find
  22. C. Consel and O. Danvy. Tutorial notes on partial evaluation. In Proceedings of the Twentieth Annual ACM Symposium on Principles of Programming Languages , pages 493501. ACM Press, 1993. find
  23. R. L. Constable. Implementing Mathematics with the NuPRL Proof Development System . Prentice Hall, 1986. find
  24. D. Currie, X. Feng, M. Fujita, A. J. Hu, M. Kwan, and S. Rajan. Embedded software verication using symbolic execution and uninterpreted functions. Int. J. Parallel Program. , 34(1):6191, 2006. find
  25. C. C. Douglas, J. Hu, M. Kowarschik, U. Rüde, and C. Weiss. Cache optimization for structured and unstructured grid multigrid. Elect. Trans. Numer. Anal. , 10:2140, 2000. find
  26. T. Emerson. Development of a constraint-based airlift scheduler by program synthesis from formal specications. In Proceedings of the 1999 Conference on Automated Software Engineering . IEEE Computer Society Press, 1999. find
  27. Advanced encryption standard MERCE/National Institute http://csrc.nist.gov/publications/ps/ps197/ps-197.pdf. ↗
  28. B. Fischer and J. Schumann. Autobayes: a system for generating data analysis programs from statistical models. Journal of Functional Programming , 13(3):483508, May 2003. find
  29. M. Frigo and S. Johnson. Fftw: An adaptive software architecture for the t. In ICASSP conference proceedings , volume 3, pages 13811384, 1998. find
  30. M. Frigo and V. Strumpen. The memory behavior of cache oblivious stencil computations. The Journal of Supercomputing , 39(2):93112, 2007. find
  31. V. Ganesh. Decision procedures for bit-vectors, arrays and integers . PhD thesis, Stanford, CA, USA, 2007. Adviser-David L. Dill. (AES). U.S. DEPARTMENT OF COM-of Standards and Technology, November 2001. find
  32. P. Godefroid. Partial-Order Methods for the Verication of Concurrent Systems  An Approach to the State-Explosion Problem . PhD thesis, 1994. find
  33. E. M. Gold. Language identication in the limit. Information and Control , 10(5):447 474, 1967. find
  34. C. K. Gomard. A self-applicable partial evaluator for the lambda calculus: correctness and pragmatics. ACM Trans. Program. Lang. Syst. , 14(2):147172, 1992. find
  35. S. Heller, M. Herlihy, V. Luchangco, M. Moir, W. N. S. III, and N. Shavit. A lazy concurrent list-based set algorithm. In OPODIS '05: 9th International Conference on Principles of Distributed Systems , volume 3974, pages 316. Springer, 2005. find
  36. D. Hensgen, R. Finkel, and U. Manber. Two algorithms for barrier synchronization. International Journal of Parallel Programming , 17(1):117, 1988. find
  37. T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software verication with blast. pages 235239. Springer, 2003. find
  38. M. Herlihy and N. Shavit. The art of multiprocessor programming . Morgan Kaufmann, 2008. find
  39. M. P. Herlihy and J. M. Wing. Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. , 12(3):463492, 1990. find
  40. G. J. Holzmann. The model checker SPIN. Software Engineering , 23(5):279295, 1997. find
  41. N. D. Jones, C. K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation . Prentice Hall International, International Series in Computer Science, June 1993. ISBN number 0-13-020249-5 (pbk). find
  42. S. Kamil, K. Datta, S. Williams, L. Oliker, J. Shalf, and K. Yelick. Implicit and explicit optimizations for stencil computations. In MSPC '06: Proceedings of the 2006 workshop on Memory system performance and correctness , pages 5160, New York, NY, USA, 2006. ACM Press. find
  43. S. Kamil, P. Husbands, L. Oliker, J. Shalf, and K. A. Yelick. Impact of modern memory subsystems on cache optimizations for stencil computations. In B. Calder and B. G. Zorn, editors, Memory System Performance , pages 3643. ACM, 2005. find
  44. L. Lamport. How to make a multiprocessor computer that correctly executes multi-process programs. IEEE Transactions on Computers , 28(9):690691, 1979. find
  45. Z. Manna and R. Waldinger. Synthesis: Dreams =\> programs. IEEE Transactions on Software Engineering , 5(4):294328, 1979. find
  46. Z. Manna and R. Waldinger. A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst. , 2(1):90121, 1980. find
  47. A. W. Mazurkiewicz. Basic notions of trace theory. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop , pages 285 363, London, UK, 1989. Springer-Verlag. find
  48. K. L. McMillan. Symbolic Model Checking . Kluwer Academic Publishers, 1993. find
  49. A. Mishchenko, S. Chatterjee, and R. Brayton. Dag-aware AIG rewriting: A fresh look at combinational logic synthesis. In DAC '06: Proceedings of the 43rd annual conference on Design automation , pages 532535, New York, NY, USA, 2006. ACM Press. find
  50. A. Pnueli and R. Rosner. On the synthesis of an asynchronous reactive module. In ICALP '89: Proceedings of the 16th International Colloquium on Automata, Languages and Programming , pages 652671, London, UK, 1989. Springer-Verlag. find
  51. A. Pnueli and R. Rosner. Distributed reactive systems are hard to synthesize. In Foundations of Computer Science 1990 . IEEE, 1990. find
  52. A. Pnueli, O. Shtrichman, and M. Siegel. The code validation tool (cvt). International Journal on Software Tools for Technology Transfer (STTT) , 2, December 1998. find
  53. G. Roth, J. Mellor-Crummey, K. Kennedy, and R. G. Brickner. Compiling stencils in high performance fortran. In Supercomputing '97: Proceedings of the 1997 ACM/IEEE conference on Supercomputing (CDROM) , pages 120, New York, NY, USA, 1997. ACM Press. find
  54. H. Samulowitz and F. Bacchus. F.: Binary clause reasoning in qbf. In In: Proc. of SAT. LNCS 4121 , pages 353367. Springer, 2006. find
  55. D. Scott and C. Strachey. Toward a mathematical semantics for computer languages. Programming Research Group Technical Monograph PRG-6, Oxford Univ. Computing Lab., 1971. find
  56. S. Sellappa and S. Chatterjee. Cache-ecient multigrid algorithms. Int. J. High Perform. Comput. Appl. , 18(1):115133, 2004. find
  57. E. Y. Shapiro. Algorithmic Program DeBugging . MIT Press, Cambridge, MA, USA, 1983. find
  58. A. Silberschatz and P. B. Galvin. Operating System Concepts . John Wiley & Sons, Inc., New York, NY, USA, 2000. find
  59. D. R. Smith. KIDS: A semiautomatic program development system. IEEE Transactions on Software Engineering , 16(9):10241043, 1990. find
  60. L. Snyder. Programming Guide to ZPL . MIT Press, Cambridge, MA, 1999. find
  61. A. Solar-Lezama, G. Arnold, L. Tancau, R. Bodik, V. Saraswat, and S. Seshia. Sketching stencils. In PLDI '07: Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation , volume 42, pages 167178, New York, NY, USA, 2007. ACM. find
  62. A. Solar-Lezama, C. Jones, G. Arnold, and R. Bodík. Sketching concurrent datastructures. In PLDI 08 , 2008. find
  63. A. Solar-Lezama, R. Rabbah, R. Bodik, and K. Ebcioglu. Programming by sketching for bit-streaming programs. In PLDI '05: Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation , pages 281294, New York, NY, USA, 2005. ACM Press. find
  64. W. Thies, M. Karczmarek, and S. Amarasinghe. Streamit: A language for streaming applications. In International Conference on Compiler Construction , Grenoble, France, Apr. 2002. find
  65. M. Vechev and E. Yahav. Deriving linearizable ne-grained concurrent objects. In PLDI '08: Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation , pages 125135, New York, NY, USA, 2008. ACM. find
  66. M. T. Vechev, E. Yahav, and D. F. Bacon. Correctness-preserving derivation of concurrent garbage collection algorithms. In PLDI '06: Proceedings of the 2006 ACM SIG-PLAN conference on Programming language design and implementation , pages 341353, New York, NY, USA, 2006. ACM. find
  67. M. T. Vechev, E. Yahav, D. F. Bacon, and N. Rinetzky. Cgcexplorer: a semi-automated search procedure for provably correct concurrent collectors. In PLDI '07: Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation , pages 456467, New York, NY, USA, 2007. ACM… find
  68. W. Visser and K. Havelund. Model checking programs. In Automated Software Engineering Journal , pages 312. Press, 2000. find
  69. H. S. Warren. Hacker's Delight . Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2002. find
  70. D. Wonnacott. Achieving scalable locality with time skewing. International Journal of Parallel Programming , 30(3):1221, 2002. find
  71. Y. Xie and A. Aiken. Scalable error detection using boolean satisability. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) , pages 351363, 2005. find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/lezama-2008-program-synthesis-sketching/