Cited By
View all- Bunte ODenkers Jvan Gool LVinju JVisser EWillemse TZaidman A(2024)OIL: an industrial case study in language engineering with SpoofaxSoftware and Systems Modeling10.1007/s10270-024-01185-xOnline publication date: 3-Jun-2024
Incremental type-checking for free: using scope graphs to derive incremental type-checkers
Article No.: 140, Pages 424 - 448
Abstract
Fast analysis response times in IDEs are essential for a good editor experience. Incremental type-checking can provide that in a scalable fashion. However, existing techniques are not reusable between languages. Moreover, mutual and dynamic dependencies preclude traditional approaches to incrementality. This makes finding automatic approaches to incremental type-checking a challenging but important open question.
In this paper, we present a technique that automatically derives incremental type-checkers from type system specifications written in the Statix meta-DSL. We use name resolution queries in scope graphs (a generic model of name binding embedded in Statix) to derive dependencies between compilation units. A novel query confirmation algorithm finds queries for which the answer changed due to an edit in the program. Only units with such queries require reanalysis. The effectiveness of this algorithm is improved by (1) splitting the type-checking task into a context-free and a context-sensitive part, and (2) reusing a generic mechanism to resolve mutual dependencies. This automatically yields incremental type-checkers for any Statix specification.
Compared to non-incremental parallel execution, we achieve speedups up to 147x on synthetic benchmarks, and up to 21x on real-world projects, with initial overheads below 10%. This suggests that our framework can provide efficient incremental type-checking to the wide range of languages supported by Statix.
Supplementary Material
This archive contains a PDF with the appendices accompanying this paper. Appendix A provides a full overview of the algorithm. Appendix B gives detailed information about the benchmarks (the commits benchmarked and the absolute runtimes).
- Download
- 1.10 MB
References
[1]
Gul A. Agha. 1990. ACTORS - a model of concurrent computation in distributed systems. MIT Press. isbn:978-0-262-01092-4
[2]
Davide Ancona. 1998. An Algebraic Framework for Separate Type-Checking. In Recent Trends in Algebraic Development Techniques, 13th International Workshop, WADT 98, Lisbon, Portugal, April 2-4, 1998, Selected Papers, José Luiz Fiadeiro (Ed.) (Lecture Notes in Computer Science, Vol. 1589). Springer, 1–15. isbn:3-540-66246-4 https://doi.org/10.1007/3-540-48483-3_1
[3]
Davide Ancona, Giovanni Lagorio, and Elena Zucca. 2002. True separate compilation of Java classes. In Proceedings of the 4th international ACM SIGPLAN conference on Principles and practice of declarative programming, October 6-8, 2002, Pittsburgh, PA, USA (Affiliated with PLI 2002). ACM, 189–200. https://doi.org/10.1145/571157.571177
[4]
Davide Ancona and Elena Zucca. 2002. A calculus of module systems. Journal of Functional Programming, 12, 2 (2002), 91–132. https://doi.org/10.1017/S0956796801004257
[5]
Steven Arzt and Eric Bodden. 2014. Reviser: efficiently updating IDE-/IFDS-based data-flow analyses in response to incremental program changes. In 36th International Conference on Software Engineering, ICSE ’14, Hyderabad, India - May 31 - June 07, 2014, Pankaj Jalote, Lionel C. Briand, and André van der Hoek (Eds.). ACM, 288–298. isbn:978-1-4503-2756-5 https://doi.org/10.1145/2568225.2568243
[6]
Janusz A. Brzozowski. 1964. Derivatives of Regular Expressions. J. ACM, 11, 4 (1964), 481–494.
[7]
Matteo Busi, Pierpaolo Degano, and Letterio Galletta. 2019. Using Standard Typing Algorithms Incrementally. In NASA Formal Methods - 11th International Symposium, NFM 2019, Houston, TX, USA, May 7-9, 2019, Proceedings, Julia M. Badger and Kristin Yvonne Rozier (Eds.) (Lecture Notes in Computer Science, Vol. 11460). Springer, 106–122. isbn:978-3-030-20652-9 https://doi.org/10.1007/978-3-030-20652-9_7
[8]
Luca Cardelli. 1997. Program Fragments, Linking, and Modularization. In Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 266–277. https://doi.org/10.1145/263699.263735
[9]
Avik Chaudhuri, Panagiotis Vekris, Sam Goldman, Marshall Roch, and Gabriel Levi. 2017. Fast and precise type checking for JavaScript. Proceedings of the ACM on Programming Languages, 1, OOPSLA (2017), https://doi.org/10.1145/3133872
[10]
Alan J. Demers, Thomas W. Reps, and Tim Teitelbaum. 1981. Incremental Evaluation for Attribute Grammars with Application to Syntax-Directed Editors. In Proceedings of the 8th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 105–116. https://doi.org/10.1145/567532.567544
[11]
Sophia Drossopoulou, Susan Eisenbach, and David Wragg. 1999. A Fragment Calculus – Towards a Model of Separate Compilation, Linking and Binary Compatibility. In Proceedings, 14th Annual IEEE Symposium on Logic in Computer Science, 2-5 July, 1999, Trento, Italy. IEEE Computer Society, 147–156. https://doi.org/10.1109/LICS.1999.782606
[12]
Eclipse. 2021. JDT Core Component. https://www.eclipse.org/jdt/core/
[13]
Martin Elsman. 2008. A Framework for Cut-Off Incremental Recompilation and Inter-Module Optimization. IT University of Copenhagen, Copenhagen. 11. https://elsman.com/pdf/sepcomp_tr.pdf
[14]
Sebastian Erdweg, Oliver Bracevac, Edlira Kuci, Matthias Krebs, and Mira Mezini. 2015. A co-contextual formulation of type rules and its application to incremental type checking. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, Jonathan Aldrich and Patrick Eugster (Eds.). ACM, 880–897. isbn:978-1-4503-3689-5 https://doi.org/10.1145/2814270.2814277
[15]
Sterling Greene. 2015. Introducing Incremental Build Support. https://blog.gradle.org/introducing-incremental-build-support
[16]
Danny M. Groenewegen, Zef Hemel, Lennart C. L. Kats, and Eelco Visser. 2008. WebDSL: a domain-specific language for dynamic web applications. In Companion to the 23rd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2008, October 19-13, 2007, Nashville, TN, USA, Gail E. Harris (Ed.). ACM, 779–780. isbn:978-1-60558-220-7 https://doi.org/10.1145/1449814.1449858
[17]
Martin Grohe and Pascal Schweitzer. 2020. The graph isomorphism problem. Commun. ACM, 63, 11 (2020), 10, 128–134. https://doi.org/10.1145/3372123
[18]
Matthew A. Hammer, Yit Phang Khoo, Michael Hicks, and Jeffrey S. Foster. 2014. Adapton: composable, demand-driven incremental computation. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, Edinburgh, United Kingdom - June 09 - 11, 2014, Michael F. P. O’Boyle and Keshav Pingali (Eds.). ACM, 18. isbn:978-1-4503-2784-8 https://doi.org/10.1145/2594291.2594324
[19]
Lennart C. L. Kats and Eelco Visser. 2010. The Spoofax language workbench: rules for declarative specification of languages and IDEs. In Proceedings of the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2010, William R. Cook, Siobhán Clarke, and Martin C. Rinard (Eds.). ACM, Reno/Tahoe, Nevada. 444–463. isbn:978-1-4503-0203-6 https://doi.org/10.1145/1869459.1869497
[20]
Gabriël Konat, Sebastian Erdweg, and Eelco Visser. 2018. Scalable incremental building with dynamic task dependencies. In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, Marianne Huchard, Christian Kästner, and Gordon Fraser (Eds.). ACM, 76–86. https://doi.org/10.1145/3238147.3238196
[21]
Edlira Kuci, Sebastian Erdweg, and Mira Mezini. 2015. Toward incremental type checking for Java. In Companion Proceedings of the 2015 ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity, Jonathan Aldrich and Patrick Eugster (Eds.). ACM, 46–47. isbn:978-1-4503-3722-9 https://doi.org/10.1145/2814189.2817272
[22]
Xavier Leroy. 1994. Manifest Types, Modules, and Separate Compilation. In Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 109–122. https://doi.org/10.1145/174675.176926
[23]
Elena Machkasova and Franklyn A. Turbak. 2000. A Calculus for Link-Time Compilation. In Programming Languages and Systems, 9th European Symposium on Programming, ESOP 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, Proceedings, Gert Smolka (Ed.) (Lecture Notes in Computer Science, Vol. 1782). Springer, 260–274. isbn:3-540-67262-1 https://doi.org/10.1007/3-540-46425-5_17
[24]
Lambert G. L. T. Meertens. 1983. Incremental Polymorphic Type Checking in B. In Proceedings of the 10th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. 265–275. https://doi.org/10.1145/567067.567092
[25]
Phil Misteli. 2021. Renaming for Everyone: Language-parametric Renaming in Spoofax. Master’s thesis. Delft University of Technology. http://resolver.tudelft.nl/uuid:60f5710d-445d-4583-957c-79d6afa45be5 Available at
[26]
Pierre Néron, Andrew P. Tolmach, Eelco Visser, and Guido Wachsmuth. 2015. A Theory of Name Resolution. In Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, Jan Vitek (Ed.) (Lecture Notes in Computer Science, Vol. 9032). Springer, 205–231. isbn:978-3-662-46668-1 https://doi.org/10.1007/978-3-662-46669-8_9
[27]
OpenJDK. 2021. Java Microbenchmark Harness (JMH). https://openjdk.java.net/projects/code-tools/jmh/
[28]
André Pacak, Sebastian Erdweg, and Tamás Szabó. 2020. A systematic approach to deriving incremental type checkers. Proceedings of the ACM on Programming Languages, 4, OOPSLA (2020), https://doi.org/10.1145/3428195
[29]
Daniël A. A. Pelsmaeker, Hendrik van Antwerpen, Casper Bach Poulsen, and Eelco Visser. 2022. Language-parametric static semantic code completion. Proceedings of the ACM on Programming Languages, 6, OOPSLA (2022), 1–30. https://doi.org/10.1145/3527329
[30]
Ganesan Ramalingam and Thomas W. Reps. 1993. A Categorized Bibliography on Incremental Computation. In Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 502–510. https://doi.org/10.1145/158511.158710
[31]
Arjen Rouvoet, Hendrik van Antwerpen, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser. 2020. Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specifications. Proceedings of the ACM on Programming Languages, 4, OOPSLA (2020), https://doi.org/10.1145/3428248
[32]
Leonid Ryzhyk and Mihai Budiu. 2019. Differential Datalog. http://budiu.info/work/ddlog.pdf
[33]
Zhong Shao and Andrew W. Appel. 1993. Smartest Recompilation. In Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 439–450. https://doi.org/10.1145/158511.158702
[34]
David Swasey, Tom Murphy VII, Karl Crary, and Robert Harper. 2006. A separate compilation extension to standard ML. In Proceedings of the ACM Workshop on ML, 2006, Portland, Oregon, USA, September 16, 2006, Andrew Kennedy and François Pottier (Eds.). ACM, 32–42. isbn:1-59593-483-9 https://doi.org/10.1145/1159876.1159883
[35]
Tamás Szabó, Sebastian Erdweg, and Gábor Bergmann. 2021. Incremental whole-program analysis in Datalog with lattices. In PLDI ’21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 20211, Stephen N. Freund and Eran Yahav (Eds.). ACM, 1–15. isbn:978-1-4503-8391-2 https://doi.org/10.1145/3453483.3454026
[36]
Tamás Szabó, Sebastian Erdweg, and Markus Völter. 2016. IncA: a DSL for the definition of incremental program analyses. In Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, David Lo, Sven Apel, and Sarfraz Khurshid (Eds.). ACM, 320–331. isbn:978-1-4503-3845-5 https://doi.org/10.1145/2970276.2970298
[37]
Tamás Szabó, Edlira Kuci, Matthijs Bijman, Mira Mezini, and Sebastian Erdweg. 2018. Incremental overload resolution in object-oriented programming languages. In Companion Proceedings for the ISSTA/ECOOP 2018 Workshops, ISSTA 2018, Amsterdam, Netherlands, July 16-21, 2018, Julian Dolby, William G. J. Halfond, and Ashish Mishra (Eds.). ACM, 27–33. isbn:978-1-4503-5939-9 https://doi.org/10.1145/3236454.3236485
[38]
Beatriz Sánchez, Dimitris S. Kolovos, and Richard F. Paige. 2020. To build, or not to build: ModelFlow, a build solution for MDE projects. In MoDELS ’20: ACM/IEEE 23rd International Conference on Model Driven Engineering Languages and Systems, Virtual Event, Canada, 18-23 October, 2020, Eugene Syriani, Houari A. Sahraoui, Juan de Lara, and Silvia Abrahão (Eds.). ACM, 1–11. isbn:978-1-4503-7019-6 https://doi.org/10.1145/3365438.3410942
[39]
Hendrik van Antwerpen, Casper Bach Poulsen, Arjen Rouvoet, and Eelco Visser. 2018. Scopes as types. Proceedings of the ACM on Programming Languages, 2, OOPSLA (2018), https://doi.org/10.1145/3276484
[40]
Hendrik van Antwerpen and Eelco Visser. 2021. Scope States: Guarding Safety of Name Resolution in Parallel Type Checkers. In 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark (Virtual Conference), Anders Møller and Manu Sridharan (Eds.) (LIPIcs, Vol. 194). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. isbn:978-3-95977-190-0 https://doi.org/10.4230/LIPIcs.ECOOP.2021.1
[41]
Guido Wachsmuth, Gabriël Konat, Vlad A. Vergu, Danny M. Groenewegen, and Eelco Visser. 2013. A Language Independent Task Engine for Incremental Name and Type Analysis. In Software Language Engineering - 6th International Conference, SLE 2013, Indianapolis, IN, USA, October 26-28, 2013. Proceedings, Martin Erwig, Richard F. Paige, and Eric Van Wyk (Eds.) (Lecture Notes in Computer Science, Vol. 8225). Springer, 260–280. isbn:978-3-319-02653-4 https://doi.org/10.1007/978-3-319-02654-1_15
[42]
Aron Zwaan, Hendrik van Antwerpen, and Eelco Visser. 2022. Incremental Type-Checking for Free: Artifact. https://doi.org/10.5281/zenodo.7071393
Index Terms
- Incremental type-checking for free: using scope graphs to derive incremental type-checkers
Recommendations
A systematic approach to deriving incremental type checkers
Static typing can guide programmers if feedback is immediate. Therefore, all major IDEs incrementalize type checking in some way. However, prior approaches to incremental type checking are often specialized and hard to transfer to new type systems. In ...
Incremental type-checking for type-reflective metaprograms
GPCE '10: Proceedings of the ninth international conference on Generative programming and component engineeringGarcia introduces a calculus for type-reflective metaprogramming that provides much of the power and flexibility of C++ templates and solves many of its problems. However, one of the problems that remains is that the residual program is not type checked ...
Incremental type-checking for type-reflective metaprograms
GPCE '10Garcia introduces a calculus for type-reflective metaprogramming that provides much of the power and flexibility of C++ templates and solves many of its problems. However, one of the problems that remains is that the residual program is not type checked ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2022
1932 pages
Copyright © 2022 Owner/Author.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 31 October 2022
Published in PACMPL Volume 6, Issue OOPSLA2
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 698Total Downloads
- Downloads (Last 12 months)293
- Downloads (Last 6 weeks)53
Reflects downloads up to 13 Nov 2024
Other Metrics
Citations
Cited By
View all- Bunte ODenkers Jvan Gool LVinju JVisser EWillemse TZaidman A(2024)OIL: an industrial case study in language engineering with SpoofaxSoftware and Systems Modeling10.1007/s10270-024-01185-xOnline publication date: 3-Jun-2024
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in