title: RT-trust: automated refactoring for trusted execution under real-time constraints

authors:
Yin Liu
Kijin An
Eli Tilevich

abstract: Real-time systems must meet strict timeliness requirements. These systems also often need to protect their critical program information (CPI) from adversarial interference and intellectual property theft. Trusted execution environments (TEE) execute CPI tasks on a special-purpose processor, thus providing hardware protection. However, adapting a system written to execute in environments without TEE requires partitioning the code into the regular and trusted parts. This process involves complex manual program transformations that are not only laborious and intellectually tiresome, but also hard to validate and verify for the adherence to real-time constraints. To address these problems, this paper presents novel program analyses and transformation techniques, accessible to the developer via a declarative meta-programming model. The developer declaratively specifies the CPI portion of the system. A custom static analysis checks CPI specifications for validity, while probe-based profiling helps identify whether the transformed system would continue to meet the original real-time constraints, with a feedback loop suggesting how to modify the code, so its CPI can be isolated. Finally, an automated refactoring isolates the CPI portion for TEE-based execution, communicated with through generated calls to the TEE API. We have evaluated our approach by successfully enabling the trusted execution of the CPI portions of several microbenchmarks and a drone autopilot. Our approach shows the promise of declarative meta-programming in reducing the programmer effort required to adapt systems for trusted execution under real-time constraints.


venue: gpce

title: Anomaly analyses for feature-model evolution

authors:
Michael Nieke
Jacopo Mauro
Christoph Seidl
Thomas Thüm
Ingrid Chieh Yu
Felix Franzke

abstract: Software Product Lines (SPLs) are a common technique to capture families of software products in terms of commonalities and variabilities. On a conceptual level, functionality of an SPL is modeled in terms of features in Feature Models (FMs). As other software systems, SPLs and their FMs are subject to evolution that may lead to the introduction of anomalies (e.g., non-selectable features). To fix such anomalies, developers need to understand the cause for them. However, for large evolution histories and large SPLs, explanations may become very long and, as a consequence, hard to understand. In this paper, we present a method for anomaly detection and explanation that, by encoding the entire evolution history, identifies the evolution step of anomaly introduction and explains which of the performed evolution operations lead to it. In our evaluation, we show that our method significantly reduces the complexity of generated explanations.


title: Model-based security analysis of feature-oriented software product lines

authors:
Sven Peldszus
Daniel Strüber
Jan Jürjens

abstract: Today's software systems are too complex to ensure security after the fact – security has to be built into systems by design. To this end, model-based techniques such as UMLsec support the design-time specification and analysis of security requirements by providing custom model annotations and checks. Yet, a particularly challenging type of complexity arises from the variability of software product lines. Analyzing the security of all products separately is generally infeasible. In this work, we propose SecPL, a methodology for ensuring security in a software product line. SecPL allows developers to annotate the system design model with product-line variability and security requirements. To keep the exponentially large configuration space tractable during security checks, SecPL provides a family-based security analysis. In our experiments, this analysis outperforms the naive strategy of checking all products individually. Finally, we present the results of a user study that indicates the usability of our overall methodology.


title: Regenerate: a language generator for extended regular expressions

authors:
Gabriel Radanne
Peter Thiemann

abstract: Regular expressions are part of every programmer’s toolbox. They are used for a wide variety of language-related tasks and there are many algorithms for manipulating them. In particular, matching algorithms that detect whether a word belongs to the language described by a regular expression are well explored, yet new algorithms appear frequently. However, there is no satisfactory methodology for testing such matchers. We propose a testing methodology which is based on generating positive as well as negative examples of words in the language. To this end, we present a new algorithm to generate the language described by a generalized regular expression with intersection and complement operators. The complement operator allows us to generate both positive and negative example words from a given regular expression. We implement our generator in Haskell and OCaml and show that its performance is more than adequate for testing.


title: Measuring effectiveness of sample-based product-line testing

authors:
Sebastian Ruland
Lars Luthmann
Johannes Bürdek
Sascha Lity
Thomas Thüm
Malte Lochau
Márcio Ribeiro

abstract: Recent research on quality assurance (QA) of configurable software systems (e.g., software product lines) proposes different analysis strategies to cope with the inherent complexity caused by the well-known combinatorial-explosion problem. Those strategies aim at improving efficiency of QA techniques like software testing as compared to brute-force configuration-by-configuration analysis. Sampling constitutes one of the most established strategies, defining criteria for selecting a drastically reduced, yet sufficiently diverse subset of software configurations considered during QA. However, finding generally accepted measures for assessing the impact of sample-based analysis on the effectiveness of QA techniques is still an open issue. We address this problem by lifting concepts from single-software mutation testing to configurable software. Our framework incorporates a rich collection of mutation operators for product lines implemented in C to measure mutation scores of samples, including a novel family-based technique for product-line mutation detection. Our experimental results gained from applying our tool implementation to a collection of subject systems confirms the widely-accepted assumption that pairwise sampling constitutes the most reasonable efficiency/effectiveness trade-off for sample-based product-line testing.


title: A domain-specific language for exploratory data visualization

authors:
Karl Smeltzer
Martin Erwig

abstract: With an ever-growing amount of collected data, the importance of visualization as an analysis component is growing in concert. The creation of good visualizations often doesn't happen in one step but is rather an iterative and exploratory process. However, this process is currently not well supported in most of the available visualization tools and systems. Visualization authors are forced to commit prematurely to particular design aspects of their creations, and when exploring potential variant visualizations, they are forced to adopt ad hoc techniques such as copying code snippets or keeping a collection of separate files.


title: Exploring feature interactions without specifications: a controlled experiment

authors:
Larissa Rocha Soares
Jens Meinicke
Sarah Nadi
Christian Kästner
Eduardo Santana de Almeida

abstract: In highly configurable systems, features may interact unexpectedly and produce faulty behavior. Those faults are not easily identified from the analysis of each feature separately, especially when feature specifications are missing. We propose VarXplorer, a dynamic and iterative approach to detect suspicious interactions. It provides information on how features impact the control and data flow of the program. VarXplorer supports developers with a graph that visualizes this information, mainly showing suppress and require relations between features. To evaluate whether VarXplorer helps improve the performance of identifying suspicious interactions, we perform a controlled study with 24 subjects. We find that with our proposed feature-interaction graphs, participants are able to identify suspicious interactions more than 3 times faster compared to the state-of-the-art tool.


title: A practical unification of multi-stage programming and macros

authors:
Nicolas Stucki
Aggelos Biboudis
Martin Odersky

abstract: Program generation is indispensable. We propose a novel unification of two existing metaprogramming techniques: multi-stage programming and hygienic generative macros. The former supports runtime code generation and execution in a type-safe manner while the latter offers compile-time code generation.


title: Meta-programming for cross-domain tensor optimizations

authors:
Adilla Susungi
Norman A. Rink
Albert Cohen
Jerónimo Castrillón
Claude Tadonki

abstract: Many modern application domains crucially rely on tensor operations. The optimization of programs that operate on tensors poses difficulties that are not adequately addressed by existing languages and tools. Frameworks such as TensorFlow offer good abstractions for tensor operations, but target a specific domain, i.e. machine learning, and their optimization strategies cannot easily be adjusted to other domains. General-purpose optimization tools such as Pluto and existing meta-languages offer more flexibility in applying optimizations but lack abstractions for tensors. This work closes the gap between domain-specific tensor languages and general-purpose optimization tools by proposing the Tensor optimizations Meta-Language (TeML). TeML offers high-level abstractions for both tensor operations and loop transformations, and enables flexible composition of transformations into effective optimization paths. This compositionality is built into TeML's design, as our formal language specification will reveal. We also show that TeML can express tensor computations as comfortably as TensorFlow and that it can reproduce Pluto's optimization paths. Thus, optimized programs generated by TeML execute at least as fast as the corresponding Pluto programs. In addition, TeML enables optimization paths that often allow outperforming Pluto.


title: Implementing a semi-causal domain-specific language for context detection over binary sensors

authors:
Nic Volanschi
Bernard P. Serpette
Charles Consel

abstract: In spite of the fact that many sensors in use today are binary (i.e. produce only values of 0 and 1), and that useful context-aware applications are built exclusively on top of them, there is currently no development approach specifically targeted to binary sensors. Dealing with notions of state and state combinators, central to binary sensors, is tedious and error-prone in current approaches. For instance, developing such applications in a general programming language requires writing code to process events, maintain state and perform state transitions on events, manage timers and/or event histories.


title: Pattern matching in an open world

authors:
Weixin Zhang
Bruno C. d. S. Oliveira

abstract: Pattern matching is a pervasive and useful feature in functional programming. There have been many attempts to bring similar notions to Object-Oriented Programming (OOP) in the past. However, a key challenge in OOP is how pattern matching can coexist with the open nature of OOP data structures, while at the same time guaranteeing other desirable properties for pattern matching.


title: A language feature to unbundle data at will (short paper)

authors:
Musa Al-hassy
Jacques Carette
Wolfram Kahl

abstract: Programming languages with sufficiently expressive type systems provide users with different means of data ‘bundling’. Specifically, in dependently-typed languages such as Agda, Coq, Lean and Idris, one can choose to encode information in a record either as a parameter or a field. For example, we can speak of graphs over a particular vertex set, or speak of arbitrary graphs where the vertex set is a component. These create isomorphic types, but differ with respect to intended use. Traditionally, a library designer would make this choice (between parameters and fields); if a user wants a different variant, they are forced to build conversion utilities, as well as duplicate functionality. For a graph data type, if a library only provides a Haskell-like typeclass view of graphs over a vertex set, yet a user wishes to work with the category of graphs, they must now package a vertex set as a component in a record along with a graph over that set.


title: Agile construction of data science DSLs (tool demo)

authors:
Artur Andrzejak
Kevin Kiefer
Diego Elias Costa
Oliver Wenz

abstract: Domain Specific Languages (DSLs) have proven useful in the domain of data science, as witnessed by the popularity of SQL. However, implementing and maintaining a DSL incurs a significant effort which limits their utility in context of fast-changing data science frameworks and libraries.


title: Foreign language interfaces by code migration

abstract: A foreign function interface (FFI) is a classical abstraction used for interfacing a programming language with another foreign language to reuse its libraries. This interface is important for a new (or non prevailing) language because it lacks libraries and thus needs to borrow libraries written in a foreign language when the programmer develops a practical application in that new language. However, a modern library often exploits unique language mechanisms of the implementation language. This makes the use of the library difficult through a simple function call from that new language. This paper presents our approach to this problem. We use an embedded domain specific language (DSL), which is designed to resemble the foreign language, and migrate the DSL code to access to the library written in the foreign language. This paper also presents our framework Yadriggy for developing the DSL from Ruby to a foreign language environment. The framework supports DSL-specific syntax checking for the migrated DSL code.


title: Floorplan: spatial layout in memory management systems

authors:
Karl Cronburg
Samuel Z. Guyer

abstract: In modern runtime systems, memory layout calculations are hand-coded in systems languages. Primitives in these languages are not powerful enough to describe a rich set of layouts, leading to reliance on ad-hoc macros, numerous interrelated static constants, and other boilerplate code. Memory management policies must also carefully orchestrate their application of address calculations in order to modify memory cooperatively, a task ill-suited to low-level systems languages at hand which lack proper safety mechanisms.


title: Lifted static analysis using a binary decision diagram abstract domain

abstract: Many software systems are today variational. They can produce a potentially large variety of related programs (variants) by selecting suitable configuration options (features) at compile time. Specialized variability-aware (lifted, family-based) static analyses allow analyzing all variants of the family, simultaneously, in a single run without generating any of the variants explicitly. In effect, they produce precise analysis results for all individual variants. The elements of the lifted analysis domain represent tuples (i.e. disjunction of properties), which maintain one property from an existing single-program analysis domain per variant. Nevertheless, explicit property enumeration in tuples, one by one for all variants, immediately yields to combinatorial explosion given that the number of variants can grow exponentially with the number of features. Therefore, such lifted analyses may be too costly or even infeasible for families with a large number of variants.


title: Supporting feature model evolution by suggesting constraints from code-level dependency analyses

authors:
Kevin Feichtinger
Daniel Hinterreiter
Lukas Linsbauer
Herbert Prähofer
Paul Grünbacher

abstract: Feature models are a de facto standard for representing the commonalities and variability of product lines and configurable software systems. Requirements-level features are commonly implemented in multiple source code artifacts, which results in complex dependencies at the code level. As developers change and evolve features frequently, it is challenging to keep feature models consistent with their implementation. We thus present an approach combining feature-to-code mappings and code dependency analyses to inform engineers about possible inconsistencies. Our focus is on code-level changes requiring updates in feature dependencies and constraints. Our approach uses static code analysis and a variation control system to lift complex code-level dependencies to feature models. We present the suggested dependencies to the engineer in two ways: directly as links between features in a feature model and as a heatmap visualizing the dependency changes of all features in a model. We present results of an evaluation on the Pick-and-Place Unit system, which demonstrates the utility and performance of our approach and the quality of the suggestions.


title: Harmonized temporal feature modeling to uniformly perform, track, analyze, and replay software product line evolution

authors:
Daniel Hinterreiter
Michael Nieke
Lukas Linsbauer
Christoph Seidl
Herbert Prähofer
Paul Grünbacher

abstract: A feature model (FM) describes commonalities and variability within a software product line (SPL) and represents the configuration options at one point in time. A temporal feature model (TFM) additionally represents FM evolution, e.g., the change history or the planning of future releases. The increasing number of different TFM notations hampers research collaborations due to a lack of interoperability regarding notations, editors, and analyses. We present a common API for TFMs, which provides the core of a TFM ecosystem, to harmonize notations. We identified the requirements for the API based on systematically classifying and comparing the capabilities of existing TFM approaches. Our approach allows to work seamlessly with different TFM notations to perform, track, analyze and replay evolution. Our evaluation investigates two research questions on the expressiveness (RQ1) and utility (RQ2) of our approach by presenting implementations for several existing FM and TFM notations and replaying evolution histories from two case study systems.


title: Reflection in attribute grammars

authors:
Lucas Kramer
Ted Kaminski
Eric Van Wyk

abstract: This paper shows how reflection on (undecorated) syntax trees used in attribute grammars can significantly reduce the amount of boiler-plate specifications that must be written. It is implemented in the Silver attribute grammar system in the form of a reflect function mapping syntax trees and other values into a generic representation and a reify function for the inverse mapping. We demonstrate its usefulness in several ways. The first is in an extension to Silver itself that simplifies writing language extensions for the ableC extensible C specification by allowing language engineers to specify C-language syntax trees using the concrete syntax of C (with typed holes) instead of writing abstract syntax trees. Secondly, a scrap-your-boilerplate style substitution mechanism is described. The third use is in serialization and de-serialization of the interface files Silver generates to support separate compilation; a custom interface language was replaced by a generic reflection-based implementation. Finally, an experimental implementation of staged interpreters for a small staged functional language is discussed.


title: Parallel nondeterministic programming as a language extension to C (short paper)

authors:
Lucas Kramer
Eric Van Wyk

abstract: This paper explores parallel nondeterministic programming as an extension to the C programming language; it provides constructs for specifying code containing ambiguous choice as introduced by McCarthy. A translator to plain C code was implemented as an extension to the ableC language specification. Translation involves a transformation to continuation passing style, providing lazy choice by storing continuation closures in a separate task buffer. This exploration considers various search evaluation approaches and their impact on correctness and performance. Multiple search drivers were implemented, including single-threaded depth-first search, a combined breadth- and depth-first approach, as well as two approaches to parallelism. Several benchmark applications were created using the extension, including n-Queens, SAT, and triangle peg solitaire. The simplest parallel search driver, using independent threads, showed the best performance in most cases, providing a significant speedup over the sequential versions. Adding task sharing between threads showed similar or slightly improved performance.


title: Automated metamodel augmentation for seamless model evolution tracking and planning

authors:
Michael Nieke
Adrian Hoff
Christoph Seidl

abstract: In model-based software engineering, models are central artifacts used for management, design and implementation. To meet new requirements, engineers need to plan and perform model evolution. So far, model evolution histories are captured using Version Control Systems (VCSs), e.g., Git. However, these systems are unsuitable for planning model evolution as they do not have a notion of future changes. Furthermore, formally assigning responsibilities to engineers for performing evolution of model parts is achieved by using additional tools for access control. To remedy these shortcomings, we provide a method to generate evolution-aware modeling notations by augmenting existing metamodels with concepts for capturing past and planned evolution as first-class entity. Our method enables engineers to seamlessly plan future model evolution while actively developing the current model state, both using a centralized access point for evolution. In our evaluation, we provide an implementation of our method in the tool TemporalRegulator3000, show applicability for real-world metamodels, and capture the entire evolution time line of corresponding models.


title: Polymorphic extractors for semantic and portable pattern matching (short paper)

abstract: This paper introduces polymorphic extractors, a technique for tackling two main issues with the existing pattern matching techniques in functional languages. First, this technique defines semantic pattern matching rather than a syntactic one. Second, this technique solves the portability issue when defining a set of patterns based on different underlying data-structure design choices. Furthermore, polymorphic extractors can be further improved by performing optimizations and multi-stage programming. The key technique behind polymorphic extractors is using the tagless-final technique (a.k.a. polymorphic embedding/object algebras) for defining different extraction semantics over expression terms.


title: Compiler generation for performance-oriented embedded DSLs (short paper)

authors:
Amir Shaikhha
Vojin Jovanovic
Christoph E. Koch

abstract: In this paper, we present a framework for generating optimizing compilers for performance-oriented embedded DSLs (EDSLs). This framework provides facilities to automatically generate the boilerplate code required for building DSL compilers on top of the existing extensible optimizing compilers. We evaluate the practicality of our framework by demonstrating a real-world use-case successfully built with it.


title: A stage-polymorphic IR for compiling MATLAB-style dynamic tensor expressions

authors:
Alen Stojanov
Tiark Rompf
Markus Püschel

abstract: We propose a novel approach for compiling MATLAB and similar languages that are characterized by tensors with dynamic shapes and types. We stage an evaluator for a subset of MATLAB using the Lightweight Modular Staging (LMS) framework to produce a compiler that generates C code. But the first Futamura projection alone does not lead to efficient code: we need to refine the rigid stage distinction based on type and shape inference to remove costly runtime checks.


title: A domain-specific language for filtering in application-level gateways

authors:
Hampus Balldin
Christoph Reichenbach

abstract:
Application-level packet filtering is a technique for network access control in which an “application-level gateway” intercepts network packets at the application level (e.g., HTTP, FTP), scans them for security concerns and optionally logs, rewrites or discards them. Existing application-level filters express their filtering rules in general-purpose languages, which limits the correctness guarantees available for them.

We present the first declarative language for application-level network filtering, developed at Advenica AB. Our DSL uses security assertions to express properties that packets must have to be allowed through the network (e.g., “IMAP packet contains no executable attachment” or “SQL reply contains only explicitly permitted columns”), along with remedies that either reject or rewrite undesirable packets.

We have designed the language around the needs of network filter developers, with a focus on correctness: our language can statically verify several properties of filter programs, such as well-formedness of the outcome, confluence, and termination, with the help of an off-the-shelf SMT solver.

Our initial results show that the language can express many typical filtering tasks, closely maps to the application domain, and provides strong correctness guarantees.


title: eFLINT: a domain-specific language for executable norm specifications

authors:
L. Thomas van Binsbergen
Lu-Chi Liu
Robert van Doesburg
Tom M. van Engers

abstract:
Software systems that share potentially sensitive data are subjected to laws, regulations, policies and/or contracts. The monitoring, control and enforcement processes applied to these systems are currently to a large extent manual, which we rather automate by embedding the processes as dedicated and adaptable software services in order to improve efficiency and effectiveness. This approach requires such regulatory services to be closely aligned with a formal description of the relevant norms.

This paper presents eFLINT, a domain-specific language developed for formalizing norms. The theoretical foundations of the language are found in transition systems and in Hohfeld's framework of legal fundamental conceptions. The language can be used to formalize norms from a large variety of sources. The resulting specifications are executable and support several forms of reasoning such as automatic case assessment, manual exploration and simulation. Moreover, the specifications can be used to develop regulatory services for several types of monitoring, control and enforcement. The language is evaluated through a case study formalizing articles 6(1)(a) and 16 of the General Data Protection Regulation (GDPR). A prototype implementation of eFLINT is discussed and is available online.


title: Correctness-by-construction for feature-oriented software product lines

authors:
Tabea Bordis
Tobias Runge
Ina Schaefer

abstract: Software product lines are increasingly used to handle the growing demand of custom-tailored software variants. They provide systematic reuse of software paired with variability mechanisms in the code to implement whole product families rather than single software products. A common domain of application for product lines are safety-critical systems, which require behavioral correctness to avoid dangerous situations in-field. While most approaches concentrate on post-hoc verification for product lines, we argue that a stepwise approach to create correct programs may be beneficial for developers to manage the growing variability. Correctness-by-construction is such a stepwise approach to create programs using a set of small, tractable refinement rules that guarantee the correctness of the program with regard to its specification. In this paper, we propose the first approach to develop correct-by-construction software product lines using feature-oriented programming. First, we extend correctness-by-construction by two refinement rules for variation points in the code. Second, we give a proof for the soundness of the proposed rules. Third, we implement our technique in a tool called VarCorC and show the applicability of the tool by conducting two case studies.


title: Modeling black-box components with probabilistic synthesis

authors:
Bruce Collie
Jackson Woodruff
Michael F. P. O'Boyle

abstract:
This paper is concerned with synthesizing programs based on black-box oracles: we are interested in the case where there exists an executable implementation of a component or library, but its internal structure is unknown. We are provided with just an API or function signature, and aim to synthesize a program with equivalent behavior.

To attack this problem, we detail Presyn: a program synthesizer designed for flexible interoperation with existing programs and compiler toolchains. Presyn uses high-level imperative control-flow structures and a pair of cooperating predictive models to efficiently narrow the space of potential programs. These models can be trained effectively on small corpora of synthesized examples.

We evaluate Presyn against five leading program synthesizers on a collection of 112 synthesis benchmarks collated from previous studies and real-world software libraries. We show that Presyn is able to synthesize a wider range of programs than each of them with less human input. We demonstrate the application of our approach to real-world code and software engineering problems with two case studies: accelerator library porting and detection of duplicated library reimplementations.


title: Automated variability injection for graphical modelling languages

authors:
Antonio Garmendia
Manuel Wimmer
Esther Guerra
Elena Gómez-Martínez
Juan de Lara

abstract: Model-based development approaches, such as Model-Driven Engineering (MDE), heavily rely on the use of modelling languages to achieve and automate software development tasks. To enable the definition of model variants (e.g., supporting the compact description of system families), one solution is to combine MDE with Software Product Lines. However, this is technically costly as it requires adapting many MDE artefacts associated to the modelling language -- especially the meta-models and graphical environments. To alleviate this situation, we propose a method for the automated injection of variability into graphical modelling languages. Given the meta-model and graphical environment of a particular language, our approach permits configuring the allowed model variability, and the graphical environment is automatically adapted to enable creating models with variability. Our solution is implemented atop the Eclipse Modeling Framework and Sirius, and synthesizes adapted graphical editors integrated with FeatureIDE.


title: Fluid quotes: metaprogramming across abstraction boundaries with dependent types

authors:
Shadaj Laddad
Koushik Sen

abstract: Object-oriented programming, functional programming, and metaprogramming each offer a unique axis of abstraction that enables modular code. Macros, a common technique for metaprogramming, capture ASTs as quotes to let users manipulate them in the host language. However, macros are often at odds with other programming techniques since they can only process code written at the call-site and cannot analyze code behind abstraction boundaries such as variables and methods. Furthermore, the quotes generated for macro expansion exist only at compile-time and cannot be passed around in user code. Multi-stage programming treats quotes as runtime values to address this problem, but introduces the cost of running the compiler when splicing quotes. This forces developers to choose between low runtime overhead and modularity. What if we could have the best of both worlds? We introduce fluid quotes, a new technique that uses dependent types to let users pass quotes through abstraction boundaries in runtime code while splicing them ahead-of-time. This technique enables new metaprogramming capabilities by eliminating the traditional requirement of co-locating parameter expressions with call-sites. Fluid quotes capture not only source code but also associated runtime context to ensure correctness. In addition, they can be composed into larger expressions without any macro code. We demonstrate the capabilities of fluid quotes through two specific applications: optimizing data processing pipelines and making language integrated queries more flexible.


title: VarSem: declarative expression and automated inference of variable usage semantics

authors:
Yin Liu
Eli Tilevich

abstract: Programmers declare variables to serve specific implementation purposes that we refer to as variable usage semantics (VUS). Understanding VUS is required for various software engineering tasks, including program comprehension, code audits, and vulnerability detection. To help programmers understand VUS, we present a new program analysis that infers a variable's usage semantics from its textual and context information (e.g., symbolic name, type, scope, information flow). To support this analysis, we introduce VarSem, a domain-specific language, in which a variable's semantic category is expressed as a set of declarative rules. VarSem's execution determines which program variables belong to a given semantic category. VarSem translates high-level declarative rules into low-level program analysis techniques, including natural language processing and data flow, and provides a highly extensible architecture for specifying new rules and analysis techniques. We evaluate VarSem with eight real-world systems to identify their personally identifiable information variables. The evaluation results show that VarSem infers variable semantics with satisfying accuracy/precision and passable recall, thus potentially benefiting both software and security engineers.


title: Reorganizing queries with grouping

authors:
Rui Okura
Yukiyoshi Kameyama

abstract:
Language-integrated query has attracted much attention from researchers and engineers. It enables one to write a database query with high-level abstractions, which makes it possible to compose, iterate, and reuse queries. An important issue in language-integrated query is the N+1 query problem, and Cheney et al. proposed a program-transformation approach to solve it for a core language of Microsoft’s LINQ. In our previous work, we extended their language to grouping (GROUP BY in SQL) and aggregate functions, and showed that any term can be transformed to a single SQL query. It still has a problem in that the resulting queries may be unnecessarily large and inefficient.

This paper solves the problem. Our key idea is re-organization of queries with nested control structures. While our previous work decomposes grouping into finer primitives before transformation, the new algorithm fuses nested control structures after transformation, while keeping the absence of nested data structures. Our algorithm also eliminates correlated subqueries as much as possible, to obtain better performance. We have conducted performance measurements, which shows that our new algorithm reduces the size of generated queries and improves the performance for several examples.


title: Multi-stage programming in the large with staged classes

authors:
Lionel Parreaux
Amir Shaikhha

abstract: Multi-stage programming (MSP) holds great promise, allowing the reliable generation of specialized, partially-evaluated code with static type- and scope-safety guarantees. Yet, we argue that MSP has not reached its full potential yet, as it has been traditionally limited to generating expressions, and has lacked principled facilities for generating modular programs and data structures. In that sense, we argue that MSP has been reserved for programming “in the small,” focused on generating efficient kernels of computation on the scale of single function bodies. We present a novel technique called staged classes, which extends MSP with the ability to manipulate class definitions as first-class constructs. This lets programmers use MSP “in the large,” on the level of applications, rather than mere functions. This way, applications can be designed in an abstract and modular way without runtime cost, as staged classes guarantee the removal of all staging-time abstractions, resulting in the generation of efficient specialized modules and data structures. We describe the design of a prototype relational database system in Scala, which uses several stages of runtime compilation to maximize the efficiency of query execution and data storage. We also show that staged classes can be used for defining type- and scope-safe implementations of type providers.


title: PReGO: a generative methodology for satisfying real-time requirements on COTS-based systems: definition and experience report

authors:
Benjamin Rouxel
Ulrik Pagh Schultz
Benny Akesson
Jesper Holst
Ole Jørgensen
Clemens Grelck

abstract:
Satisfying real-time requirements in cyber-physical systems is challenging as timing behaviour depends on the application software, the embedded hardware, as well as the execution environment. This challenge is exacerbated as real-world, industrial systems often use unpredictable hardware and software libraries or operating systems with timing hazards and proprietary device drivers. All these issues limit or entirely prevent the application of established real-time analysis techniques.

In this paper we propose PReGO, a generative methodology for satisfying real-time requirements in industrial commercial-off-the-shelf (COTS) systems. We report on our experience in applying PReGO to a use-case: a Search & Rescue application running on a fixed-wing drone with COTS components, including an NVIDIA Jetson board and a stock Ubuntu/Linux. We empirically evaluate the impact of each integration step and demonstrate the effectiveness of our methodology in meeting real-time application requirements in terms of deadline misses and energy consumption.


title: Manipulating GUI structures declaratively

authors:
Knut Anders Stokke
Mikhail Barash
Jaakko Järvi

abstract: GUIs often contain structures that are incidental, not properly manipulatable through well-defined APIs. For example, modifying a list of items in a GUI's model may require extraneous bookkeeping operations in the view, such as adding and removing event handlers, and updating the menu structure. Observing GUIs in practice gives an indication that programmers may find it difficult or tedious to implement complete and convenient sets of operations for manipulating various structures: useful operations for adding, inserting, swapping, or reordering elements are often missing, inconsistent, or limited. This paper introduces a DSL for programming operations that manipulate such incidental structures. The programmer specifies structures via relations between elements, concretely by defining methods that unestablish and establish a relation. This gives the programmer an ability to describe structural transformations via rules that control which relations should hold before and after a rule is applied. The API for structure manipulation is generated from these rules. Our DSL can give an abstract view on ad-hoc structures, making it easier to provide the necessary set of operations for their convenient manipulation.


title: A variational database management system

authors:
Parisa Ataei
Fariba Khan
Eric Walkingshaw

abstract: Many problems require working with data that varies in its structure and content. Current approaches, such as schema evolution or data integration tools, are highly tailored to specific kinds of variation in databases. While these approaches work well in their roles, they do not address all kinds of variation and do address the interaction of different kinds of variation in databases. In this paper, we define a framework for capturing variation as a generic and orthogonal con- cern in relational databases. We define variational schemas, variational databases, and variational queries for capturing variation in the structure, content, and information needs of relational databases, respectively. We define a type system that ensures variational queries are consistent with respect to a variational schema. Finally, we design and implement a variational database management system as an abstraction layer over a traditional relational database management system. Using previously developed use cases, we show the feasibility of our framework and demonstrate the performance of different approaches used in our system


title: Artifact and reference models for generative machine learning frameworks and build systems

authors:
Abdallah Atouani
Jörg Christian Kirchhof
Evgeny Kusmenko
Bernhard Rumpe

abstract: Machine learning is a discipline which has become ubiquitous in the last few years. While the research of machine learning algorithms is very active and continues to reveal astonishing possibilities on a regular basis, the wide usage of these algorithms is shifting the research focus to the integration, maintenance, and evolution of AI-driven systems. Although there is a variety of machine learning frameworks on the market, there is little support for process automation and DevOps in machine learning-driven projects. In this paper, we discuss how metamodels can support the development of deep learning frameworks and help deal with the steadily increasing variety of learning algorithms. In particular, we present a deep learning-oriented artifact model which serves as a foundation for build automation and data management in iterative, machine learning-driven development processes. Furthermore, we show how schema and reference models can be used to structure and maintain a versatile deep learning framework. Feasibility is demonstrated on several state-of-the-art examples from the domains of image and natural language processing as well as decision making and autonomous driving.


title: HACCLE: metaprogramming for secure multi-party computation

authors:
Yuyan Bao
Kirshanthan Sundararajah
Raghav Malik
Qianchuan Ye
Christopher Wagner
Nouraldin Jaber
Fei Wang
Mohammad Hassan Ameri
Donghang Lu
Alexander Seto
Benjamin Delaware
Roopsha Samanta
Aniket Kate
Christina Garman
Jeremiah Blocki
Pierre-David Letourneau
Benoît Meister
Jonathan Springer
Tiark Rompf
Milind Kulkarni

abstract:
Cryptographic techniques have the potential to enable distrusting parties to collaborate in fundamentally new ways, but their practical implementation poses numerous challenges. An important class of such cryptographic techniques is known as Secure Multi-Party Computation (MPC). Developing Secure MPC applications in realistic scenarios requires extensive knowledge spanning multiple areas of cryptography and systems. And while the steps to arrive at a solution for a particular application are often straightforward, it remains difficult to make the implementation efficient, and tedious to apply those same steps to a slightly different application from scratch. Hence, it is an important problem to design platforms for implementing Secure MPC applications with minimum effort and using techniques accessible to non-experts in cryptography.

In this paper, we present the HACCLE (High Assurance Compositional Cryptography: Languages and Environments) toolchain, specifically targeted to MPC applications. HACCLE contains an embedded domain-specific language Harpoon, for software developers without cryptographic expertise to write MPC-based programs, and uses Lightweight Modular Staging (LMS) for code generation.

Harpoon programs are compiled into acyclic circuits represented in HACCLE’s Intermediate Representation (HIR) that serves as an abstraction over different cryptographic protocols such as secret sharing, homomorphic encryption, or garbled circuits. Implementations of different cryptographic protocols serve as different backends of our toolchain. The extensible design of HIR allows cryptographic experts to plug in new primitives and protocols to realize computation. And the use of standard metaprogramming techniques lowers the development effort significantly.

We have implemented Harpoon and HACCLE, and used them to program interesting applications (e.g., secure auction) and key computation components of Secure MPC applications (e.g., matrix-vector multiplication and merge sort). We show that the performance is improved by using our optimization strategies and heuristics.


title: Towards supporting SPL engineering in low-code platforms using a DSL approach

authors:
Alexandre Bragança
Isabel Azevedo
Nuno Bettencourt
Carlos Morais
Diogo Teixeira
David Caetano

abstract: Low-code application platforms enable citizen developers to autonomously build complete applications, such as web applications or mobile applications. Some of these platforms also offer support for reuse to facilitate the development of similar applications. The offered mechanisms are usually elementary, they allow module reuse or building a new application from a template. However, they are insufficient to achieve the industrial level reuse necessary for software product lines (SPL). In fact, these platforms were conceived to help build standalone applications, not software families and even fewer software product lines. In this paper, we argue that the major limitation is that these platforms seldom provide access to their metamodel, the access to applications’ models and code is also limited and, therefore, makes it harder to analyze commonality and variability and construct models based on it. An approach is proposed to surpass these limitations: firstly, a metamodel of the applications built with the platform is obtained, and then, based on the metamodel, a domain-specific language (DSL) that can express the models of the applications, including variability, is constructed. With this DSL, users can combine and reuse models from different applications to explore and build similar applications. The solution is illustrated with an industrial case study. A discussion of the results is presented as well as its limitations and related work. The authors hope that this work provides inspiration and some ideas that the community can explore to facilitate the adoption and implementation of SPLs in the context, and supported by, low-code platforms.


title: Lifted termination analysis by abstract interpretation and its applications

abstract:
This paper is focused on proving termination for program families with numerical features by using abstract interpretation. Furthermore, we present an interesting application of the above lifted termination analysis for resolving “sketches”, i.e. partial programs with missing numerical parameters (holes), such that the resulting complete programs always terminate. To successfully address the above problems, we employ an abstract interpretation-based framework for inferring sufficient preconditions for termination of single programs that synthesizes piecewise-defined ranking functions.

We introduce a novel lifted decision tree domain for termination, in which decision nodes contain linear constraints defined over numerical features and leaf nodes contain piecewise ranking functions defined over program variables. Moreover, we encode a program sketch as a program family, thereby allowing the use of the lifted termination analysis as a program sketcher. In particular, we aim to find the variants (family members) that terminate under all possible inputs, which represent the correct sketch realizations.

We have implemented an experimental lifted termination analyzer, called SPLFuncTion, for proving termination of #if-based C program families and for termination-directed resolving of C program sketches. We have evaluated our approach by a set of loop benchmarks from SV-COMP, and experimental results confirm the effectiveness our approach.


title: MADMAX: a DSL for explanatory decision making

authors:
Martin Erwig
Prashant Kumar

abstract:
MADMAX is a Haskell-embedded DSL for multi-attribute, multi-layered decision making. An important feature of this DSL is the ability to generate explanations of why a computed optimal solution is better than its alternatives.

The functional approach and Haskell's type system support a high-level formulation of decision-making problems, which facilitates a number of innovations, including the gradual evolution and adaptation of problem representations, a more user-friendly form of sensitivity analysis based on problem domain data, and fine-grained control over explanations.


title: On-stack replacement for program generators and source-to-source compilers

authors:
Grégory M. Essertel
Ruby Y. Tahboub
Tiark Rompf

abstract:
On-stack replacement (OSR) describes the ability to replace currently executing code with a different version, either a more optimized one (tiered execution) or a more general one (deoptimization to undo speculative optimization). While OSR is a key component in all modern VMs for languages like Java or JavaScript, OSR has only recently been studied as a more abstract program transformation, independent of language VMs. Still, previous work has only considered OSR in the context of low-level execution models based on stack frames, labels, and jumps.

With the goal of making OSR more broadly applicable, this paper presents a surprisingly simple pattern for implementing OSR in source-to-source compilers or explicit program generators that target languages with structured control flow (loops and conditionals). We evaluate our approach through experiments demonstrating both tiered execution and speculative optimization, based on representative code patterns in the context of a state-of-the-art in-memory database system that compiles SQL queries to C at runtime. We further show that casting OSR as a high-level transformation enables new speculative optimization patterns beyond what is commonly implemented in language VMs.


title: Leveraging relational concept analysis for automated feature location in software product lines

authors:
Nicolas Hlad
Bérénice Lemoine
Marianne Huchard
Abdelhak-Djamel Seriai

abstract:
Formal Concept Analysis (FCA) has been introduced for almost a decade as a suitable method for Feature Location (FL) on a collection of product variants. Even though FCA-based FL techniques allow to locate the core of a feature implementation, they do not propose a solution to trace feature interactions to their implementation. Thus, the extracted traceability links (traces) are too inaccurate, and, in the context of SPL extraction, cannot be used to generate complete products.

In this paper, we propose to complement the FCA-based FL techniques by leveraging the power of Relational Concept Analysis, an extension of FCA to multi-relational data. From two given formal contexts, one for the product’s artefact and one for their features, our technique computes the traces that link the features and the feature interactions to their corresponding artefacts. Additionally, we introduce a stage that removes unnecessary features from the extracted traces, to make them easier to understand by an expert. Our FL technique can be applied at any artefact granularity (from files to statements) and independently from software languages.

The results show that our technique produces valid traces, from which we were able to completely rebuild the set of artefacts for each initial product. Moreover, they show that our trace reduction removes, on average, between 31% and 85% of unnecessary features from the traces.


title: Compiling pattern matching to in-place modifications

authors:
Paul Iannetta
Laure Gonnord
Gabriel Radanne

abstract:
Algebraic data types and pattern matching are popular tools to build programs manipulating complex datastructures in a safe yet efficient manner. On top of its safety advantages, compilation techniques can turn pattern matching into highly efficient deconstruction code for immutable use cases. Conversely, high-performance datastructures and languages prefer to leverage (controlled) mutations to maximize time and memory efficiency. Algebraic data types provide a natural framework to efficiently describe in-place transformations as rewrite rules. Such representation could take advantage of parallelism opportunities that appear in tree-like structures.

We present early steps towards a new technique to compile pattern matching as parallel in-place modifications of the underlying memory representation. Towards this goal, we combine the usual language approach which is common in pattern-matching compilation with tools from the polyhedral model, which is commonly used in high-performance code generation to output efficient C code.

We present our formalism, along with a prototype implementation.


title: Understanding and improving model-driven IoT systems through accompanying digital twins

authors:
Jörg Christian Kirchhof
Lukas Malcher
Bernhard Rumpe

abstract: Developers questioning why their system behaves differently than expected often have to rely on time-consuming and error-prone manual analysis of log files. Understanding the behavior of Internet of Things (IoT) applications is a challenging task because they are not only inherently hard-to-trace distributed systems, but their integration with the environment via sensors adds another layer of complexity. Related work proposes to record data during the execution of the system, which can later be replayed to analyze the system. We apply the model-driven development approach to this idea and leverage digital twins to collect the required data. We enable developers to replay and analyze the system’s executions by applying model-to-model transformations. These transformations instrument component and connector (C&C) architecture models with components that reproduce the system’s environment based on the data recorded by the system’s digital twin. We validate and evaluate the feasibility of our approach using a heating, ventilation, and air conditioning (HVAC) case study. By facilitating the reproduction of the system’s behavior, our method lowers the barrier to understanding the behavior of model-driven IoT systems.


title: Live programming and programming by example: better together (keynote)

abstract: Live programming is a paradigm in which values from program execution are shown to the programmer through continual feedback. Programming by example is a paradigm in which code is synthesized from example values showing a desired behavior. This talk presents some of our recent research that combines these two paradigms in beneficial ways. I will walk through our ideas, explain our contributions, discuss what we learned and finally provide thoughts for the future.


title: The life cycle of features in highly-configurable software systems evolving in space and time

authors:
Gabriela Karoline Michelon
Wesley K. G. Assunção
David Obermann
Lukas Linsbauer
Paul Grünbacher
Alexander Egyed

abstract: Feature annotation based on preprocessor directives is the most common mechanism in Highly-Configurable Software Systems (HCSSs) to manage variability. However, it is challenging to understand, maintain, and evolve feature fragments guarded by #ifdef directives. Yet, despite HCSSs being implemented in Version Control Systems, the support for evolving features in space and time is still limited. To extend the knowledge on this topic, we analyze the feature life cycle in space and time. Specifically, we introduce an automated mining approach and apply it to four HCSSs, analyzing commits of their entire development life cycle (13 to 20 years and 37,500 commits). This goes beyond existing studies, which investigated only differences between specific releases or entire systems. Our results show that features undergo frequent changes, often with substantial modifications of their code. The findings of our empirical analyses stress the need for better support of system evolution in space and time at the level of features. In addition to these analyses, we contribute an automated mining approach for the analysis of system evolution at the level of features. Furthermore, we also make available our dataset to foster new studies on feature evolution in HCSSs.


title: Type-safe generation of modules in applicative and generative styles

authors:
Yuhi Sato
Yukiyoshi Kameyama

abstract:
The MetaML approach for multi-stage programming provides the static guarantee of type safety and scope safety for generated code, regardless of the values of static parameters. Modules are indispensable to build large-scale programs in ML-like languages, however, they have a performance problem. To solve this problem, several languages proposed recently allow one to generate ML-style modules. Unfortunately, those languages had the problems of limited expressiveness, incomplete proofs, and code explosion.

This paper proposes two-stage programming languages for module generation, which solve all the above issues. Our languages accommodate two styles: first-class modules with generative functors and second-class modules with applicative functors. Module generation in both styles is shown to have their own merits by concrete examples. We present type systems, and type-preserving translations from our languages to plain MetaOCaml. We also show the results of performance measurements, which confirms the effectiveness of our languages.


title: Delta-based verification of software product families

authors:
Marco Scaletta
Reiner Hähnle
Dominic Steinhöfel
Richard Bubel

abstract:
The quest for feature- and family-oriented deductive verification of software product lines resulted in several proposals. In this paper we look at delta-oriented modeling of product lines and combine two new ideas: first, we extend Hähnle & Schaefer’s delta-oriented version of Liskov’s substitution principle for behavioral subtyping to work also for overridden behavior in benign cases. For this to succeed, programs need to be in a certain normal form. The required normal form turns out to be achievable in many cases by a set of program transformations, whose correctness is ensured by the recent technique of abstract execution. This is a generalization of symbolic execution that permits reasoning about abstract code elements. It is needed, because code deltas contain partially unknown code contexts in terms of “original” calls.

Second, we devise a modular verification procedure for deltas based on abstract execution, representing deltas as abstract programs calling into unknown contexts.

The result is a “delta-based” verification approach, where each modification of a method in a code delta is verified in isolation, but which overcomes the strict limitations of behavioral subtyping and works for many practical programs. The latter claim is substantiated with case studies and benchmarks.


title: Metaprogramming with combinators

authors:
Mahshid Shahmohammadian
Geoffrey Mainland

abstract: There are a wide array of methods for writing code generators. We advocate for a point in the design space, which we call metaprogramming with combinators, where programmers use (and write) combinator libraries that directly manipulate object language terms. The key language feature that makes this style of programming palatable is quasiquotation. Our approach leverages quasiquotation and other host language features to provide what is essentially a rich, well-typed macro language. Unlike other approaches, metaprogramming with combinators allows full control over generated code, thereby also providing full control over performance and resource usage. This control does not require sacrificing the ability to write high-level abstractions. We demonstrate metaprogramming with combinators through several code generators written in Haskell that produce VHDL targeted to Xilinx FPGAs.


title: Extracting the power of dependent types

authors:
Artjoms Sinkarovs
Jesper Cockx

abstract:
Most existing programming languages provide little support to formally state and prove properties about programs. Adding such capabilities is far from trivial, as it requires significant re-engineering of the existing compilers and tools. This paper proposes a novel technique to write correct-by-construction programs in languages without built-in verification capabilities, while maintaining the ability to use existing tools. This is achieved in three steps. Firstly, we give a shallow embedding of the language (or a subset) into a dependently typed language. Secondly, we write a program in that embedding, and we use dependent types to guarantee correctness properties of interest within the embedding. Thirdly, we extract a program written in the original language, so it can be used with existing compilers and tools.

Our main insight is that it is possible to express all three steps in a single language that supports both dependent types and reflection. Essentially, this allows us to express a program, its formal properties, and a compiler for it hand-in-hand, offering a lot of flexibility to programmers. We demonstrate this three-step approach by embedding a subset of the PostScript language in Agda, and illustrating it with several short examples. Thus we use the power of reflection to bring the benefits of dependent types to languages that had to go without them so far.


title: Multi-stage programming with generative and analytical macros

authors:
Nicolas Stucki
Jonathan Immanuel Brachthäuser
Martin Odersky

abstract:
In metaprogramming, code generation and code analysis are complementary. Traditionally, principled metaprogramming extensions for programming languages, like MetaML and BER MetaOCaml, offer strong foundations for code generation but lack equivalent support for code analysis. Similarly, existing macro systems are biased towards the code generation aspect.

In this work, we present a calculus for macros featuring both code generation and code analysis. The calculus directly models separate compilation of macros, internalizing a commonly neglected aspect of macros. The system ensures that the generated code is well-typed and hygienic.

We implement our system in Scala 3, provide a formalization, and prove its soundness.


title: Language-Integrated Query for Temporal Data

authors:
Simon Fowler
Vashti Galpin
James Cheney

abstract:
Modern applications often manage time-varying data. Despite decades of research on temporal databases, which culminated in the addition of temporal data operations into the SQL:2011 standard, temporal data query and manipulation operations are unavailable in most mainstream database management systems, leaving developers with the unenviable task of implementing such functionality from scratch.

In this paper, we extend language-integrated query to support writing temporal queries and updates in a uniform host language, with the language performing the required rewriting to emulate temporal capabilities automatically on any standard relational database.

We introduce two core languages, λTLINQ and λVLINQ, for manipulating transaction time and valid time data respectively, and formalise existing implementation strategies by giving provably correct semantics-preserving translations into a non-temporal core language, λLINQ. We show how existing work on query normalisation supports a surprisingly simple implementation strategy for sequenced joins. We implement our approach in the Links programming language, and describe a non-trivial case study based on curating COVID-19 statistics.


title: Preserving Consistency of Interrelated Models during View-Based Evolution of Variable Systems

authors:
Sofia Ananieva
Thomas Kühn
Ralf Reussner

abstract: Coping with different and changing requirements leads to concurrent products (variability in space) and subsequent revisions (variability in time). Moreover, products consist of interrelated models that represent different kinds of artifacts. Dependencies and redundancies between interrelated models within a product and across products can quickly lead to inconsistencies during evolution. Thus, dealing with both variability dimensions uniformly while preserving consistency of interrelated models is a major challenge when developing large and long-living variable systems. Recent research addresses uniform management of variability in space and time by unifying concepts and operations from software product line engineering and software configuration management. However, consistency preservation for interrelated models, which is a major research topic in model-driven software development, has hardly been considered in variability management. We propose an approach that builds on recent efforts for unifying variability in space and time and leverages view-based consistency preservation for systems comprised of different kinds of interrelated models. We evaluate our approach by applying it to two real-world case studies: the well-known ArgoUML-SPL, that is based on the UML modeling tool ArgoUML, and MobileMedia, a mobile application for media management. Our results show that, by manually evolving only the Java models of products, other interrelated models (i.e.,~UML class diagrams) and the remaining affected products can be kept consistent fully automatically.


title: Composable Sequence Macros for Fast Iteration

authors:
Anna Bolotina
Ryan Culpepper

abstract: Racket provides for loops with macro-extensible sequence expressions. Sequence macros offer better performance than dynamic sequence implementations, but they are complicated to define and Racket offers little support for creating new sequence macros by combining existing ones. In this paper, we develop such support in the form of sequence combinator macros and a general comprehension form. These utilities are implemented by manipulating compile-time records that contain binders and expressions; the binding relationships between the components are not trivial. We discuss how to diagnose and solve type and scoping problems in our implementation.


title: Model-Driven IoT App Stores: Deploying Customizable Software Products to Heterogeneous Devices

authors:
Arvid Butting
Jörg Christian Kirchhof
Anno Kleiss
Judith Michael
Radoslav Orlov
Bernhard Rumpe

abstract: Internet of Things (IoT) devices and the software they execute are often strongly coupled with vendors preinstalling their software at the factory. Future IoT applications are expected to be distributed via app stores. A strong coupling between hard- and software hinders the rise of such app stores. Existing model-driven approaches for developing IoT applications focus largely on the behavior specification and message exchange but generate code that targets a specific set of devices. By raising the level of abstraction, models can be utilized to decouple hard- and software and adapt to various infrastructures. We present a concept for a model-driven app store that decouples hardware and software development of product lines of IoT applications.


title: Dynamic Replanning of Multi-drone Missions using Dynamic Forward Slicing

authors:
Miguel Campusano
Ulrik Pagh Schultz Lundquist

abstract:
Unmanned Aerial Systems (UAS, typically known as drones) are useful in many application domains, such as logistics and precision farming, especially when they fly Beyond Visual Line of Sight (BVLOS). To effectively use multiple UAS for BVLOS missions, it is required to precisely plan the flight of each UAS involved in the missions, allocating the required airspace ahead of time. The dots Domain-Specific Language (DSL) can be used to plan and execute such missions but does not support the adaptation of missions when unexpected changes occur during the execution of these missions. Such dynamic replanning of missions to changing conditions is a crucial feature for the safe integration of UAS into the airspace since it allows the UAS to adapt to these changes, such as yielding to emergency response aircraft.

In this work, we propose a program transformation technique inspired by program slicing to dynamically replan ongoing dots-specified multi-UAS missions using the same planner built for the dots language. Whenever dynamic replanning is needed, we compute a forward slice of the dots program based on the current runtime state of the mission. This generates a new program that obeys the original mission specification but only specifies the mission from the point in time where the replanning is needed. We validate our proposed technique by integrating it into ros-dots, a service-oriented architecture for autonomous UAS operations.


title: Data Types as a More Ergonomic Frontend for Grammar-Guided Genetic Programming

authors:
Guilherme Espada
Leon Ingelse
Paulo Canelas
Pedro Barbosa
Alcides Fonseca

abstract:
Genetic Programming (GP) is an heuristic method that can be applied to many Machine Learning, Optimization and Engineering problems. In particular, it has been widely used in Software Engineering for Test-case generation, Program Synthesis and Improvement of Software (GI).

Grammar-Guided Genetic Programming (GGGP) approaches allow the user to refine the domain of valid program solutions. Backus Normal Form is the most popular interface for describing Context-Free Grammars (CFG) for GGGP. BNF and its derivatives have the disadvantage of interleaving the grammar language and the target language of the program.

We propose to embed the grammar as an internal Domain-Specific Language in the host language of the framework. This approach has the same expressive power as BNF and EBNF while using the host language type-system to take advantage of all the existing tooling: linters, formatters, type-checkers, autocomplete, and legacy code support. These tools have a practical utility in designing software in general, and GP systems in particular.

We also present Meta-Handlers, user-defined overrides of the tree-generation system. This technique extends our object-oriented encoding with more practicability and expressive power than existing CFG approaches, achieving the same expressive power of Attribute Grammars, but without the grammar vs target language duality.

Furthermore, we evidence that this approach is feasible, showing an example Python implementation as proof. We also compare our approach against textual BNF-representations w.r.t. expressive power and ergonomics. These advantages do not come at the cost of performance, as shown by our empirical evaluation on 5 benchmarks of our example implementation against PonyGE2. We conclude that our approach has better ergonomics with the same expressive power and performance of textual BNF-based grammar encodings.


title: The Cost of Dynamism in Static Languages for Image Processing

authors:
Baptiste Esteban
Edwin Carlinet
Guillaume Tochon
Didier Verna

abstract: Generic programming is a powerful paradigm abstracting data structures and algorithms to improve their reusability, as long as they respect a given interface. Coupled with a performance-driven language, it is a paradigm of choice for scientific libraries where the implementation of manipulated objects may change depending on their use case, or for performance purposes. In those performance-driven languages, genericity is often implemented statically to perform some optimization. This does not fit well with the dynamism needed to handle objects which may only be known at runtime. Thus, in this article, we evaluate a model that couples static genericity with a dynamic model based on type erasure in the context of image processing. Its cost is assessed by comparing the performance of the implementation of some common image processing algorithms in C++ and Rust, two performance-driven languages supporting some form of genericity. Finally, we demonstrate that compile-time knowledge of some specific information is critical for performance, and also that the runtime overhead depends on the algorithmic scheme in use.


title: Language Support for Refactorability Decay Prevention

authors:
Dov Fraivert
David H. Lorenz

abstract: Even code that is free of smells may be at high risk of forming them. In such cases, developers can either perform preventive refactoring in order to reduce this risk, or leave the code as is and perform corrective refactoring as smells emerge. In practice, however, developers usually avoid preventive refactoring during the development phase, and when code smells eventually form, other developers who are less acquainted with the code avoid the more complex corrective refactoring. As a result, a refactoring opportunity is missed, and the quality and maintainability of the code is compromised. In this work, we treat refactoring not as a single atomic action, but rather as a sequence of subactions. We divide the responsibility for these subactions between the original developer of the code, who just prepares the code for refactoring, and a future developer, who may need to carry out the actual refactoring action. To manage this division of responsibility, we introduce a set of annotations along with an annotation processor that prevents software erosion from compromising the ability to perform the refactoring action.


title: Generic Solution-Space Sampling for Multi-domain Product Lines

authors:
Marc Hentze
Tobias Pett
Chico Sundermann
Sebastian Krieter
Thomas Thüm
Ina Schaefer

abstract: Validating a configurable software system is challenging, as there are potentially millions of configurations, which makes testing each configuration individually infeasible. Thus, existing sampling algorithms allow to compute a representative subset of configurations, called sample, that can be tested instead. However, sampling on the set of configurations may miss potential error sources on implementation level. In this paper, we present solution-space sampling, a concept that mitigates this problem by allowing to sample directly on the implementation level. We apply solution-space sampling to six real-word, automotive product lines and show that it produces up to 56 % smaller samples, while also covering all potential error sources missed by problem-space sampling.


title: Type System for Four Delimited Control Operators

authors:
Chiaki Ishio
Kenichi Asai

abstract: The operational behavior of control operators has been studied comprehensively in the past few decades, but type systems of control operators have not. There are distinct type systems for shift, control, and shift0 without any relationship between them, and there has not been a type system that directly corresponds to control0. This paper remedies this situation by giving a uniform type system for all the four control operators. Following Danvy and Filinski’s approach, we derive a monomorphic type system from the CPS interpreter that defines the operational semantics of the four control operators. By implementing the typed CPS interpreter in Agda, we show that the CPS translation preserves types and that the calculus with all the four control operators is terminating. Furthermore, we show the relationship between our type system and the previous type systems for shift, control, and shift0.


title: A Model-Driven Generative Self Play-Based Toolchain for Developing Games and Players

authors:
Evgeny Kusmenko
Maximilian Münker
Matthias Nadenau
Bernhard Rumpe

abstract: Turn-based games such as chess are very popular, but tool-chains tailored for their development process are still rare. In this paper we present a model-driven and generative toolchain aiming to cover the whole development process of rule-based games. In particular, we present a game description language enabling the developer to model the game in a logics-based syntax. An executable game interpreter is generated from the game model and can then act as an environment for reinforcement learning-based self-play training of players. Before the training, the deep neural network can be modeled manually by a deep learning developer or generated using a heuristics estimating the complexity of mapping the state space to the action space. Finally, we present a case study modeling three games and evaluate the language features as well as the player training capabilities of the toolchain.


title: Incremental Processing of Structured Data in Datalog

authors:
André Pacak
Tamás Szabó
Sebastian Erdweg

abstract: Incremental computations react to input changes by updating their outputs. Compared to a non-incremental rerun, incremental computations can provide order-of-magnitude speedups, since often small input changes trigger small output changes. One popular means for implementing incremental computations is to encode the computation in Datalog, for which efficient incremental solvers exist. However, Datalog is very restrictive in terms of the data types it can process: Atomic data organized in relations. While structured tree and graph-shaped data can be encoded in relations, a naive encoding inhibits incrementality. In this paper, we present an encoding of structured data in Datalog that supports efficient incrementality such that small input changes are expressible. We explain how to efficiently implement and integrate this encoding into an existing incremental Datalog engine, and we show how tree diffing algorithms can be used to change the encoded data.


title: Language Design Meets Verifying Compilers (Keynote)

abstract: The dream of developing compilers that automatically verify whether or not programs meet their specifications remains an ongoing challenge. Such "verifying compilers" are (finally) on the verge of entering mainstream software development. This is partly due to advancements made over the last few decades, but also to the increasingly significant and complex role software plays in the modern world. As computer scientists, we should encourage this transition and help relegate many forms of software error to the history books. One way of increasing adoption is to design languages around these tools which look, on the surface, like regular programming languages. That is, to seamlessly integrate specification and verification and offer something that, for the everyday programmer, appears as nothing more than glorified type checking. This requires, amongst other things, careful consideration as to which language features mesh well with verification, and which do not. The design space here is interesting and subtle, but has been largely overlooked. In this talk, I will attempt to shed light on this murky area by contrasting the choices made in two existing languages: Dafny and Whiley.


title: A Modern C++ Point of View of Programming in Image Processing

authors:
Michaël Roynard
Edwin Carlinet
Thierry Géraud

abstract: C++ is a multi-paradigm language that enables the programmer to set up efficient image processing algorithms easily. This language strength comes from many aspects. C++ is high-level, so this enables developing powerful abstractions and mixing different programming styles to ease the development. At the same time, C++ is low-level and can fully take advantage of the hardware to deliver the best performance. It is also very portable and highly compatible which allows algorithms to be called from high-level, fast-prototyping languages such as Python or Matlab. One fundamental aspects where C++ shines is generic programming. Generic programming makes it possible to develop and reuse bricks of software on objects (images) of different natures (types) without performance loss. Nevertheless, conciliating genericity, efficiency, and simplicity at the same time is not trivial. Modern C++ (post-2011) has brought new features that made it simpler and more powerful. In this paper, we focus on some C++20 aspects of generic programming: ranges, views, and concepts, and see how they extend to images to ease the development of generic image algorithms while lowering the computation time.


title: SQL to Stream with S2S: An Automatic Benchmark Generator for the Java Stream API

authors:
Filippo Schiavio
Andrea Rosà
Walter Binder

abstract: The Java Stream API was introduced in Java 8, allowing developers to express computations in a functional style by defining a pipeline of data-processing operations. Despite the growing importance of this API, there is a lack of benchmarks specifically targeting stream-based applications. Instead of designing and implementing new ad-hoc workloads for the Java Stream API, we propose to automatically translate existing data-processing workloads. To this end, we present S2S, an automatic benchmark generator for the Java Stream API. S2S is a SQL query compiler that converts existing workloads designed for relational databases to stream-based code. We use S2S to generate BSS, the first benchmark suite for the Java Stream API.


title: Deep Fusion for Efficient Nested Recursive Computations

abstract: One of the performance bottlenecks of nested recursive computations is the intermediate collections created at different levels of recursion. The existing techniques such as vertical and horizontal loop fusion do not remove such intermediate allocations. This paper proposes deep fusion, a technique for the efficient compilation of nested recursive computation over collections. The input to our compilation framework is a high-level functional program that can represent computations on flat and nested collections such as lists, sets, bags, and maps. The intermediate collections are removed in three levels. First, the immutable collections are translated into mutable ones by leveraging in-place updates using the destination-passing style technique. Second, deep fusion enables the inner level of recursion to reuse the destinations of the outer levels for in-place updates. Third, deep fusion removes the need to allocate tiny intermediate collections at different depths of recursion. Our experiments show that deep fusion can improve the performance of nested recursion over nested lists and maps.


title: Crossover: Towards Compiler-Enabled COBOL-C Interoperability

authors:
Mart van Assen
Manzi Aimé Ntagengerwa
Ömer Sayilir
Vadim Zaytsev

abstract: Interoperability across software languages is an important practical topic. In this paper, we take a deep dive into investigating and tackling the challenges involved with achieving interoperability between C and BabyCobol. The latter is a domain-specific language condensing challenges found in compiling legacy languages — borrowing directly from COBOL's data philosophy. Crossover, a compiler designed specifically to showcase the interoperability, exposes details of connecting a COBOL-like language with PICTURE clauses and re-entrant procedures, to C with primitive types and struct composites. Crossover features a C library for overcoming the differences between the data representations native to the respective languages. We illustrate the design process of Crossover and demonstrate its usage to provide a strategy to achieve interoperability between legacy and modern languages. The described process is aimed to be a blueprint for achievable interoperability between full-fledged COBOL and modern C-like programming languages.


title: Automatically Generated Supernodes for AST Interpreters Improve Virtual-Machine Performance

authors:
Matteo Basso
Daniele Bonetta
Walter Binder

abstract:
Abstract syntax tree (AST) interpreters allow implementing programming languages in a straight-forward way. However, AST interpreters implemented in object-oriented languages, such as e.g. in Java, often suffer from two serious performance issues. First, these interpreters commonly implement AST nodes by leveraging class inheritance and polymorphism, leading to many polymorphic call sites in the interpreter implementation and hence lowering interpreter performance. Second, widely used implementations of these interpreters throw costly runtime exceptions to model the control flow. Even though Just-in-Time (JIT) compilation mitigates these issues, performance in the first stages of the program execution remains poor.

In this paper, we propose a novel technique to improve both interpreter performance and steady-state performance, lowering also the pressure on the JIT compiler. Our technique automatically generates AST supernodes ahead-of-time, i.e., we automatically generate compound AST-node classes that encode the behavior of several other primitive AST nodes before the execution of the application. Our technique extracts common control-flow structures from an arbitrary, given set of ASTs, such as e.g. the functions of popular packages. It is based on matchmaking of AST structures, instantiation of matching supernodes, and replacement of the corresponding AST subtrees with the instantiated supernodes at load-time. We implement our technique in the GraalVM JavaScript engine, showing that our supernodes lead to an average interpreter speedup of 1.24x, an average steady-state speedup of 1.14x, and an average just-in-time compilation speedup of 1.33x on the web-tooling benchmark suite.


title: Generating Constraint Programs for Variability Model Reasoning: A DSL and Solver-Agnostic Approach

authors:
Camilo Correa-Restrepo
Jacques Robin
Raúl Mazo

abstract: Verifying and configuring large Software Product Lines (SPL) requires automation tools. Current state-of-the-art approaches involve translating variability models into a formalism accepted as input by a constraint solver. There are currently no standards for variability modeling languages (VML). There is also a variety of constraint solver input languages. This has resulted in a multiplication of ad-hoc architectures and tools specialized for a single pair of VML and solver, fragmenting the SPL community. To overcome this limitation, we propose a novel architecture based on model-driven code generation, where the syntax and semantics of VMLs can be declaratively specified as data, and a standard, human-readable, formal pivot language is used between the VML and the solver input language. This architecture is the first to be fully generic by being agnostic to both VML and the solver paradigm. To validate the genericity of the approach, we have implemented a prototype tool together with declarative specifications for the syntax and semantics of two different VMLs and two different solver families. One VML is for classic, static SPL, and the other for run-time reconfigurable dynamic SPL with soft constraints to be optimized during configuration. The two solver families are Constraint Satisfaction Programs (CSP) and Constraint Logic Programs (CLP).


title: Partial Evaluation of Automatic Differentiation for Differential-Algebraic Equations Solvers

authors:
Oscar Eriksson
Viktor Palmkvist
David Broman

abstract: Differential-Algebraic Equations (DAEs) are the foundation of high-level equation-based languages for modeling physical dynamical systems. Simulating models in such languages requires a transformation known as index reduction that involves differentiating individual equations before numerical integration. Commercial and open-source implementations typically perform index reduction by symbolic differentiation (SD) and produce a Jacobian callback function with forward-mode automatic differentiation (AD). The former results in efficient runtime code, and the latter is asymptotically efficient in both runtime and code size. However, AD introduces runtime overhead caused by a non-standard representation of real numbers, and SD is not always applicable in models with general recursion. This work proposes a new approach that uses partial evaluation of AD in the context of numerical DAE solving to combine the strengths of the two differentiation methods while mitigating their weaknesses. Moreover, our approach selectively specializes partial derivatives of the Jacobian by exploiting structural knowledge while respecting a user-defined bound on the code size. Our evaluation shows that the new method both enables expressive modeling from AD and retains the efficiency of SD for many practical applications.


title: Generating Conforming Programs with Xsmith

authors:
William Gallard Hatch
Pierce Darragh
Sorawee Porncharoenwase
Guy Watson
Eric Eide

abstract:
Fuzz testing is an effective tool for finding bugs in software, including programming language compilers and interpreters. Advanced fuzz testers can find deep semantic bugs in language implementations through differential testing. However, input programs used for differential testing must not only be syntactically and semantically valid, but also be free from nondeterminism and undefined behaviors. Developing a fuzzer that produces such programs can require tens of thousands of lines of code and hundreds of person-hours. Despite this significant investment, fuzzers designed for differential testing of different languages include many of the same features and analyses in their implementations. To make the implementation of language fuzz testers for differential testing easier, we introduce Xsmith.

Xsmith is a Racket library and domain-specific language that provides mechanisms for implementing a fuzz tester in only a few hundred lines of code. By sharing infrastructure, allowing declarative language specification, and by allowing procedural extensions, Xsmith allows developers to write correct fuzzers for differential testing with little effort. We have developed fuzzers for several languages, and found bugs in implementations of Racket, Dafny, Standard ML, and WebAssembly.


title: A pred-LL(*) Parsable Typed Higher-Order Macro System for Architecture Description Languages

authors:
Christoph Hochrainer
Andreas Krall

abstract: Macro systems are powerful language extension tools for Architecture Description Languages (ADLs). Their generative power in combination with the simplicity of specification languages allows for a substantial reduction of repetitive specification sections. This paper explores how the introduction of function- and record types in a template-based macro system impacts the specification of ADLs. We present design and implementation of a pattern-based syntax macro system for the Vienna Architecture Description Language (VADL). The macro system is directly integrated into the language and is analyzed at parse time using a context-sensitive pred-LL(*) parser. The usefulness of the macro system is illustrated by some typical macro application design patterns. The effectiveness is shown by a detailed evaluation of the Instruction Set Architecture (ISA) specification of five different processor architectures. The observed specification reduction can be up to 90 times, leading to improved maintainability, readability and runtime performance of the specifications.


title: Virtual Domain Specific Languages via Embedded Projectional Editing

authors:
Niklas Korz
Artur Andrzejak

abstract:
Domain Specific Languages (DSLs) can be implemented as either internal DSL, i.e. essentially a library in a host general-purpose programming language (GPL), or as external DSL which is a stand-alone language unconstrained in its syntax. This choice implies an inherent trade-off between a limited syntactic and representational flexibility (internal DSLs), or an involved integration with GPLs and the need for a full stack of tools from a parser to a code generator (external DSLs).

We propose a solution which addresses this problem by representing a subset of a GPL - from simple code patterns to complex API calls - as GUI widgets in a hybrid editor. Our approach relies on matching parametrized patterns against the GPL program, and displaying the matched parts as dynamically rendered widgets. Such widgets can be interpreted as components of an external DSL. Since the source code is serialized as GPL text without annotations, there is no DSL outside the editor - hence the term ‘virtual’ DSL.

This solution has several advantages. The underlying GPL and the virtual DSL can be mixed in a compositional way, with zero cost of their integration. The project infrastructure does not need to be adapted. Furthermore, our approach works with mainstream GPLs like Python or JavaScript.

To lower the development effort of such virtual DSLs, we also propose an approach to generate patterns and the corresponding text-only GUI widgets from pairs of examples.

We evaluate our approach and its implementation on use cases from several domains. A live demo of the system can be accessed at https://puredit.korz.dev/ and the source code with examples at https://github.com/niklaskorz/puredit/.


title: C2TACO: Lifting Tensor Code to TACO

authors:
José Wesley de Souza Magalhães
Jackson Woodruff
Elizabeth Polgreen
Michael F. P. O'Boyle

abstract:
Domain-specific languages (DSLs) promise a significant performance and portability advantage over traditional languages. DSLs are designed to be high-level and platform-independent, allowing an optimizing compiler significant leeway when targeting a particular device. Such languages are particularly popular with emerging tensor algebra workloads. However, DSLs present their own challenge: they require programmers to learn new programming languages and put in significant effort to migrate legacy code.

We present C2TACO, a synthesis tool for synthesizing TACO, a well-known tensor DSL, from C code. We develop a smart, enumerative synthesizer that uses automatically generated IO examples and source-code analysis to efficiently generate code. C2TACO is able to synthesize 95% bench marks from a tensor benchmark suite, out-performing an alternative neural machine translation technique, and demonstrates substantially higher levels of accuracy when evaluated against two state-of-the-art existing schemes, TF-Coder and ChatGPT. Our synthesized TACO programs are, by design, portable achieving significant performance improvement when evaluated on a multi-core and GPU platform.


title: Unleashing the Power of Implicit Feedback in Software Product Lines: Benefits Ahead

authors:
Raul Medeiros
Oscar Díaz
David Benavides

abstract: Software Product Lines (SPLs) facilitate the development of a complete range of software products through systematic reuse. Reuse involves not only code but also the transfer of knowledge gained from one product to others within the SPL. This transfer includes bug fixing, which, when encountered in one product, affects the entire SPL portfolio. Similarly, feedback obtained from the usage of a single product can inform beyond that product to impact the entire SPL portfolio. Specifically, implicit feedback refers to the automated collection of data on software usage or execution, which allows for the inference of customer preferences and trends. While implicit feedback is commonly used in single-product development, its application in SPLs has not received the same level of attention. This paper promotes the investigation of implicit feedback in SPLs by identifying a set of SPL activities that can benefit the most from it. We validate this usefulness with practitioners using a questionnaire-based approach (n=8). The results provide positive insights into the advantages and practical implications of adopting implicit feedback at the SPL level.


title: A Monadic Framework for Name Resolution in Multi-phased Type Checkers

authors:
Casper Bach Poulsen
Aron Zwaan
Paul Hübner

abstract:
An important aspect of type checking is name resolution --- i.e., determining the types of names by resolving them to a matching declaration. For most languages, we can give typing rules that define name resolution in a way that abstracts from what order different units of code should be checked in. However, implementations of type checkers in practice typically use multiple phases to ensure that declarations of resolvable names are available before names are resolved. This gives rise to a gap between typing rules that abstract from order of type checking and multi-phased type checkers that rely on explicit ordering.

This paper introduces techniques that reduce this gap. First, we introduce a monadic interface for phased name resolution which detects and rejects type checking runs with name resolution phasing errors where names were wrongly resolved because some declarations were not available when they were supposed to be. Second, building on recent work by Gibbons et al., we use applicative functors to compositionally map abstract syntax trees onto (phased) monadic computations that represent typing constraints. These techniques reduce the gap between type checker implementations and typing rules in the sense that (1) both are given by compositional mappings over abstract syntax trees, and (2) type checker cases consist of computations that roughly correspond to typing rule premises, except these are composed using monadic combinators. We demonstrate our approach by implementing type checkers for Mini-ML with Damas-Hindley-Milner type inference, and LM, a toy module language with a challenging import resolution policy.


title: Multi-Stage Vertex-Centric Programming for Agent-Based Simulations

abstract:
In vertex-centric programming, users express a graph algorithm as a vertex program and specify the iterative behavior of a vertex in a compute function, which is executed by all vertices in a graph in parallel, synchronously in a sequence of supersteps. While this programming model is straightforward for simple algorithms where vertices behave the same in each superstep, for complex vertex programs where vertices have different behavior across supersteps, a vertex needs to frequently dispatch on the value of supersteps in compute, which suffers from unnecessary interpretation overhead and complicates the control flow.

We address this using meta-programming: instead of branching on the value of a superstep, users separate instructions that should be executed in different supersteps via a staging-time wait() instruction. When a superstep starts, computations in a vertex program resume from the last execution point, and continue executing until the next wait(). We implement this in the programming model of an agent-based simulation framework CloudCity and show that avoiding the interpretation overhead caused by dispatching on the value of a superstep can improve the performance by up to 25% and lead to more robust performance.