Scope States: Guarding Safety of Name Resolution in Parallel Type Checkers

Authors Hendrik van Antwerpen , Eelco Visser

Thumbnail PDF


  • Filesize: 1.11 MB
  • 29 pages

Document Identifiers

Author Details

Hendrik van Antwerpen
  • Delft University of Technology, The Netherlands
Eelco Visser
  • Delft University of Technology, The Netherlands


We thank the anonymous reviewers for their helpful comments.

Cite AsGet BibTex

Hendrik van Antwerpen and Eelco Visser. Scope States: Guarding Safety of Name Resolution in Parallel Type Checkers. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 1:1-1:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Compilers that can type check compilation units in parallel can make more efficient use of multi-core architectures, which are nowadays widespread. Developing parallel type checker implementations is complicated by the need to handle concurrency and synchronization of parallel compilation units. Dependencies between compilation units are induced by name resolution, and a parallel type checker needs to ensure that units have defined all relevant names before other units do a lookup. Mutually recursive references and implicitly discovered dependencies between compilation units preclude determining a static compilation order for many programming languages. In this paper, we present a new framework for implementing hierarchical type checkers that provides implicit parallel execution in the presence of dynamic and mutual dependencies between compilation units. The resulting type checkers can be written without explicit handling of communication or synchronization between different compilation units. We achieve this by providing type checkers with an API for name resolution based on scope graphs, a language-independent formalism that supports a wide range of binding patterns. We introduce the notion of scope state to ensure safe name resolution. Scope state tracks the completeness of a scope, and is used to decide whether a scope graph query between compilation units must be delayed. Our framework is implemented in Java using the actor paradigm. We evaluated our approach by parallelizing the solver for Statix, a meta-language for type checkers based on scope graphs, using our framework. This parallelizes every Statix-based type checker, provided its specification follows a split declaration-type style. Benchmarks show that the approach results in speedups for the parallel Statix solver of up to 5.0x on 8 cores for real-world code bases.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Compilers
  • Theory of computation → Parallel algorithms
  • type checking
  • name resolution
  • parallel algorithms


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


  1. Gul A. Agha. ACTORS - a model of concurrent computation in distributed systems. MIT Press series in artificial intelligence. MIT Press, 1990. Google Scholar
  2. Andrew W. Appel. Modern Compiler Implementation in Java. Cambridge University Press, 1998. Google Scholar
  3. Janusz A. Brzozowski. Derivatives of regular expressions. Journal of the ACM, 11(4):481-494, 1964. Google Scholar
  4. K. Mani Chandy, Jayadev Misra, and Laura M. Haas. Distributed deadlock detection. ACM Trans. Comput. Syst., 1(2):144-156, 1983. URL:
  5. Sebastian Erdweg, Moritz Lichter, and Manuel Weiel. A sound and optimal incremental build system with dynamic dependencies. In Jonathan Aldrich and Patrick Eugster, editors, Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SPLASH 2015, Pittsburgh, PA, USA, October 25-30, 2015, pages 89-106. ACM, 2015. URL:
  6. GCC. The parallel gcc. URL:
  7. Go. Go 1.9: Parallel compilation. URL:
  8. Dominik Helm, Florian Kübler, Jan Thomas Kölzer, Philipp Haller, Michael Eichberg, Guido Salvaneschi, and Mira Mezini. A programming model for semi-implicit parallelization of static analyses. In Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2020, page 428–439, New York, NY, USA, 2020. Association for Computing Machinery. URL:
  9. Lennart C. L. Kats and Eelco Visser. The Spoofax language workbench: rules for declarative specification of languages and IDEs. In William R. Cook, Siobhán Clarke, and Martin C. Rinard, editors, Proceedings of the 25th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2010, pages 444-463, Reno/Tahoe, Nevada, 2010. ACM. URL:
  10. Gabriël Konat, Sebastian Erdweg, and Eelco Visser. Scalable incremental building with dynamic task dependencies. In Marianne Huchard, Christian Kästner, and Gordon Fraser, editors, Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE 2018, Montpellier, France, September 3-7, 2018, pages 76-86. ACM, 2018. URL:
  11. Gabriël Konat, Lennart C. L. Kats, Guido Wachsmuth, and Eelco Visser. Declarative name binding and scope rules. In Krzysztof Czarnecki and Görel Hedin, editors, Software Language Engineering, 5th International Conference, SLE 2012, Dresden, Germany, September 26-28, 2012, Revised Selected Papers, volume 7745 of Lecture Notes in Computer Science, pages 311-331. Springer, 2012. URL:
  12. Milind Kulkarni, Keshav Pingali, Bruce Walter, Ganesh Ramanarayanan, Kavita Bala, and L. Paul Chew. Optimistic parallelism requires abstractions. In Jeanne Ferrante and Kathryn S. McKinley, editors, Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10-13, 2007, pages 211-222. ACM, 2007. URL:
  13. Lindsey Kuper, Aaron Turon, Neelakantan R. Krishnaswami, and Ryan R. Newton. Freeze after writing: quasi-deterministic parallel programming with lvars. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 257-270. ACM, 2014. URL:
  14. David C. J. Matthews and Makarius Wenzel. Efficient parallel programming in poly/ml and isabelle/ml. In Leaf Petersen and Enrico Pontelli, editors, Proceedings of the POPL 2010 Workshop on Declarative Aspects of Multicore Programming, DAMP 2010, Madrid, Spain, January 19, 2010, pages 53-62. ACM, 2010. URL:
  15. Ryan R. Newton, Ömer S. Agacan, Peter P. Fogg, and Sam Tobin-Hochstadt. Parallel type-checking with haskell using saturating lvars and stream generators. In Rafael Asenjo 0001 and Tim Harris, editors, Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2016, Barcelona, Spain, March 12-16, 2016, page 6. ACM, 2016. URL:
  16. Pierre Néron, Andrew P. Tolmach, Eelco Visser, and Guido Wachsmuth. A theory of name resolution. In Jan Vitek, editor, 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, volume 9032 of Lecture Notes in Computer Science, pages 205-231. Springer, 2015. URL:
  17. OpenJDK. Java Microbenchmark Harness (JMH). URL:
  18. Patrik Reali. Structuring a compiler with active objects. In Jürg Gutknecht and Wolfgang Weck, editors, Modular Programming Languages, Joint Modular Languages Conference, JMLC 2000, Zurich, Switzerland, September 6-8, 2000, Proceedings, volume 1897 of Lecture Notes in Computer Science, pages 250-262. Springer, 2000. Google Scholar
  19. Jonathan Rodriguez and Ondrej Lhoták. Actor-based parallel dataflow analysis. In Jens Knoop, editor, Compiler Construction - 20th International Conference, CC 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, volume 6601 of Lecture Notes in Computer Science, pages 179-197. Springer, 2011. URL:
  20. Arjen Rouvoet, Hendrik van Antwerpen, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser. 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. URL:
  21. Rust. Parallel compilation. URL:
  22. V. Seshadri, David B. Wortman, Michael D. Junkin, S. Weber, C. P. Yu, and I. Small. Semantic analysis in a concurrent compiler. In PLDI, pages 233-240, 1988. Google Scholar
  23. Zhong Shao and Andrew W. Appel. Smartest recompilation. In POPL, pages 439-450, 1993. Google Scholar
  24. StackExchange. Do compilers utilize multithreading for faster compile times? URL:
  25. StackExchange. Is there something that prevents a multithreaded c# compiler implementation? URL:
  26. StackExchange. Why isn't javac running on multiple cores? URL:
  27. Richard M. Stallman, Roland McGrath, and Paul D. Smith. GNU Make. Free Software Foundation, May 2016. Google Scholar
  28. Swift. Swift compiler performance. URL:
  29. Triplequote. Hydra: The parallel scala compiler. URL:
  30. Hendrik van Antwerpen, Pierre Néron, Andrew P. Tolmach, Eelco Visser, and Guido Wachsmuth. A constraint language for static semantic analysis based on scope graphs. In Martin Erwig and Tiark Rompf, editors, Proceedings of the 2016 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 49-60. ACM, 2016. URL:
  31. Hendrik van Antwerpen, Casper Bach Poulsen, Arjen Rouvoet, and Eelco Visser. Scopes as types. Proceedings of the ACM on Programming Languages, 2(OOPSLA), 2018. URL:
  32. Makarius Wenzel. Parallel Proof Checking in Isabelle/Isar. In ACM SIGSAM Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS '09), page 9, New York, NY, USA, 2009. Association for Computing Machinery. Google Scholar
  33. Makarius Wenzel. Shared-memory multiprocessing for interactive theorem proving. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, volume 7998 of Lecture Notes in Computer Science, pages 418-434. Springer, 2013. URL:
  34. Jesper Öqvist and Görel Hedin. Concurrent circular reference attribute grammars. In Benoît Combemale, Marjan Mernik, and Bernhard Rumpe, editors, Proceedings of the 10th ACM SIGPLAN International Conference on Software Language Engineering, SLE 2017, Vancouver, BC, Canada, October 23-24, 2017, pages 151-162. ACM, 2017. URL: