A vision for online verification-validation
Pages 190 - 201
Abstract
Today's programmers face a false choice between creating software that is extensible and software that is correct. Specifically, dynamic languages permit software that is richly extensible (via dynamic code loading, dynamic object extension, and various forms of reflection), and today's programmers exploit this flexibility to "bring their own language features" to enrich extensible languages (e.g., by using common JavaScript libraries). Meanwhile, such library-based language extensions generally lack enforcement of their abstractions, leading to programming errors that are complex to avoid and predict.
To offer verification for this extensible world, we propose online verification-validation (OVV), which consists of language and VM design that enables a "phaseless" approach to program analysis, in contrast to the standard static-dynamic phase distinction. Phaseless analysis freely interposes abstract interpretation with concrete execution, allowing analyses to use dynamic (concrete) information to prove universal (abstract) properties about future execution.
In this paper, we present a conceptual overview of OVV through a motivating example program that uses a hypothetical database library. We present a generic semantics for OVV, and an extension to this semantics that offers a simple gradual type system for the database library primitives. The result of instantiating this gradual type system in an OVV setting is a checker that can progressively type successive continuations of the program until a continuation is fully verified. To evaluate the proposed vision of OVV for this example, we implement the VM semantics (in Rust), and show that this design permits progressive typing in this manner.
References
[1]
Jong-hoon (David) An, Avik Chaudhuri, and Jeffrey S. Foster. Static typing for Ruby on Rails. In Automated Software Engineering (ASE), 2009.
[2]
Esben Andreasen and Anders Møller. Determinacy in static analysis for jQuery. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2014.
[3]
Kenichi Asai. Reflection in direct style. In Generative Programming and Component Engineering (GPCE), 2011.
[4]
Kenichi Asai, Satoshi Matsuoka, and Akinori Yonezawa. Duplication and partial evaluation for a better understanding of reflective languages. Lisp and Symbolic Computation, 9(2-3), 1996.
[5]
SungGyeong Bae, Hyunghun Cho, Inho Lim, and Sukyoung Ryu. SAFEWAPI: web API misuse detector for web applications. In Foundations of Software Engineering (FSE), 2014.
[6]
Nels E. Beckman, Aditya V. Nori, Sriram K. Rajamani, Robert J. Simmons, Sai Deep Tetali, and Aditya V. Thakur. Proofs from tests. IEEE Transactions on Software Engineering, 2010.
[7]
Pramod Bhatotia, Alexander Wieder, Rodrigo Rodrigues, Umut A. Acar, and Rafael Pasquin. Incoop: MapReduce for incremental computations. In Cloud Computing (SoCC), 2011.
[8]
Pramod Bhatotia, Pedro Fonseca, Umut A. Acar, Björn B. Brandenburg, and Rodrigo Rodrigues. iThreads: A threading library for parallel incremental computation. In Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2015.
[9]
Eric Bodden, Andreas Sewe, Jan Sinschek, Hela Oueslati, and Mira Mezini. Taming reflection: Aiding static analysis in the presence of reflection and custom class loaders. In International Conference on Software Engineering (ICSE), 2011.
[10]
Adam Chlipala, Leaf Petersen, and Robert Harper. Strict bidirectional type checking. 2005.
[11]
Ravi Chugh, David Herman, and Ranjit Jhala. Dependent types for JavaScript. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2012.
[12]
Ravi Chugh, Patrick Maxim Rondon, and Ranjit Jhala. Nested refinements: a logic for duck typing. In Principles of Programming Languages (POPL), 2012.
[13]
Olivier Danvy and Karoline Malmkjær. Intensions and extensions in a reflective tower. In LISP and Functional Programming, 1988.
[14]
Jim des Rivières and Brian Cantwell Smith. The implementation of procedurally reflective languages. In LISP and Functional Programming, 1984.
[15]
Bruno Dufour, Barbara G. Ryder, and Gary Sevitsky. Blended analysis for performance understanding of framework-based applications. In Software Testing and Analysis (ISSTA), 2007.
[16]
Joshua Dunfield and Neelakantan R. Krishnaswami. Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types. CoRR, abs/1601.05106, 2016.
[17]
Sebastian Erdweg, Oliver Bracevac, Edlira Kuci, Matthias Krebs, and Mira Mezini. A co-contextual formulation of type rules and its application to incremental type checking. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2015.
[18]
Jean-Christophe Filliˆatre and Sylvain Conchon. Type-safe modular hash-consing. In Proceedings of the 2006 Workshop on ML. ACM, 2006.
[19]
Daniel P. Friedman and Mitchell Wand. Reification: Reflection without metaphysics. In LISP and Functional Programming, 1984.
[20]
Michael Furr, Jong hoon (David) An, and Jeffrey S. Foster. Profile-guided static typing for dynamic scripting languages. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2009.
[21]
Philippa Gardner, Sergio Maffeis, and Gareth David Smith. Towards a program logic for JavaScript. In Principles of Programming Languages (POPL), 2012.
[22]
Patrice Godefroid, Nils Klarlund, and Koushik Sen. DART: Directed automated random testing. In Programming Language Design and Implementation (PLDI), 2005.
[23]
Neville Grech, Julian Rathke, and Bernd Fischer. Preemptive type checking in dynamically typed languages. In Theoretical Aspects of Computing - ICTAC, 2013.
[24]
Philip J. Guo and Dawson Engler. Using automatic persistent memoization to facilitate data analysis scripting. In Software Testing and Analysis (ISSTA), 2011.
[25]
Matthew A. Hammer, Yit Phang Khoo, Michael Hicks, and Jeffrey S. Foster. Adapton: Composable, demand-driven incremental computation. In Programming Language Design and Implementation (PLDI), 2014.
[26]
Matthew A. Hammer, Joshua Dunfield, Kyle Headley, Nicholas Labich, Jeffrey S. Foster, Michael W. Hicks, and David Van Horn. Incremental computation with names. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2015.
[27]
Simon Holm Jensen, Anders Møller, and Peter Thiemann. Type analysis for JavaScript. In Static Analysis (SAS), 2009.
[28]
Vineeth Kashyap, Kyle Dewey, Ethan A. Kuefner, John Wagner, Kevin Gibbons, John Sarracino, Ben Wiedermann, and Ben Hardekopf. JSAI: a static analysis platform for JavaScript. In Foundations of Software Engineering (FSE), 2014.
[29]
Benjamin S. Lerner, Liam Elberty, Jincheng Li, and Shriram Krishnamurthi. Combining form and function: Static types for jQuery programs. In Object-Oriented Programming (ECOOP), 2013.
[30]
Paul Blain Levy. Call-by-push-value: A subsuming paradigm. In Typed Lambda Calculi and Applications (TLCA), 1999.
[31]
Paul Blain Levy. Call-by-push-value: A Functional/imperative Synthesis, volume 2. 2003.
[32]
Changhee Park and Sukyoung Ryu. Scalable and precise static analysis of JavaScript applications via loop-sensitivity. In Object-Oriented Programming (ECOOP), 2015.
[33]
William Pugh. Incremental Computation via Function Caching. PhD thesis, Cornell University, 1988.
[34]
William Pugh and Tim Teitelbaum. Incremental computation via function caching. In Principles of Programming Languages (POPL), 1989.
[35]
Max Schäfer, Manu Sridharan, Julian Dolby, and Frank Tip. Dynamic determinacy analysis. In Programming Language Design and Implementation (PLDI), 2013.
[36]
Jeremy G. Siek and Walid Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, 2006.
[37]
Jeremy G. Siek and Walid Taha. Gradual typing for objects. In Object-Oriented Programming (ECOOP), 2007.
[38]
Brian Cantwell Smith. Reflection and semantics in Lisp. In Principles of Programming Languages (POPL), 1984.
[39]
Manu Sridharan, Julian Dolby, Satish Chandra, Max Schäfer, and Frank Tip. Correlation tracking for points-to analysis of JavaScript. In Object-Oriented Programming (ECOOP), 2012.
[40]
Mitchell Wand and Daniel P. Friedman. The mystery of the tower revealed: A nonreflective description of the reflective tower. Lisp and Symbolic Computation, 1(1), 1988.
[41]
Shiyi Wei and Barbara G. Ryder. Practical blended taint analysis for JavaScript. In Software Testing and Analysis (ISSTA), 2013.
[42]
Introduction Overview OVV Machine Semantics Gradual Typing for Simple Databases Discussion Related Work Conclusion
Recommendations
A vision for online verification-validation
GPCE '16Today's programmers face a false choice between creating software that is extensible and software that is correct. Specifically, dynamic languages permit software that is richly extensible (via dynamic code loading, dynamic object extension, and ...
Explicitly heterogeneous metaprogramming with MetaHaskell
ICFP '12: Proceedings of the 17th ACM SIGPLAN international conference on Functional programmingLanguages with support for metaprogramming, like MetaOCaml, offer a principled approach to code generation by guaranteeing that well-typed metaprograms produce well-typed programs. However, many problem domains where metaprogramming can fruitfully be ...
Explicitly heterogeneous metaprogramming with MetaHaskell
ICFP '12Languages with support for metaprogramming, like MetaOCaml, offer a principled approach to code generation by guaranteeing that well-typed metaprograms produce well-typed programs. However, many problem domains where metaprogramming can fruitfully be ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2016
212 pages
March 2017212 pages
Copyright © 2016 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 2016
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
Conference
GPCE '16
Sponsor:
GPCE '16: Generative Programming: Concepts and Experiences
October 31 - November 1, 2016
Amsterdam, Netherlands
Acceptance Rates
Overall Acceptance Rate 56 of 180 submissions, 31%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 436Total Downloads
- Downloads (Last 12 months)122
- Downloads (Last 6 weeks)31
Reflects downloads up to 18 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in