Skip to main content
SpringerLink
Log in

Learning Guided Enumerative Synthesis for Superoptimization

  • Conference paper
  • First Online:
Model Checking Software (SPIN 2019)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11636))

Included in the following conference series:

Abstract

The field of program synthesis has seen substantial recent progress in new ideas, e.g., program sketching and synthesis modulo pruning, and applications, e.g., in program repair and superoptimization, which is our focus in this paper. The goal of superoptimization is to generate a program which is functionally equivalent to the given program but is optimal with respect to some desired criteria. We develop a learning-based approach to guide the exploration of the space of candidate programs to parts of the space where an optimal solution likely exists. We introduce the techniques of bulk and sequence orderings which enable this directed search. We integrate these machine learning techniques with an enumerative superoptimizer and experimentally evaluate our framework using a suite of subjects. Our findings demonstrate that machine learning techniques can play a useful role in reducing the amount of candidate program space that the enumerative search must to explore in order to find an optimal solution; for the subject programs, the reduction is up to 80% on average.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Abadi, M., et al.: TensorFlow: a system for large-scale machine learning. In: Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation, OSDI 2016, pp. 265–283. USENIX Association, Berkeley (2016). http://dl.acm.org/citation.cfm?id=3026877.3026899

  2. Alur, R., et al.: Syntax-guided synthesis. In: 2013 Formal Methods in Computer-Aided Design, pp. 1–8, October 2013. https://doi.org/10.1109/FMCAD.2013.6679385

  3. Alur, R., Radhakrishna, A., Udupa, A.: Scaling enumerative program synthesis via divide and conquer. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 319–336. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54577-5_18

    Chapter  Google Scholar 

  4. Balog, M., Gaunt, A.L., Brockschmidt, M., Nowozin, S., Tarlow, D.: DeepCoder: learning to write programs. arXiv preprint arXiv:1611.01989 (2016)

  5. Bansal, S., Aiken, A.: Automatic generation of peephole superoptimizers. In: Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS XII, pp. 394–403. ACM, New York (2006). https://doi.org/10.1145/1168857.1168906

  6. Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825–885, 1st edn (2009). https://doi.org/10.3233/978-1-58603-929-5-825

  7. Bornholt, J., Torlak, E., Grossman, D., Ceze, L.: Optimizing synthesis with metasketches. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pp. 775–788. ACM, New York (2016). https://doi.org/10.1145/2837614.2837666

  8. Bunel, R., Desmaison, A., Kumar, M.P., Torr, P.H.S., Kohli, P.: Learning to superoptimize programs. CoRR abs/1611.01787 (2016)

    Google Scholar 

  9. Cho, K., van Merrienboer, B., Bahdanau, D., Bengio, Y.: On the properties of neural machine translation: encoder-decoder approaches. CoRR abs/1409.1259 (2014). http://arxiv.org/abs/1409.1259

  10. Chollet, F.: Keras (2015). https://github.com/fchollet/keras

  11. Chung, J., Gülçehre, Ç., Cho, K., Bengio, Y.: Empirical evaluation of gated recurrent neural networks on sequence modeling. CoRR abs/1412.3555 (2014). http://arxiv.org/abs/1412.3555

  12. D’Antoni, L., Samanta, R., Singh, R.: Qlose: program repair with quantitative objectives. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 383–401. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_21

    Chapter  Google Scholar 

  13. Desai, A., et al.: Program synthesis using natural language. CoRR abs/1509.00413 (2015). http://arxiv.org/abs/1509.00413

  14. Devlin, J., Uesato, J., Bhupatiraju, S., Singh, R., Mohamed, A.R., Kohli, P.: RobustFill: neural program learning under noisy I/O. arXiv preprint arXiv:1703.07469 (2017)

  15. Elman, J.L.: Finding structure in time. Cogn. Sc. 14(2), 179–211 (1990). https://doi.org/10.1016/0364-0213(90)90002-E. http://www.sciencedirect.com/science/article/pii/036402139090002E

    Article  Google Scholar 

  16. Feser, J.K., Chaudhuri, S., Dillig, I.: Synthesizing data structure transformations from input-output examples. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, pp. 229–239. ACM, New York (2015). https://doi.org/10.1145/2737924.2737977

  17. Gao, K.: IBM pytorch-seq2seq (2017). https://github.com/IBM/pytorch-seq2seq/

  18. Granlund, T., Kenner, R.: Eliminating branches using a superoptimizer and the GNU C compiler. In: Proceedings of the ACM SIGPLAN 1992 Conference on Programming Language Design and Implementation, PLDI 1992, pp. 341–352. ACM, New York (1992). https://doi.org/10.1145/143095.143146

  19. Graves, A.: Generating sequences with recurrent neural networks. CoRR abs/1308.0850 (2013). http://arxiv.org/abs/1308.0850

  20. Gulwani, S.: Dimensions in program synthesis. In: Proceedings of the 12th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2010, pp. 13–24. ACM, New York (2010). https://doi.org/10.1145/1836089.1836091

  21. Gulwani, S.: Automating string processing in spreadsheets using input-output examples. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, pp. 317–330. ACM, New York (2011). https://doi.org/10.1145/1926385.1926423

  22. Gulwani, S.: Applications of program synthesis to end-user programming and intelligent tutoring systems. In: Proceedings of the Companion Publication of the 2014 Annual Conference on Genetic and Evolutionary Computation, GECCO Comp 2014, pp. 5–6. ACM, New York (2014). https://doi.org/10.1145/2598394.2598397

  23. Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Synthesis of loop-free programs. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp. 62–73. ACM, New York (2011). https://doi.org/10.1145/1993498.1993506

  24. Gulwani, S., Jojic, N.: Program verification as probabilistic inference. In: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, pp. 277–289. ACM, New York (2007). https://doi.org/10.1145/1190216.1190258

  25. Gulwani, S., Polozov, O., Singh, R.: Program synthesis. Found. Trends® Program. Lang. 4(1–2), 1–119 (2017). https://doi.org/10.1561/2500000010

    Article  Google Scholar 

  26. Jojic, V., Gulwani, S., Jojic, N.: Probabilistic inference of programs from input/output examples, April 2018

    Google Scholar 

  27. Joshi, R., Nelson, G., Randall, K.: Denali: A goal-directed superoptimizer. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, PLDI 2002, pp. 304–314. ACM, New York (2002). https://doi.org/10.1145/512529.512566

  28. Katz, G., Peled, D.: Genetic programming and model checking: synthesizing new mutual exclusion algorithms. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 33–47. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-88387-6_5

    Chapter  MATH  Google Scholar 

  29. Kuniyoshi, Y., Inaba, M., Inoue, H.: Learning by watching: extracting reusable task knowledge from visual observation of human performance. IEEE Trans. Robot. Autom. 10(6), 799–822 (1994). https://doi.org/10.1109/70.338535

    Article  Google Scholar 

  30. Lamb, A., Goyal, A., Zhang, Y., Zhang, S., Courville, A., Bengio, Y.: Professor forcing: a new algorithm for training recurrent networks. ArXiv e-prints, October 2016

    Google Scholar 

  31. Massalin, H.: Superoptimizer: a look at the smallest program. In: Proceedings of the Second International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS II, pp. 122–126. IEEE Computer Society Press, Los Alamitos (1987). https://doi.org/10.1145/36206.36194

  32. Paszke, A., et al.: Automatic differentiation in PyTorch. In: NIPS-W (2017)

    Google Scholar 

  33. Phothilimthana, P.M., Thakur, A., Bodik, R., Dhurjati, D.: Greenthumb: superoptimizer construction framework. In: Proceedings of the 25th International Conference on Compiler Construction, CC 2016, pp. 261–262. ACM, New York (2016). https://doi.org/10.1145/2892208.2892233

  34. Phothilimthana, P.M., Thakur, A., Bodik, R., Dhurjati, D.: Scaling up superoptimization. SIGPLAN Not. 51(4), 297–310 (2016). https://doi.org/10.1145/2954679.2872387

    Article  Google Scholar 

  35. Polozov, O., Gulwani, S.: FlashMeta: a framework for inductive program synthesis. In: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, pp. 107–126. ACM, New York (2015). https://doi.org/10.1145/2814270.2814310

  36. Ruck, D.W., Rogers, S.K., Kabrisky, M., Oxley, M.E., Suter, B.W.: The multilayer perceptron as an approximation to a Bayes optimal discriminant function. IEEE Trans. Neural Netw. 1(4), 296–298 (1990). https://doi.org/10.1109/72.80266

    Article  Google Scholar 

  37. Rumelhart, D.E., Hinton, G.E., Williams, R.J.: Learning representations by back-propagating errors. In: Neurocomputing: Foundations of Research, pp. 696–699. MIT Press, Cambridge (1988). http://dl.acm.org/citation.cfm?id=65669.104451

  38. Schkufza, E., Sharma, R., Aiken, A.: Stochastic superoptimization. In: Proceedings of the Eighteenth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2013, pp. 305–316. ACM, New York (2013). https://doi.org/10.1145/2451116.2451150

  39. Schkufza, E., Sharma, R., Aiken, A.: Stochastic optimization of floating-point programs with tunable precision. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, pp. 53–64. ACM, New York (2014). https://doi.org/10.1145/2594291.2594302

  40. Solar-Lezama, A., Rabbah, R., Bodík, R., Ebcioğlu, K.: Programming by sketching for bit-streaming programs. In: Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2005, pp. 281–294. ACM, New York (2005). https://doi.org/10.1145/1065010.1065045

  41. Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS XII, pp. 404–415. ACM, New York (2006). https://doi.org/10.1145/1168857.1168907

  42. Sutskever, I., Vinyals, O., Le, Q.V.: Sequence to sequence learning with neural networks. CoRR abs/1409.3215 (2014). http://arxiv.org/abs/1409.3215

  43. Udupa, A., Raghavan, A., Deshmukh, J.V., Mador-Haim, S., Martin, M.M., Alur, R.: TRANSIT: specifying protocols with concolic snippets. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, pp. 287–296. ACM, New York (2013). https://doi.org/10.1145/2491956.2462174

  44. Ruck, D.W., Rogers, S., Kabrisky, M.: Feature selection using a multilayer perceptron 2, July 1993

    Google Scholar 

  45. Weimer, W., Nguyen, T., Le Goues, C., Forrest, S.: Automatically finding patches using genetic programming. In: Proceedings of the 31st International Conference on Software Engineering, ICSE 2009, pp. 364–374. IEEE Computer Society, Washington, DC (2009). https://doi.org/10.1109/ICSE.2009.5070536

  46. Williams, R.J.: Simple statistical gradient-following algorithms for connectionist reinforcement learning. Mach. Learn. 8(3), 229–256 (1992). https://doi.org/10.1007/BF00992696

    Article  MathSciNet  MATH  Google Scholar 

  47. Zheng, S., et al.: Conditional random fields as recurrent neural networks. CoRR abs/1502.03240 (2015). http://arxiv.org/abs/1502.03240

  48. Zohar, A., Wolf, L.: Automatic program synthesis of long programs with a learned garbage collector. CoRR abs/1809.04682 (2018). http://arxiv.org/abs/1809.04682

Download references

Acknowledgments

This work started as a class project for Program Synthesis taught by Dr. Keshav Pingali at UT Austin. The authors are grateful for his valuable input.

This research was partially supported by the US National Science Foundation under Grant Nos. CCF-1704790 and CCF-1718903.

Author information

Authors and Affiliations

  1. University of Texas, Austin, USA

    Shikhar Singh, Mengshi Zhang & Sarfraz Khurshid

Authors
  1. Shikhar Singh
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mengshi Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sarfraz Khurshid
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Shikhar Singh .

Editor information

Editors and Affiliations

  1. Avast Software, Prague, Czech Republic

    Fabrizio Biondi

  2. Université Catholique de Louvain, Louvain-la-Neuve, Belgium

    Thomas Given-Wilson

  3. Université Catholique de Louvain, Louvain-la-Neuve, Belgium

    Axel Legay

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Singh, S., Zhang, M., Khurshid, S. (2019). Learning Guided Enumerative Synthesis for Superoptimization. In: Biondi, F., Given-Wilson, T., Legay, A. (eds) Model Checking Software. SPIN 2019. Lecture Notes in Computer Science(), vol 11636. Springer, Cham. https://doi.org/10.1007/978-3-030-30923-7_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30923-7_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30922-0

  • Online ISBN: 978-3-030-30923-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation