Incrementalizing Lattice-Based Program Analyses in Datalog
Tamás Szabó, Gábor Bergmann, Sebastian Erdweg, and Markus Völter.
In Proceedings of Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). ACM, 2018.
[ pdf ]
Program analyses detect errors in code, but when code changes frequently as in an IDE,
repeated re-analysis from-scratch is unnecessary: It leads to poor performance unless
we give up on precision and recall. Incremental program analysis promises to deliver
fast feedback without giving up on precision or recall by deriving a new analysis
result from the previous one. However, Datalog and other existing frameworks for
incremental program analysis are limited in expressive power: They only support the
powerset lattice as representation of analysis results, whereas many practically
relevant analyses require custom lattices and aggregation over lattice values. To
this end, we present a novel algorithm called DRedL that supports incremental
maintenance of recursive lattice-value aggregation in Datalog. The key insight of
DRedL is to dynamically recognize increasing replacements of old lattice values by
new ones, which allows us to avoid the expensive deletion of the old value. We
integrate DRedL into the analysis framework IncA and use IncA to realize
incremental implementations of strong-update points-to analysis and string analysis
for Java. As our performance evaluation demonstrates, both analyses react to code
changes within milliseconds.
Incremental Overload Resolution in Object-Oriented Programming Languages
Tamás Szabó, Edlira Kuci, Matthijs Bijman, Mira Mezini, and Sebastian Erdweg.
In Proceedings of International Workshop on Formal Techniques for Java-like Programs (FTfJP). ACM, 2018.
[ pdf ]
Object-oriented programming languages feature static and
dynamic overloading: Multiple methods share the same name
but provide different implementations. Dynamic overloading
(also know as dynamic dispatch) is resolved at run time based
on the type of the receiver object. In this paper, we focus
on static overloading, which is resolved at compile time
based on the types of the method arguments.
The challenge this paper addresses is to incrementalize static
overload resolution in IDEs. IDEs resolve overloaded methods
for the developer to help them discern which implementation a
method call refers to. However, as the code changes, the IDE
has to reconsider previously resolved method calls when they
are affected by the code change. This paper clarifies when a
method call is affected by a code change and how to re-resolve
method calls with minimal computational effort. To this end,
we explore and compare two approaches to incremental type
checking: co-contextual type checking and IncA.
An Overview of Program Analysis using Formal Methods
Markus Völter, Tamás Szabó, Björn Engelmann, and Klaus Birken.
An addendum to the book DSL Engineering (http://dslbook.org), 2017.
[ pdf ]
Static program analysis refers to determining properties of programs
without executing it, relying on a range of formal methods. While
these methods have been around for a long time, over the last couple
of years, some of these methods started to scale to solve problems
of interesting size. We have used advanced type systems, abstract
interpretation, SMT solving and model checking to answer relevant
questions about programs written with various DSLs. In this booklet
we introduce the methods, illustrate what we have done with them,
and describe how we have integrated the analysis method and existing
tools with languages and IDEs.
IncAL: A DSL for Incremental Program Analysis with Lattices
Tamás Szabó, Sebastian Erdweg, and Markus Völter.
In International Workshop on Incremental Computing (IC), 2017.
[ pdf ]
We describe IncAL, a DSL for incremental lattice-based
program analyses. IncAL is an extension of our previous work,
IncA, which supported relational program analyses, that has
been used for practically relevant analyses on industrial code
bases. IncAL improves the expressive power of IncA by
adding support for synthesis of data, enabling, for example,
incremental execution of interval analysis.
Lessons learned from developing mbeddr: a case study in language engineering with MPS
Markus Völter, Bernd Kolb, Tamás Szabó, Daniel Ratiu, and Arie van Deursen.
In Software and Systems Modeling, 2016.
[ pdf ]
Language workbenches are touted as a promising technology to engineer languages for use in a wide range
of domains, from programming to science to business. However, not many real-world case studies exist
that evaluate the suitability of language workbench technology for this task. This paper contains such a
In particular, we evaluate the development of mbeddr, a collection of integrated languages and
language extensions built with the Jetbrains MPS language workbench. mbeddr consists of 81 languages,
with their IDE support, 34 of them C extensions. The mbeddr languages use a wide variety of
notations – textual, tabular, symbolic and graphical – and the C extensions are modular; new extensions
can be added without changing the existing implementation of C. mbeddr’s development has spanned 10 person
years so far, and the tool is used in practice and continues to be developed. This makes mbeddr a
meaningful case study of non-trivial size and complexity.
The evaluation is centered around five research questions: language modularity, notational freedom and
projectional editing, mechanisms for managing complexity, performance and scalability issues and the
consequences for the development process.
Dedicated Support for Analyses and Optimizations in Language Workbenches
In Proceedings of Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH) - Doctoral Symposium, ACM, 2016.
[ pdf ]
Language workbenches are widely used to implement domain-specific languages (DSLs)
and their accompanying integrated development environments (IDEs). They help to define
the abstract syntax, concrete syntax(es), type system, and transformations for the languages.
However, there are other language aspects, specifically program analyses and optimizations,
that are also crucial to a language implemen- tation, but state-of-the-art language workbenches
has only limited support for them. The high implementation effort for these language aspects
is justifiable for a general-purpose language (GPL), but is not justifiable for DSLs because
of their different development economies.
To this end, I conduct research on dedicated support for analyses and optimizations for DSLs
in language workbenches. My main goal is to develop declarative meta-languages that help to
define static program analyses and that capture and automate patterns and techniques of optimizations.
The research directions are directly driven by industrial need, and upon successful completion,
the results would be applied in projects centered around DSLs for high-performance computing (HPC),
insurance, and concurrent embedded systems.
Efficient Development of Consistent Projectional Editors using Grammar Cells
Markus Völter, Tamás Szabó, Sascha Lisson, Bernd Kolb, Sebastian Erdweg, and Thorsten Berger.
In Proceedings of Software Language Engineering (SLE), ACM, 2016.
[ pdf ]
The definition of a projectional editor does not just specify the notation of a
language, but also how users interact with the notation. Because of that it is
easy to end up with different interaction styles within one and between multiple
languages. The resulting inconsistencies have proven to be a major usability problem.
To address this problem, we introduce grammar cells, an approach for declaratively
specifying textual notations and their interactions for projectional editors.
In the paper we motivate the problem, give a formal definition of grammar cells,
and define their mapping to low-level editor behaviors. Our evaluation based
on project experience shows that grammar cells improve editing experience by
providing a consistent and intuitive, “text editor-like” user experience for
textual notations. At the same time they do not limit language composability
and the use of non-textual notations, the primary benefits of projectional
editors. We have implemented grammar cells for Jetbrains MPS, but they can also
be used with other projectional editors.
IncA: A DSL for the Definition of Incremental Program Analyses
Tamás Szabó, Sebastian Erdweg, and Markus Voelter.
In Proceedings of International Conference on Automated Software Engineering (ASE), ACM, 2016.
[ pdf ]
Program analyses support software developers, for example, through error
detection, code-quality assurance, and by enabling compiler optimizations
and refactorings. To provide real-time feedback to developers within IDEs,
an analysis must run efficiently even if the analyzed code base is large.
To achieve this goal, we present a domain-specific language called IncA for
the definition of efficient incremental program analyses that update their
result as the program changes. IncA compiles analyses into graph patterns
and relies on existing incremental matching algorithms. To scale IncA analyses
to large programs, we describe optimizations that reduce caching and prune
change propagation. Using IncA, we have developed incremental control flow
and points-to analysis for C, well-formedness checks for DSLs, and 10 FindBugs
checks for Java. Our evaluation demonstrates significant speedups for all analyses
compared to their non-incremental counterparts.
An Extensible Framework for Variable-Precision Data-Flow Analyses in MPS
Tamás Szabó, Simon Alperovich, Markus Voelter, and Sebastian Erdweg.
In Proceedings of International Conference on Automated Software Engineering (ASE) - Tool Track, ACM, 2016.
[ pdf ]
Data-flow analyses are used as part of many software engineering
tasks: they are the foundations of program understanding, refactorings
and optimized code generation. Similar to general-purpose languages
(GPLs), state-of-the-art domain-specific languages (DSLs) also require
sophisticated data-flow analyses. However, as a consequence of the
different economies of DSL development and their typically relatively
fast evolution, the effort for developing and evolving such analyses
must be lowered compared to GPLs. This tension can be resolved with
dedicated support for data-flow analyses in language workbenches.
In this tool paper we present MPS-DF, which is the component in the MPS
language workbench that supports the definition of data-flow analyses
for DSLs. Language developers can define data-flow graph builders
declaratively as part of a language definition and compute analysis
results efficiently based on these data-flow graphs. MPS-DF is
extensible such that it does not compromise the support for language
composition in MPS. Additionally, clients of MPS-DF analyses can run the
analyses with variable precision thus trading off precision for
performance. This allows clients to tailor an analysis to a particular
mbeddr: Extensible Languages for Embedded Software Development
Tamás Szabó, Markus Voelter, Bernd Kolb, Daniel Ratiu, Bernhard Schaetz.
In Proceedings of High Integrity Language Technology (HILT), ACM, 2014.
[ pdf ]
In this industrial presentation we will demonstrate mbeddr,
an extensible set of integrated languages for embedded software
development. After discussing the context of the talk,
we will give details about the mbeddr architecture, which
relies on the MPS language workbench. Then, we will elaborate
on the extension modules and show how they fit with
safety-critical development processes. Finally, we will point
out how the existing languages can be extended by the user
by giving some real-world examples, including a language
construct that could have prevented the Apple “goto fail”
bug as well as mathematical notations.
Developing and Visualizing Live Model Queries
Zoltán Újhelyi, Tamás Szabó, István Ráth, Dániel Varró.
In Proceedings of Analysis of Model Transformations (AMT), ACM, 2012.
[ pdf ]
Several important tasks performed by model driven development tools —
such as well-formedness constraint validation or model transformations —
rely on evaluating model queries. If the model changes rapidly or frequently,
it is beneficial to provide live queries that automatically propagate
these model changes into the query results. To ease the development and
debugging of live queries, the development environment should provide a
way to evaluate the query results continuously, helping to understand how the created query works.
This paper presents a generic live model query visualizer that displays
and updates the query results depending on their source models. It has
been implemented for the EMF-IncQuery framework and presented here
for validating BPMN models.
Incremental pattern matching for the efficient computation of transitive closure
Gábor Bergmann, István Ráth, Tamás Szabó, Paolo Torrini, Dániel Varró.
In Proceedings of International Conference on Graph Transformations (ICGT), Springer-Verlag, 2012.
[ pdf ]
Pattern matching plays a central role in graph transformations as a key
technology for computing local contexts in which transformation rules are to be applied.
Incremental matching techniques offer a performance advantage over the search-based approach,
in a number of scenarios including on-the-fly model synchronization, model simulation,
view maintenance, well-formedness checking and state space traversal. However, the incremental
computation of transitive closure in graph pattern matching has started to be investigated
only recently. In this paper, we propose multiple algorithms for the efficient computation of
generalized transitive closures. As such, our solutions are capable of computing reachability
regions defined by simple graph edges as well as complex binary relationships defined by
graph patterns, that may be used in a wide spectrum of modeling problems. We also report on
experimental evaluation of our prototypical implementation, carried out within the context
of a stochastic system simulation case study.
Parallel Saturation Based Model Checking
András Vörös, Tamás Szabó, Attila Jámbor, Dániel Darvas, Ákos Horváth, Tamás Bartha.
In Proceedings of International Symposium on Parallel and Distributed Computing (ISPDC), IEEE, 2011.
[ pdf ]
Formal verification is becoming a fundamental step
of safety-critical and model-based software development. As
part of the verification process, model checking is one of the
current advanced techniques to analyze the behavior of a
system. In this paper, we examine an existing parallel model
checking algorithm and we propose improvements to eliminate
some computational bottlenecks. Our measurements show that
the resulting new algorithm has better scalability and
performance than both the former parallel approach and the