arXiv subjects

Philipp Haller

Publications and source records attributed to Philipp Haller.

At least 19 recordsLinked to original sources

arXiv2026

Where did we fail? -- Reproducing build failures in embedded open source software

Due to hardware-software co-development in embedded systems, continuous integration (CI) builds frequently fail because of complex cross-compilation, board configurations, and toolchain constraints. Although CI build logs contain valuable diagnostic information, they are short-lived and difficult to reuse due to heterogeneous runners, toolchains, and log formats. To address these challenges, we present PhantomRun, a unified abstraction layer and publicly reusable dataset that standardizes the retrieval, storage, and reproduction of CI build logs and metadata. Across 4628 failing CI runs, we reconstructed 91.8% of builds and preserved execution outcomes in 98% of evaluated cases. PhantomRun provides two core capabilities: retrieving the build log of any commit and faithfully re-executing the corresponding build in a controlled environment. By exposing all build artifacts and metadata in a uniform, machine-readable format, PhantomRun enables reproducible and longitudinal studies of CI failures. An empirical evaluation shows that reproduced builds closely match their originals, typically differing only in timestamps or minor nondeterministic reordering, demonstrating the feasibility of large-scale historical CI reconstruction.

cs.SE↗

arXiv2026

JoinActors: A Modular Library for Actors with Join Patterns

Join patterns are a high-level programming construct for message-passing applications. They offer an intuitive and declarative approach for specifying how concurrent and distributed components coordinate, possibly depending on complex conditions over combinations of messages. Join patterns have inspired many implementations -- but most of them are not available as libraries: rather, they are domain-specific languages that can be hard to integrate into pre-existing ecosystems. Moreover, all implementations ship with a predefined matching algorithm, which may not be optimal depending on the application requirements. These limitations are addressed by `JoinActors`, a recently published library which integrates join patterns in the off-the-shelf Scala 3 programming language, and is designed to be modular w.r.t. the matching algorithm in use. In this work we address the problem of designing, developing, and evaluating a modular join pattern matching toolkit that (1) can be used as a regular library with a developer-friendly syntax within a pre-existing programming language, and (2) has an extensible design that supports the use and comparison of different matching algorithms. We analyse how `JoinActors` achieves goals (1) and (2) above. The paper that introduced `JoinActors` only briefly outlined its design and implementation (as its main goal was formalising its novel fair matching semantics*). In this work we present and discuss in detail an improved version of `JoinActors`, focusing on its use of metaprogramming (which enables an intuitive API resembling standard pattern matching) and on its modular design. We show how this enables the integration of multiple matching algorithms with different optimisations and we evaluate their performance via benchmarks covering different workloads. We illustrate a sophisticated use of Scala 3's metaprogramming for the integration of an advanced concurrent programming construct within a pre-existing language. In addition, we discuss the insights and "lessons learned" in optimising join pattern matching, and how they are facilitated by `JoinActors`'s modularity -- which allows for the systematic comparison of multiple matching algorithm implementations. We adopt the fair join pattern matching semantics and the benchmark suite from the paper that originally introduced `JoinActors`. Through extensive testing we ensure that our new optimised matching algorithms produce exactly the same matches as the original `JoinActors` library, while achieving significantly better performance. The improved version of `JoinActors` is the companion artifact of this paper. This work showcases the expressiveness, effectiveness, and usability of join patterns for implementing complex coordination patterns in distributed message-passing systems, within a pre-existing language. It also demonstrates promising performance results, with significant improvements over previous work. Besides the practical promise, `JoinActors`'s modular design offers a research playground for exploring and comparing new join pattern matching algorithms, possibly based on entirely different semantics.

cs.PL↗

arXiv2026

PhantomRun: Auto Repair of Compilation Errors in Embedded Open Source Software

Continuous Integration (CI) pipelines for embedded software sometimes fail during compilation, consuming significant developer time for debugging. We study four major open-source embedded system projects, spanning over 4000 build failures from the project's CI runs. We find that hardware dependencies account for the majority of compilation failures, followed by syntax errors and build-script issues. Most repairs need relatively small changes, making automated repair potentially suitable as long as the diverse setups and lack of test data can be handled. In this paper, we present PhantomRun, an automated framework that leverages large language models (LLMs) to generate and validate fixes for CI compilation failures. The framework addresses the challenge of diverse build infrastructures and tool chains across embedded system projects by providing an adaptation layer for GitHub Actions and GitLab CI and four different build systems. PhantomRun utilizes build logs, source code, historical fixes, and compiler error messages to synthesize fixes using LLMs. Our evaluations show that PhantomRun successfully repairs up to 45% of CI compilation failures across the targeted projects, demonstrating the viability of LLM-based repairs for embedded-system CI pipelines.

cs.SE↗

arXiv2025

Holon Streaming: Global Aggregations with Windowed CRDTs

Scaling global aggregations is a challenge for exactly-once stream processing systems. Current systems implement these either by computing the aggregation in a single task instance, or by static aggregation trees, which limits scalability and may become a bottleneck. Moreover, the end-to-end latency is determined by the slowest path in the tree, and failures and reconfiguration cause large latency spikes due to the centralized coordination. Towards these issues, we present Holon Streaming, an exactly-once stream processing system for global aggregations. Its deterministic programming model uses windowed conflict-free replicated data types (Windowed CRDTs), a novel abstraction for shared replicated state. Windowed CRDTs make computing global aggregations scalable. Furthermore, their guarantees such as determinism and convergence enable the design of efficient failure recovery algorithms by decentralized coordination. Our evaluation shows a 5x lower latency and 2x higher throughput than an existing stream processing system on global aggregation workloads, with an 11x latency reduction under failure scenarios. The paper demonstrates the effectiveness of decentralized coordination with determinism, and the utility of Windowed CRDTs for global aggregations.

cs.DC↗

arXiv2025

Auto-repair without test cases: How LLMs fix compilation errors in large industrial embedded code

The co-development of hardware and software in industrial embedded systems frequently leads to compilation errors during continuous integration (CI). Automated repair of such failures is promising, but existing techniques rely on test cases, which are not available for non-compilable code. We employ an automated repair approach for compilation errors driven by large language models (LLMs). Our study encompasses the collection of more than 40000 commits from the product's source code. We assess the performance of an industrial CI system enhanced by four state-of-the-art LLMs, comparing their outcomes with manual corrections provided by human programmers. LLM-equipped CI systems can resolve up to 63 % of the compilation errors in our baseline dataset. Among the fixes associated with successful CI builds, 83 % are deemed reasonable. Moreover, LLMs significantly reduce debugging time, with the majority of successful cases completed within 8 minutes, compared to hours typically required for manual debugging.

cs.SE↗

arXiv2024

Failure Transparency in Stateful Dataflow Systems (Technical Report)

Failure transparency enables users to reason about distributed systems at a higher level of abstraction, where complex failure-handling logic is hidden. This is especially true for stateful dataflow systems, which are the backbone of many cloud applications. In particular, this paper focuses on proving failure transparency in Apache Flink, a popular stateful dataflow system. Even though failure transparency is a critical aspect of Apache Flink, to date it has not been formally proven. Showing that the failure transparency mechanism is correct, however, is challenging due to the complexity of the mechanism itself. Nevertheless, this complexity can be effectively hidden behind a failure transparent programming interface. To show that Apache Flink is failure transparent, we model it in small-step operational semantics. Next, we provide a novel definition of failure transparency based on observational explainability, a concept which relates executions according to their observations. Finally, we provide a formal proof of failure transparency for the implementation model; i.e., we prove that the failure-free model correctly abstracts from the failure-related details of the implementation model. We also show liveness of the implementation model under a fair execution assumption. These results are a first step towards a verified stack for stateful dataflow systems.

cs.PL↗

arXiv2024

In industrial embedded software, are some compilation errors easier to localize and fix than others?

Industrial embedded systems often require specialized hardware. However, software engineers have access to such domain-specific hardware only at the continuous integration (CI) stage and have to use simulated hardware otherwise. This results in a higher proportion of compilation errors at the CI stage than in other types of systems, warranting a deeper study. To this end, we create a CI diagnostics solution called ``Shadow Job'' that analyzes our industrial CI system. We collected over 40000 builds from 4 projects from the product source code and categorized the compilation errors into 14 error types, showing that the five most common ones comprise 89 % of all compilation errors. Additionally, we analyze the resolution time, size, and distance for each error type, to see if different types of compilation errors are easier to localize or repair than others. Our results show that the resolution time, size, and distance are independent of each other. Our research also provides insights into the human effort required to fix the most common industrial compilation errors. We also identify the most promising directions for future research on fault localization.

cs.SE↗

arXiv2024

Behavioural Types for Heterogeneous Systems (Position Paper)

Behavioural types provide a promising way to achieve lightweight, language-integrated verification for communication-centric software. However, a large barrier to the adoption of behavioural types is that the current state of the art expects software to be written using the same tools and typing discipline throughout a system, and has little support for components over which a developer has no control. This position paper describes the outcomes of a working group discussion at Dagstuhl Seminar 24051 (Next-Generation Protocols for Heterogeneous Systems). We propose a methodology for integrating multiple behaviourally-typed components, written in different languages. Our proposed approach involves an extensible protocol description language, a session IR that can describe data transformations and boundary monitoring and which can be compiled into program-specific session proxies, and finally a session middleware to aid session establishment. We hope that this position paper will stimulate discussion on one of the most pressing challenges facing the widespread adoption of behavioural typing.

cs.PL↗

arXiv2023

P4R-Type: a Verified API for P4 Control Plane Programs (Technical Report)

Software-Defined Networking (SDN) significantly simplifies programming, reconfiguring, and optimizing network devices, such as switches and routers. The de facto standard for programmming SDN devices is the P4 language. However, the flexibility and power of P4, and SDN more generally, gives rise to important risks. As a number of incidents at major cloud providers have shown, errors in SDN programs can compromise the availability of networks, leaving them in a non-functional state. The focus of this paper are errors in control-plane programs that interact with P4-enabled network devices via the standardized P4Runtime API. For clients of the P4Runtime API it is easy to make mistakes that lead to catastrophic failures, despite the use of Google's Protocol Buffers as an interface definition language. This paper proposes P4R-Type, a novel verified P4Runtime API for Scala that performs static checks for P4 control plane operations, ruling out mismatches between P4 tables, allowed actions, and action parameters. As a formal foundation of P4R-Type, we present the $F_{\text{P4R}}$ calculus and its typing system, which ensure that well-typed programs never get stuck by issuing invalid P4Runtime operations. We evaluate the safety and flexibility of P4R-Type with 3 case studies. To the best of our knowledge, this is the first work that formalises P4Runtime control plane applications, and a typing discipline ensuring the correctness of P4Runtime operations.

cs.PL↗

arXiv2022

Expression Acceleration: Seamless Parallelization of Typed High-Level Languages

Efficient parallelization of algorithms on general-purpose GPUs is essential in many areas today. However, it is a non-trivial task for software engineers to utilize GPUs to improve the performance of high-level programs in general. Although many domain-specific approaches are available for GPU acceleration, it is difficult to accelerate existing high-level programs without rewriting parts of the programs using low-level GPU code. We present a compiler implementation using an alternative approach called expression acceleration. This approach marks expressions for acceleration, and the compiler automatically infers which dependent code needs to be accelerated. We design and implement a compiler supporting expression acceleration for a statically typed functional language and evaluate its applicability and performance.

cs.PL↗

arXiv2019

Resolvable Ambiguity

A common standpoint when designing the syntax of programming languages is that the grammar definition has to be unambiguous. However, requiring up front unambiguous grammars can force language designers to make more or less arbitrary choices to disambiguate the language. In this paper, we depart from the traditional view of unambiguous grammar design, and enable the detection of ambiguities to be delayed until parse time, allowing the user of the language to perform the disambiguation. A natural decision problem follows: given a language definition, can a user always disambiguate an ambiguous program? We introduce and formalize this fundamental problem - called the resolvable ambiguity problem - and divide it into separate static and dynamic resolvability problems. We provide solutions to the static problem for a restricted language class and sketch proofs of soundness and completeness. We also provide a sound and complete solution to the dynamic problem for a much less restricted class of languages. The approach is evaluated through two separate case studies, covering both a large existing programming language, and the composability of domain-specific languages.

cs.FL↗

arXiv2019

Consistency types for replicated data in a higher-order distributed programming language

Distributed systems address the increasing demand for fast access to resources and fault tolerance for data. However, due to scalability requirements, software developers need to trade consistency for performance. For certain data, consistency guarantees may be weakened if application correctness is unaffected. In contrast, data flow from data with weak consistency to data with strong consistency requirements is problematic, since application correctness may be broken. In this paper, we propose lattice-based consistency types for replicated data (CTRD), a higher-order static consistency-typed language with replicated data types. The type system of CTRD supports shared data among multiple clients, and statically enforces noninterference between data types with weaker consistency and data types with stronger consistency. The language can be applied to many distributed applications and guarantees that updates of weakly-consistent data can never affect strongly-consistent data. We also extend the basic CTRD with an optimization that reduces synchronization for generating reference graphs.

cs.PL↗

arXiv2018

A Chaos Engineering System for Live Analysis and Falsification of Exception-handling in the JVM

Software systems contain resilience code to handle those failures and unexpected events happening in production. It is essential for developers to understand and assess the resilience of their systems. Chaos engineering is a technology that aims at assessing resilience and uncovering weaknesses by actively injecting perturbations in production. In this paper, we propose a novel design and implementation of a chaos engineering system in Java called ChaosMachine. It provides a unique and actionable analysis on exception-handling capabilities in production, at the level of try-catch blocks. To evaluate our approach, we have deployed ChaosMachine on top of 3 large-scale and well-known Java applications totaling 630k lines of code. Our results show that ChaosMachine reveals both strengths and weaknesses of the resilience code of a software system at the level of exception handling.

cs.SE↗

arXiv2018

Observable atomic consistency for CvRDTs

The development of distributed systems requires developers to balance the need for consistency, availability, and partition tolerance. Conflict-free replicated data types (CRDTs) are widely used in eventually consistent systems to reduce concurrency control. However, due to the lack of consistent non-monotonic operations, the usage of CRDTs can be difficult. In this paper, we propose a new consistency protocol, the observable atomic consistency protocol (OACP). OACP enables a principled relax- ation of strong consistency to improve performance in specific scenarios. OACP combines the advantages of mergeable data types, specifically, convergent replicated data types, and reliable total order broadcast to provide on-demand strong consistency. By providing observable atomic consistency, OACP avoids the anomalies of related protocols. We provide a distributed, cluster-enabled implementation of OACP based on Akka, a widely-used actor-based middleware. Our experimental evaluation shows that OACP can reduce the coordination between replicas compared to other protocols providing atomic consistency in several bench- marks. Our results also suggest that OACP gains availability through mergeable data types and provides acceptable latency for achieving strong consistency.

cs.DC↗

arXiv2017

Towards an Empirical Study of Affine Types for Isolated Actors in Scala

LaCasa is a type system and programming model to enforce the object capability discipline in Scala, and to provide affine types. One important application of LaCasa's type system is software isolation of concurrent processes. Isolation is important for several reasons including security and data-race freedom. Moreover, LaCasa's affine references enable efficient, by-reference message passing while guaranteeing a "deep-copy" semantics. This deep-copy semantics enables programmers to seamlessly port concurrent programs running on a single machine to distributed programs running on large-scale clusters of machines. This paper presents an integration of LaCasa with actors in Scala, specifically, the Akka actor-based middleware, one of the most widely-used actor systems in industry. The goal of this integration is to statically ensure the isolation of Akka actors. Importantly, we present the results of an empirical study investigating the effort required to use LaCasa's type system in existing open-source Akka-based systems and applications.

cs.PL↗

arXiv2017

Quantifying and Explaining Immutability in Scala

Functional programming typically emphasizes programming with first-class functions and immutable data. Immutable data types enable fault tolerance in distributed systems, and ensure process isolation in message-passing concurrency, among other applications. However, beyond the distinction between reassignable and non-reassignable fields, Scala's type system does not have a built-in notion of immutability for type definitions. As a result, immutability is "by-convention" in Scala, and statistics about the use of immutability in real-world Scala code are non-existent. This paper reports on the results of an empirical study on the use of immutability in several medium-to-large Scala open-source code bases, including Scala's standard library and the Akka actor framework. The study investigates both shallow and deep immutability, two widely-used forms of immutability in Scala. Perhaps most interestingly, for type definitions determined to be mutable, explanations are provided for why neither the shallow nor the deep immutability property holds; in turn, these explanations are aggregated into statistics in order to determine the most common reasons for why type definitions are mutable rather than immutable.

cs.PL↗

arXiv2017

Proceedings Tenth Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software

PLACES 2017 (full title: Programming Language Approaches to Concurrency- and Communication-cEntric Software) is the tenth edition of the PLACES workshop series. After the first PLACES, which was affiliated to DisCoTec in 2008, the workshop has been part of ETAPS every year since 2009 and is now an established part of the ETAPS satellite events. PLACES 2017 was held on 29th April in Uppsala, Sweden. The workshop series was started in order to promote the application of novel programming language ideas to the increasingly important problem of developing software for systems in which concurrency and communication are intrinsic aspects. This includes software for both multi-core systems and large-scale distributed and/or service-oriented systems. The scope of PLACES includes new programming language features, whole new programming language designs, new type systems, new semantic approaches, new program analysis techniques, and new implementation mechanisms. This volume consists of the papers accepted for presentation at the workshop.

cs.PL↗

arXiv2016

Object Capabilities and Lightweight Affinity in Scala: Implementation, Formalization, and Soundness

Aliasing is a known source of challenges in the context of imperative object-oriented languages, which have led to important advances in type systems for aliasing control. However, their large-scale adoption has turned out to be a surprisingly difficult challenge. While new language designs show promise, they do not address the need of aliasing control in existing languages. This paper presents a new approach to isolation and uniqueness in an existing, widely-used language, Scala. The approach is unique in the way it addresses some of the most important obstacles to the adoption of type system extensions for aliasing control. First, adaptation of existing code requires only a minimal set of annotations. Only a single bit of information is required per class. Surprisingly, the paper shows that this information can be provided by the object-capability discipline, widely-used in program security. We formalize our approach as a type system and prove key soundness theorems. The type system is implemented for the full Scala language, providing, for the first time, a sound integration with Scala's local type inference. Finally, we empirically evaluate the conformity of existing Scala open-source code on a corpus of over 75,000 LOC.

cs.PL↗