article

Combinatorial sketching for finite programs

Authors:

Armando Solar-Lezama,

Rastislav Bodik,

Vijay SaraswatAuthors Info & Claims

ACM SIGPLAN Notices, Volume 41, Issue 11

Pages 404 - 415

https://doi.org/10.1145/1168918.1168907

Published: 20 October 2006 Publication History

Abstract

Sketching is a software synthesis approach where the programmer develops a partial implementation - a sketch - and a separate specification of the desired functionality. The synthesizer then completes the sketch to behave like the specification. The correctness of the synthesized implementation is guaranteed by the compiler, which allows, among other benefits, rapid development of highly tuned implementations without the fear of introducing bugs.We develop SKETCH, a language for finite programs with linguistic support for sketching. Finite programs include many highperformance kernels, including cryptocodes. In contrast to prior synthesizers, which had to be equipped with domain-specific rules, SKETCH completes sketches by means of a combinatorial search based on generalized boolean satisfiability. Consequently, our combinatorial synthesizer is complete for the class of finite programs: it is guaranteed to complete any sketch in theory, and in practice has scaled to realistic programming problems.Freed from domain rules, we can now write sketches as simpleto-understand partial programs, which are regular programs in which difficult code fragments are replaced with holes to be filled by the synthesizer. Holes may stand for index expressions, lookup tables, or bitmasks, but the programmer can easily define new kinds of holes using a single versatile synthesis operator.We have used SKETCH to synthesize an efficient implementation of the AES cipher standard. The synthesizer produces the most complex part of the implementation and runs in about an hour.

References

[1]

D. Andre and S. Russell. Programmable reinforcement learning agents. Advances in Neural Information Processing Systems, 13, 2001. MIT Press.

[2]

R.M. Burstall and J. Darlington. A transformation system for developing recursive programs. Journal of the ACM, 24(1):44--67, 1977.

Digital Library

[3]

E. Clarke, D. Kroening, and K. Yorav. Behavioral consistency of C and Verilog programs using bounded model checking. In DAC, pages 368--371, May 2003.

Digital Library

[4]

N. Eézn and N. Sörensson. An extensible SAT-solver. In E. Giunchiglia and A. Tacchella, editors, SAT, volume 2919 of Lecture Notes in Computer Science, pages 502--518. Springer, 2003.

[5]

Advanced encryption standard (AES). U.S. DEPARTMENT OF COMMERCE/National Institute of Standards and Technology, November 2001. http://csrc.nist.gov/publications/fips/fips197/fips-197.pdf.

[6]

B. Fischer and J. Schumann. Autobayes: a system for generating data analysis programs from statistical models. Journal of Functional Programming, 13(3):483--508, May 2003.

Digital Library

[7]

P.V. Hentenryck and V. Saraswat. Strategic directions in constraint programming. ACM Comput. Surv., 28(4):701--726, 1996.

Digital Library

[8]

R. Joshi, G. Nelson, and K.H. Randall. Denali: A goal-directed superoptimizer. In PLDI, pages 304--314, 2002.

Digital Library

[9]

Z. Manna and R.J. Waldinger. Toward automatic program synthesis. Commun. ACM, 14(3):151--165, 1971.

Digital Library

[10]

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 532--535, New York, NY, USA, 2006. ACM Press.

Digital Library

[11]

D.P. Ranjan, D. Tang, and S. Malik. A comparative study of 2qbf algorithms. In The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), May 2004.

[12]

E.M. Reingold, J. Nievergelt, and N. Deo. Combinatorial Algorithms - Theory and Practice. Prentice-Hall, 1977.

Digital Library

[13]

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 281--294, New York, NY, USA, 2005. ACM Press.

Digital Library

[14]

W. Thies, M. Karczmarek, and S. Amarasinghe. Streamit: A language for streaming applications. In International Conference on Compiler Construction, Grenoble, France, Apr. 2002.

Digital Library

[15]

H.S. Warren. Hacker's Delight. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2002.

Digital Library

[16]

P. Wegner. A technique for counting ones in a binary computer. Commun. ACM, 3(5):322, 1960.

Digital Library

[17]

Y. Xie and A. Aiken. Scalable error detection using boolean satisfiability. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 351--363, 2005.

Digital Library

Cited By

Nguyen Trong BTsushima KHu Z(2024)S_YNTHBX: An Example-guided Synthesizer for Bidirectional Programs on RelationsJournal of Information Processing10.2197/ipsjjip.32.47132(471-486)Online publication date: 2024
https://doi.org/10.2197/ipsjjip.32.471
Zhao HLiu BDehbi LXie HYang ZQian H(2024)Polynomial Neural Barrier Certificate Synthesis of Hybrid Systems via Counterexample GuidanceIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2024.344722643:11(3756-3767)Online publication date: Nov-2024
https://doi.org/10.1109/TCAD.2024.3447226
Abate AGiacobbe MRoy DSchnitzer Y(2024)Model Checking and Strategy Synthesis with Abstractions and CertificatesPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75775-4_16(360-391)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75775-4_16
Show More Cited By

Index Terms

Combinatorial sketching for finite programs
1. Software and its engineering
  1. Software creation and management
    1. Designing software
      1. Software implementation planning
        Software design techniques
    2. Software development process management
  2. Software notations and tools
    1. General programming languages
      1. Language features

Recommendations

Combinatorial sketching for finite programs
ASPLOS XII: Proceedings of the 12th international conference on Architectural support for programming languages and operating systems

Sketching is a software synthesis approach where the programmer develops a partial implementation - a sketch - and a separate specification of the desired functionality. The synthesizer then completes the sketch to behave like the specification. The ...
Sketching concurrent data structures
PLDI '08

We describe PSketch, a program synthesizer that helps programmers implement concurrent data structures. The system is based on the concept of sketching, a form of synthesis that allows programmers to express their insight about an implementation as a ...
Combinatorial sketching for finite programs
Proceedings of the 2006 ASPLOS Conference

Sketching is a software synthesis approach where the programmer develops a partial implementation - a sketch - and a separate specification of the desired functionality. The synthesizer then completes the sketch to behave like the specification. The ...

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 41, Issue 11

Proceedings of the 2006 ASPLOS Conference

November 2006

425 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1168918

Issue’s Table of Contents

ASPLOS XII: Proceedings of the 12th international conference on Architectural support for programming languages and operating systems
October 2006
440 pages
ISBN:1595934510
DOI:10.1145/1168857
General Chair:
John Paul Shen
Intel Corp.
,
Program Chair:
Margaret R. Martonosi
Princeton University

Copyright © 2006 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 October 2006

Published in SIGPLAN Volume 41, Issue 11

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

681
Total Citations
View Citations
2,396
Total Downloads

Downloads (Last 12 months)157
Downloads (Last 6 weeks)11

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Nguyen Trong BTsushima KHu Z(2024)S_YNTHBX: An Example-guided Synthesizer for Bidirectional Programs on RelationsJournal of Information Processing10.2197/ipsjjip.32.47132(471-486)Online publication date: 2024
https://doi.org/10.2197/ipsjjip.32.471
Zhao HLiu BDehbi LXie HYang ZQian H(2024)Polynomial Neural Barrier Certificate Synthesis of Hybrid Systems via Counterexample GuidanceIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2024.344722643:11(3756-3767)Online publication date: Nov-2024
https://doi.org/10.1109/TCAD.2024.3447226
Abate AGiacobbe MRoy DSchnitzer Y(2024)Model Checking and Strategy Synthesis with Abstractions and CertificatesPrinciples of Verification: Cycling the Probabilistic Landscape10.1007/978-3-031-75775-4_16(360-391)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-75775-4_16
Abate AGiacobbe MSchnitzer Y(2024)Bisimulation LearningComputer Aided Verification10.1007/978-3-031-65633-0_8(161-183)Online publication date: 26-Jul-2024
https://doi.org/10.1007/978-3-031-65633-0_8
Gu YTsukada TUnno H(2023)Optimal CHC Solving via Termination ProofsProceedings of the ACM on Programming Languages10.1145/35712147:POPL(604-631)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571214
Wang YLi ZJiang CQiu XRao S(2023)Comparative Synthesis: Learning Near-Optimal Network Designs by QueryProceedings of the ACM on Programming Languages10.1145/35711977:POPL(91-120)Online publication date: 11-Jan-2023
https://doi.org/10.1145/3571197
Jha SJha SLincoln PBastian NVelasquez AEwetz RNeema S(2023)Counterexample Guided Inductive Synthesis Using Large Language Models and Satisfiability SolvingMILCOM 2023 - 2023 IEEE Military Communications Conference (MILCOM)10.1109/MILCOM58377.2023.10356332(944-949)Online publication date: 30-Oct-2023
https://doi.org/10.1109/MILCOM58377.2023.10356332
Masti DFabiani FGnecco GBemporad A(2023)Counter-Example Guided Inductive Synthesis of Control Lyapunov Functions for Uncertain SystemsIEEE Control Systems Letters10.1109/LCSYS.2023.32851027(2047-2052)Online publication date: 2023
https://doi.org/10.1109/LCSYS.2023.3285102
Abate ABarbosa HBarrett CDavid CKesseli PKroening DPolgreen EReynolds ATinelli C(2023)Synthesising Programs with Non-trivial ConstantsJournal of Automated Reasoning10.1007/s10817-023-09664-467:2Online publication date: 13-May-2023
https://dl.acm.org/doi/10.1007/s10817-023-09664-4
Rothenberg BGrumberg OVizel YSingher E(2023)Condition Synthesis Realizability via Constrained Horn ClausesNASA Formal Methods10.1007/978-3-031-33170-1_23(380-396)Online publication date: 3-Jun-2023
https://doi.org/10.1007/978-3-031-33170-1_23
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents