nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Fixing Code that Explodes Under Symbolic Evaluation

verfasst von : Sorawee Porncharoenwase, James Bornholt, Emina Torlak

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Effective symbolic evaluation is key to building scalable verification and synthesis tools based on SMT solving. These tools use symbolic evaluators to reduce the semantics of all paths through a finite program to logical constraints, discharged with an SMT solver. Using an evaluator effectively requires tool developers to be able to identify and repair performance bottlenecks in code under all-path evaluation, a difficult task, even for experts. This paper presents a new method for repairing such bottlenecks automatically. The key idea is to formulate the symbolic performance repair problem as combinatorial search through a space of semantics-preserving transformations, or repairs, to find an equivalent program with minimal cost under symbolic evaluation. The key to realizing this idea is (1) defining a small set of generic repairs that can be combined to fix common bottlenecks, and (2) searching for combinations of these repairs to find good solutions quickly and best ones eventually. Our technique, SymFix, contributes repairs based on deforestation and symbolic reflection, and an efficient algorithm that uses symbolic profiling to guide the search for fixes. To evaluate SymFix, we implement it for the Rosette solver-aided language and symbolic evaluator. Applying SymFix to 18 published verification and synthesis tools built in Rosette, we find that it automatically improves the performance of 12 tools by a factor of 1.1 \(\times \)–91.7 \(\times \), and 4 of these fixes match or outperform expert-written repairs. SymFix also finds 5 fixes that were missed by experts.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel : Backward Context-Sensitive Flow Reconstruction of Taint Analysis Results

Nächstes Kapitel The Correctness of a Code Generator for a Functional Language

The RISC-V Instruction Set Manual, Volume II: Privileged Architecture. RISC-V Foundation, June 2019

Amazon Web Services: Quivela (2018). https://github.com/awslabs/quivela

Becker, N., Müller, P., Summers, A.J.: The axiom profiler: understanding and debugging SMT quantifier instantiations. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 99–116. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17462-0_6CrossRef

Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-49059-0_14CrossRef

Bornholt, J., Kaufmann, A., Li, J., Krishnamurthy, A., Torlak, E., Wang, X.: Specifying and checking file system crash-consistency models. In: Proceedings of the 21st International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), Atlanta, GA, USA, pp. 83–98, April 2016

Bornholt, J., Torlak, E.: Synthesizing memory models from framework sketches and litmus tests. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Barcelona, Spain, pp. 467–481, June 2017

Bornholt, J., Torlak, E.: Finding code that explodes under symbolic evaluation. Proc. ACM Program. Lang. (OOPSLA) 2, 149:1–149:26 (2018)

Borning, A.: Wallingford: toward a constraint reactive programming language. In: Proceedings of the Constrained and Reactive Objects Workshop (CROW), Málaga, Spain, March 2016

Bucur, S., Kinder, J., Candea, G.: Prototyping symbolic execution engines for interpreted languages. In: Proceedings of the 19th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), Salt Lake City, UT, USA , pp. 239–254, March 2014

10.

Butler, E., Torlak, E., Popović, Z.: Synthesizing interpretable strategies for solving puzzle games. In: Proceedings of the 12th International Conference on the Foundations of Digital Games (FDG), No. 10, Hyannis, MA, USA, August 2017

11.

Cadar, C.: Targeted program transformations for symbolic execution. In: Proceedings of the 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), Bergamo, Italy, pp. 906–909, August 2015

12.

Chandra, K., Bodik, R.: Bonsai: synthesis-based reasoning for type systems. Proc. ACM Program. Lang. 2(POPL), 62:1–62:34 (2018)CrossRef

13.

Chipounov, V., Kuznetsov, V., Candea, G.: S2E: a platform for in-vivo multi-path analysis of software systems. In: Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 265–278 (2011)

14.

Chu, S., Wang, C., Weitz, K., Cheung, A.: Cosette: an automated prover for SQL. In: Proceedings of the 8th Biennial Conference on Innovative Data Systems (CIDR), Chaminade, CA, USA, January 2017

15.

Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)MATH

16.

de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24CrossRef

17.

Dershowitz, N., Jouannaud, J.: Rewrite systems. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 243–320 (1990)

18.

Flatt, M.: PLT: Reference: Racket. Technical report, PLT-TR-2010-1, PLT Design Inc. (2010)

19.

Fleming, M.: A thorough introduction to eBPF, December 2017. https://lwn.net/Articles/740157/

20.

Gal, A., et al.: Trace-based just-in-time type specialization for dynamic languages. In: Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 465–478, June 2009

21.

Galois Inc: Crucible (2018). https://github.com/GaloisInc/crucible

22.

Gill, A.J., Jones, S.L.P.: Cheap deforestation in practice: an optimizer for Haskell. In: IFIP Congress (1994)

23.

Gupta, R., Mehofer, E., Zhang, Y.: Profile guided compiler optimizations (chap. 4). In: The Compiler Design Handbook: Optimizations and Machine Code Generation. CRC Press, September 2002

24.

Intel Corporation: Intel 64 and IA-32 Architectures Software Developer’s Manual. Intel Corporation (2015). Revision 53

25.

Kazerounian, M., Vazou, N., Bourgerie, A., Foster, J.S., Torlak, E.: Refinement types for ruby. In: Dillig, I., Palsberg, J., et al. (eds.) Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 10747, pp. 269–290. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-73721-8_13CrossRef

26.

King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)MathSciNetCrossRef

27.

Kuznetsov, V., Kinder, J., Bucur, S., Candea, G.: Efficient state merging in symbolic execution. In: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Beijing, China, pp. 89–98, June 2012

28.

Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO), Palo Alto, California, March 2004

29.

Nelson, L., Bornholt, J., Gu, R., Baumann, A., Torlak, E., Wang, X.: Scaling symbolic evaluation for automated verification of systems code with Serval. In: Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP), pp. 225–242 (2019)

30.

Nelson, L., et al.: Hyperkernel: push-button verification of an OS kernel. In: Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP), pp. 252–269 (2017)

31.

Newcomb, J.L., Bodik, R.: Using human-in-the-loop synthesis to author functional reactive programs (2019)

32.

Paleczny, M., Vick, C., Click, C.: The Java HotSpot server compiler. In: Proceedings of the 2001 Symposium on Java Virtual Machine Research and Technology (JVM), Monterey, CA, USA, April 2001

33.

Pernsteiner, S., Loncaric, C., Torlak, E., Tatlock, Z., Wang, X., Ernst, M.D., Jacky, J.: Investigating safety of a radiotherapy machine using system models with pluggable checkers. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 23–41. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_2CrossRef

34.

Pettis, K., Hansen, R.C.: Profile guided code positioning. In: Proceedings of the 11th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), White Plains, NY, USA, pp. 16–27, June 1990

35.

Phothilimthana, P.M., et al.: Swizzle inventor: data movement synthesis for GPU kernels. In: Proceedings of the 24th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp. 65–78 (2019)

36.

Phothilimthana, P.M., Thakur, A., Bodik, R., Dhurjati, D.: Scaling up superoptimization. In: Proceedings of the 21st International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), Atlanta, GA, USA, pp. 297–310, April 2016

37.

Racket: The Racket Programming Language (2017). https://racket-lang.org

38.

S2E: S2E: exponential analysis speedup with state merging (2019). http://s2e.systems/docs/StateMerging.html

39.

Sen, K., Kalasapur, S., Brutch, T., Gibbs, S.: Jalangi: a selective record-replay and dynamic analysis framework for JavaScript. In: Proceedings of the 9th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), Saint Petersburg, Russian Federation, pp. 488–498, August 2013

40.

Sharma, R., Schkufza, E., Churchill, B., Aiken, A.: Conditionally correct superoptimization. In: Proceedings of the 30th ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Pittsburgh, PA, USA, pp. 147–162, October 2015

41.

Sigurbjarnarson, H., Nelson, L., Castro-Karney, B., Bornholt, J., Torlak, E., Wang, X.: Nickel: a framework for design and verification of information flow control systems. In: Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI), pp. 287–305 (2018)

42.

St-Amour, V., Tobin-Hochstadt, S., Felleisen, M.: Optimization coaching: optimizers learn to communicate with programmers. In: Proceedings of the 27th ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Tuscon, AZ, USA, pp. 163–178, October 2012

43.

Torlak, E.: Rosette (2018). http://github.com/emina/rosette

44.

Torlak, E.: The Rosette guide: symbolic reflection (2019). https://docs.racket-lang.org/rosette-guide/ch_symbolic-reflection.html

45.

Torlak, E., Bodik, R.: Growing solver-aided languages with Rosette. In: Proceedings of the 2013 ACM Symposium on New Ideas in Programming and Reflections on Software (Onward!), Indianapolis, IN, USA, pp. 135–152, October 2013

46.

Torlak, E., Bodik, R.: A lightweight symbolic virtual machine for solver-aided host languages. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Edinburgh, United Kingdom, pp. 530–541, June 2014

47.

Uhler, R., Dave, N.: Smten with satisfiability-based search. In: Proceedings of the 29th ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Portland, OR, USA, pp. 157–176, October 2014

48.

Wadler, P.: Deforestation: transforming programs to eliminate trees. In: Ganzinger, H. (ed.) ESOP 1988. LNCS, vol. 300, pp. 344–358. Springer, Heidelberg (1988). https://doi.org/10.1007/3-540-19027-9_23 CrossRef

49.

Wagner, J., Kuznetsov, V., Candea, G.: -OVERIFY: optimizing programs for fast verification. In: Proceedings of the 14th Workshop on Hot Topics in Operating Systems (HotOS), Santa Ana Pueblo, NM, USA, May 2013

50.

Weitz, K., Woos, D., Torlak, E., Ernst, M.D., Krishnamurthy, A., Tatlock, Z.: Scalable verification of border gateway protocol configurations with an SMT solver. In: Proceedings of the 31st ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Amsterdam, The Netherlands, pp. 765–780, October 2016

51.

Willsey, M., Ceze, L., Strauss, K.: Puddle: an operating system for reliable, high-level programming of digital microfluidic devices. In: Proceedings of the 23rd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), Wild and Crazy Ideas Session, Williamsburg, VA, USA, March 2018

Titel: Fixing Code that Explodes Under Symbolic Evaluation
verfasst von: Sorawee Porncharoenwase
James Bornholt
Emina Torlak
Verlag: Springer International Publishing
Buch: Verification, Model Checking, and Abstract Interpretation
Print ISBN: 978-3-030-39321-2

Electronic ISBN: 978-3-030-39322-9

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-39322-9_3

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"