Document Open Access Logo

Domain-Specific Symbolic Compilation

Authors Rastislav Bodík, Kartik Chandra, Phitchaya Mangpo Phothilimthana, Nathaniel Yazdani

PDF
Thumbnail PDF

File

LIPIcs.SNAPL.2017.2.pdf
  • Filesize: 1.99 MB
  • 17 pages

Document Identifiers

Author Details

Rastislav Bodík
Kartik Chandra
Phitchaya Mangpo Phothilimthana
Nathaniel Yazdani

Cite As Get BibTex

Rastislav Bodík, Kartik Chandra, Phitchaya Mangpo Phothilimthana, and Nathaniel Yazdani. Domain-Specific Symbolic Compilation. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 2:1-2:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.SNAPL.2017.2

Abstract

A symbolic compiler translates a program to symbolic constraints, automatically reducing model checking and synthesis to constraint solving. We show that new applications of constraint solving require domain-specific encodings that yield the required orders of magnitude improvements in solver efficiency. Unfortunately, these encodings cannot be obtained with today's symbolic compilation. 

We introduce symbolic languages that encapsulate domain-specific encodings under abstractions that behave as their non-symbolic counterparts: client code using the abstractions can be tested and debugged on concrete inputs. When client code is symbolically compiled, the resulting constraints use domain-specific encodings. 

We demonstrate the idea on the first fully symbolic checker of type systems; a program partitioner; and a parallelizer of tree computations. In each of these case studies, symbolic languages improved on classical symbolic compilers by orders of magnitude.

Subject Classification

Keywords
  • Symbolic evaluation
  • program synthesis
  • DSLs

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Nada Amin and Ross Tate. Java and scala’s type systems are unsound: the existential crisis of null pointers. In OOPSLA, 2016. Google Scholar
  2. James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze. Optimizing synthesis with metasketches. In POPL, 2016. Google Scholar
  3. Edmund Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ansi-c programs. In Kurt Jensen and Andreas Podelski, editors, Tools and Algorithms for the Construction and Analysis of Systems: 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004. Proceedings, pages 168-176, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. Google Scholar
  4. Robert Glück. Is there a fourth futamura projection? In Proceedings of the 2009 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation, PEPM 2009, Savannah, GA, USA, January 19-20, 2009, pages 51-60, 2009. Google Scholar
  5. GreenArrays. Product Brief: GreenArrays Architecture, 2010. URL: http://www.greenarraychips.com/home/documents/greg/PB002-100822-GA-Arch.pdf.
  6. Sumit Gulwani, Susmit Jha, Ashish Tiwari, and Ramarathnam Venkatesan. Synthesis of loop-free programs. In PLDI, 2011. Google Scholar
  7. Jad Hamza, Barbara Jobstmann, and Viktor Kuncak. Synthesis for regular specifications over unbounded domains. In FMCAD, 2010. Google Scholar
  8. Lavanya Jose, Lisa Yan, George Varghese, and Nick McKeown. Compiling packet programs to reconfigurable switches. In NSDI, 2015. Google Scholar
  9. James C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385-394, July 1976. Google Scholar
  10. Krzysztof Kuchcinski. Constraints-driven scheduling and resource assignment. ACM Trans. Des. Autom. Electron. Syst., 8(3):355-383, July 2003. Google Scholar
  11. Leo Meyerovich, Matthew Torok, Eric Atkinson, and Rastislav Bodik. Parallel schedule synthesis for attribute grammars. In PPoPP, 2013. Google Scholar
  12. Leo A. Meyerovich and Rastislav Bodik. Fast and parallel webpage layout. In WWW, 2010. Google Scholar
  13. Tony Nowatzki, Michael Sartin-Tarm, Lorenzo De Carli, Karthikeyan Sankaralingam, Cristian Estan, and Behnam Robatmili. A general constraint-centric scheduling framework for spatial architectures. In PLDI, 2013. Google Scholar
  14. Jens Palsberg and Mayur Naik. ILP-based Resource-aware Compilation, 2004. Google Scholar
  15. Phitchaya Mangpo Phothilimthana, Tikhon Jelvis, Rohin Shah, Nishant Totla, Sarah Chasins, and Rastislav Bodik. Chlorophyll: Synthesis-aided compiler for low-power spatial architectures. In PLDI, 2014. Google Scholar
  16. Phitchaya Mangpo Phothilimthana, Michael Schuldt, and Rastislav Bodik. Compiling a gesture recognition application for a low-power spatial architecture. In Proceedings of Conference on Languages, Compilers, Tools, and Theory for Embedded Systems, 2016. Google Scholar
  17. Sketch: a synthesizer language and compiler. URL: http://bitbucket.org/gatoatigrado/sketch-frontend.
  18. Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. Combinatorial sketching for finite programs. In ASPLOS, New York, NY, USA, 2006. Google Scholar
  19. Emina Torlak and Rastislav Bodik. Growing solver-aided languages with Rosette. In Onward!, 2013. Google Scholar
  20. Emina Torlak and Rastislav Bodik. A lightweight symbolic virtual machine for solver-aided host languages. In PLDI, 2014. Google Scholar
  21. Kent Wilken, Jack Liu, and Mark Heffernan. Optimal instruction scheduling using integer programming. In PLDI, 2000. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact