More Web Proxy on the site http://driver.im/

Article

Combinatorial sketching for finite programs

Authors:

Armando Solar-Lezama,

Rastislav Bodik,

Vijay SaraswatAuthors Info & Claims

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

Pages 404 - 415

https://doi.org/10.1145/1168857.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

Chen SMolu LFazlyab M(2024)Verification-Aided Learning of Neural Network Barrier Functions with Termination Guarantees2024 American Control Conference (ACC)10.23919/ACC60939.2024.10645043(3610-3617)Online publication date: 10-Jul-2024
https://doi.org/10.23919/ACC60939.2024.10645043
Mariano BWang ZPailoor SCollberg CDillig I(2024)Control-Flow Deobfuscation using Trace-Informed Compositional Program SynthesisProceedings of the ACM on Programming Languages10.1145/36897898:OOPSLA2(2211-2241)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689789
Craaijo JVerbeek FRavindran B(2024)libLISA: Instruction Discovery and Analysis on x86-64Proceedings of the ACM on Programming Languages10.1145/36897238:OOPSLA2(333-361)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689723
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
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 ...
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 ...
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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

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

ACM SIGOPS Operating Systems Review Volume 40, Issue 5
Proceedings of the 2006 ASPLOS Conference
December 2006
425 pages
ISSN:0163-5980
DOI:10.1145/1168917
Issue’s Table of Contents
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
ACM SIGARCH Computer Architecture News Volume 34, Issue 5
Proceedings of the 2006 ASPLOS Conference
December 2006
425 pages
ISSN:0163-5964
DOI:10.1145/1168919
Issue’s Table of Contents

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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 October 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ASPLOS06

Sponsor:

ASPLOS06: Architectural Support for Programming Languages and Operating Systems

October 21 - 25, 2006

California, San Jose, USA

Acceptance Rates

ASPLOS XII Paper Acceptance Rate 38 of 158 submissions, 24%;

Overall Acceptance Rate 535 of 2,713 submissions, 20%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

676
Total Citations
View Citations
2,371
Total Downloads

Downloads (Last 12 months)163
Downloads (Last 6 weeks)22

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Chen SMolu LFazlyab M(2024)Verification-Aided Learning of Neural Network Barrier Functions with Termination Guarantees2024 American Control Conference (ACC)10.23919/ACC60939.2024.10645043(3610-3617)Online publication date: 10-Jul-2024
https://doi.org/10.23919/ACC60939.2024.10645043
Mariano BWang ZPailoor SCollberg CDillig I(2024)Control-Flow Deobfuscation using Trace-Informed Compositional Program SynthesisProceedings of the ACM on Programming Languages10.1145/36897898:OOPSLA2(2211-2241)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689789
Craaijo JVerbeek FRavindran B(2024)libLISA: Instruction Discovery and Analysis on x86-64Proceedings of the ACM on Programming Languages10.1145/36897238:OOPSLA2(333-361)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689723
Plocharski ASwidzinski JPorter-Sobieraj JMusialski P(2024)FaçAID: A Transformer Model for Neuro-Symbolic Facade ReconstructionSIGGRAPH Asia 2024 Conference Papers10.1145/3680528.3687657(1-11)Online publication date: 3-Dec-2024
https://dl.acm.org/doi/10.1145/3680528.3687657
Kura SUnno H(2024)Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type SystemProceedings of the ACM on Programming Languages10.1145/36746628:ICFP(973-1002)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674662
Wen HLiu HSong JChen YGuo WFeng YLuo BLiao XXu JKirda ELie D(2024)FORAY: Towards Effective Attack Synthesis against Deep Logical Vulnerabilities in DeFi ProtocolsProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security10.1145/3658644.3690293(1001-1015)Online publication date: 2-Dec-2024
https://dl.acm.org/doi/10.1145/3658644.3690293
Lubin JFerguson JYe KYim JChasins S(2024)Equivalence by Canonicalization for Synthesis-Backed RefactoringProceedings of the ACM on Programming Languages10.1145/36564538:PLDI(1879-1904)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656453
Wang ZPailoor SPrakash AWang YDillig I(2024)From Batch to Stream: Automatic Generation of Online AlgorithmsProceedings of the ACM on Programming Languages10.1145/36564188:PLDI(1014-1039)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656418
Ji RZhao YPolikarpova NXiong YHu Z(2024)Superfusion: Eliminating Intermediate Data Structures via Inductive SynthesisProceedings of the ACM on Programming Languages10.1145/36564158:PLDI(939-964)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656415
Zhao HQi NRen MZeng XZeng ZYang ZDe V(2024)Neural Barrier Certificates Synthesis of NN-Controlled Continuous Systems via Counterexample-Guided LearningProceedings of the 61st ACM/IEEE Design Automation Conference10.1145/3649329.3658256(1-6)Online publication date: 23-Jun-2024
https://dl.acm.org/doi/10.1145/3649329.3658256
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.

Media

Figures

Other

Tables

View Table of Contents