Dr. Pascal Weisenburger
pascal.weisenburger@unisg.ch
0000-0003-1288-1485
pweisenburger

School of Computer Science
Torstrasse 25
9000 St. Gallen, Switzerland

My current research focuses on the design of languages for distributed systems with a wide range of software architectures – e.g., peer-to-peer, cloud, edge, serverless, IoT – regarding areas such as sound programming models for the interaction between components, their composition, privacy protection issues, type systems for reasoning about the placement of data and computation.

Within the MAKI project, I worked on complex event processing (CEP) and multitier languages for developing modular distributed applications. I’m the main developer of the ScalaLoci multitier programming language.

I served on the following committees:

• APLAS ’25 (PC)
• ECOOP ’25 (PC)
• ECOOP ’24 (Web Chair)
• OOPSLA ’23 (PC)
• ECOOP ’23 (AEC, ERC, Web Co-Chair)
• ‹Programming› ’23 (AEC)
• REBLS ’22 (Chair) at SPLASH ’22
• Workshop on Real-time Stream Analytics, Stream Mining, CER/CEP & Stream Data Management in Big Data ’22 (PC) at IEEE BigData
• ECOOP ’22 (AEC, ERC).
• Demos and posters (Co-Chair) at IoT ’21
• Workshop on Real-time Stream Analytics, Stream Mining, CER/CEP & Stream Data Management in Big Data ’21 (PC) at IEEE BigData
• REBLS ’21 (PC) at SPLASH
• ProWeb ’20 (PC) at ‹Programming›

Short Bio

I got my PhD from the Departement of Computer Science at the Technical University of Darmstadt under the supervision of Prof. Guido Salvaneschi in 2020. My doctoral dissertation focuses on multitier programming for developing distributed software systems. I worked as a postdoc with Prof. Mira Mezini at the Technical University of Darmstadt until spring 2021. I joined the Programming Group at the University of St. Gallen in May 2021.

Publications

1. POPL
   Propel
   

   Dis/Equality Graphs

   George Zakhour, Pascal Weisenburger, Jahrim Gabriele Cesario, Guido Salvaneschi

   Proceedings of the ACM on Programming Languages 8 (POPL), 2025

   Abstract PDF Supp

   E-graphs are a data structure to compactly represent a program space and reason about equality of program terms. E-graphs have been successfully applied to a number of domains, including program optimization and automated theorem proving. In many applications, however, it is necessary to reason about disequality of terms as well as equality. While disequality reasoning can be encoded, direct support for disequalities increases performance and simplifies the metatheory.

   In this paper, we develop a framework independent of a specific implementation to formally reason about e-graphs. For the first time, we prove the equivalence of e-graphs to the reflexive, symmetric, transitive, and congruent closure of the equivalence relation they are expected to encode. We use these results to present the first formalization of an extension of e-graphs that directly supports disequalities and prove an analytical result about their superior efficiency compared to embedding techniques that are commonly used in SMT solvers and automated verifiers. We further profile an SMT solver and find that it spends a measurable amount of time handling disequalities.

   We implement our approach in an extension to egg, a popular e-graph Rust library. We evaluate our solution in an SMT solver and an automated theorem prover using standard benchmarks. The results indicate that direct support for disequalities outperforms other encodings based on equality embedding, confirming the results obtained analytically.

2. TSE
   

   Consistent Local-First Software: Enforcing Safety and Invariants for Local-First Applications

   Mirko Köhler, George Zakhour, Pascal Weisenburger, Guido Salvaneschi

   IEEE Transactions on Software Engineering, 2024

   Abstract PDF

   Local-first software embraces data replication as a means to achieve scalability and offline availability. A crucial ingredient of local-first software are mergeable data types, like conflict-free replicated data types (CRDTs), which feature eventual consistency by enabling processes to access data locally and later merge it with other replicas in an asynchronous manner. Notably, the merging process needs to adhere to application constraints for correctness. Ensuring such application-level invariants poses a challenge, as developers must reason about the replicated program state and resort to manual synchronization of specific application components to enforce the invariant.

   This paper introduces ConLoc (Consistent Local-First Software), a novel system designed to automatically enforce safety and maintain invariants in local-first applications. ConLoc effectively addresses the issue of preserving invariants in the execution of programs with replicated data types, including CRDTs. Our approach is able to verify the correctness of many CRDTs examined in the literature and in implementations, such the ones used in the Riak database. ConLoc ensures that applications are automatically synchronized correctly, resulting in substantial latency and throughput improvements when compared to sequential execution, while upholding the same set of invariants.

3. ECOOP
   

   Compiling with Arrays

   David Richter, Timon Böhler, Pascal Weisenburger, Mira Mezini

   In Proceedings of the 38th European Conference on Object-Oriented Programming (ECOOP), Leibniz International Proceedings in Informatics (LIPIcs), 2024

   Abstract PDF Supp

   Linear algebra computations are foundational for neural networks and machine learning, often handled through arrays. While many functional programming languages feature lists and recursion, arrays in linear algebra demand constant-time access and bulk operations. To bridge this gap, some languages represent arrays as (eager) functions instead of lists. In this paper, we connect this idea to a formal logical foundation by interpreting functions as the usual negative types from polarized type theory, and arrays as the corresponding dual positive version of the function type. Positive types are defined to have a single elimination form whose computational interpretation is pattern matching. Just like (positive) product types bind two variables during pattern matching, (positive) array types bind variables with multiplicity during pattern matching. We follow a similar approach for Booleans by introducing conditionally-defined variables.

   The positive formulation for the array type enables us to combine typed partial evaluation and common subexpression elimination into an elegant algorithm whose result enjoys a property we call maximal fission, which we argue can be beneficial for further optimizations. For this purpose, we present the novel intermediate representation indexed administrative normal form (AiNF), which relies on the formal logical foundation of the positive formulation for the array type to facilitate maximal loop fission and subsequent optimizations. AiNF is normal with regard to commuting conversion for both let-bindings and for-loops, leading to flat and maximally fissioned terms. We mechanize the translation and normalization from a simple surface language to AiNF, establishing that the process terminates, preserves types, and produces maximally fissioned terms.

4. PLDI
   Propel
   

   Automated Verification of Fundamental Algebraic Laws

   George Zakhour, Pascal Weisenburger, Guido Salvaneschi

   Proceedings of the ACM on Programming Languages 8 (PLDI), 2024

   Abstract PDF Supp Code Website

   Algebraic laws of functions in mathematics – such as commutativity, associativity, and idempotence – are often used as the basis to derive more sophisticated properties of complex mathematical structures and are heavily used in abstract computational thinking. Algebraic laws of functions in coding, however, are rarely considered. Yet, they are essential. For example, commutativity and associativity are crucial to ensure correctness of a variety of software systems in numerous domains, such as compiler optimization, big data processing, data flow processing, machine learning or distributed algorithms and data structures. Still, most programming languages lack built-in mechanisms to enforce and verify that operations adhere to such properties.

   In this paper, we propose a verifier specialized on a set of fundamental algebraic laws that ensures that such laws hold in application code. The verifier can conjecture auxiliary properties and can reason about both equalities and inequalities of expressions, which is crucial to prove a given property when other competitors do not succeed. We implement these ideas in the Propel verifier. Our evaluation against five state-of-the-art verifiers on a total of 142 instances of algebraic properties shows that Propel is able to automatically deduce algebraic properties in different domains that rely on such properties for correctness, even in cases where competitors fail to verify the same properties or time out.

5. EGRAPHS
   Propel
   

   Disequalities in E-Graphs: An Experiment

   George Zakhour, Pascal Weisenburger, Guido Salvaneschi

   Presentation at the 3rd Workshop on E-Graph Research, Applications, Practices, and Human-factors (EGRAPHS), 2024

   Abstract PDF

   This talk explores the integration of disequalities into e-graphs for enhancing the efficiency of automated theorem provers. We discuss two existing approaches, which we implement in the egg e-graph library, presenting preliminary results on comparing their effectiveness. Our initial experiments demonstrate the feasibility of integrating disequalities into e-graphs implemented in egg, with promising results suggesting improved efficiency in the proof search algorithm. We plan to refine this approach, integrate it into our Propel automated theorem prover, and make our extensions to egg available to the research community.

6. CP
   ScalaLoci
   

   Exploring Algebraic Placement in Multiparty Languages

   George Zakhour, Pascal Weisenburger, Guido Salvaneschi

   Presentation at the 1st Workshop on Choreographic Programming (CP), 2024

   Abstract PDF

   This talk provides an overview of our ongoing research on the relationship between type systems and placement systems in programming languages for distributed systems.

   In distributed systems, the placement of data and computation plays a crucial role in ensuring protocol correctness, fault tolerance, security of information flow, and performance optimization. Thus, researchers have explored various techniques to express and manage data placement. Type-based approaches have proven particularly effective in modeling places and their interactions. For example, choreographic programming ensures safe communication protocols across different locations by modeling these locations – so-called roles – types. Similarly, multiparty session types specify a communication protocol for message exchange over communication channels. Recent languages for multitier programming – a programming paradigm that provides language abstractions to specify the placement of data and computations on the different components of the distributed system – also opted for expressing placement in the type system.

   Reification of placements into language-level concepts enables programmers to reason about which components perform computations and about the communication between them.

7. LNCS
   ScalaLoci
   

   Bridging Between Active Objects: Multitier Programming for Distributed, Concurrent Systems

   Guido Salvaneschi, Pascal Weisenburger

   In Active Object Languages: Current Research Trends, Lecture Notes in Computer Science, 2024

   Abstract PDF

   Programming distributed and concurrent systems is notoriously hard. Active objects, which encapsulate operations, state and control flow, have been investigated by researchers to alleviate this issue. In a distributed system, message exchange among active objects or actors often coincides with network boundaries, and determines a major modularization direction for the application. Yet, certain application functionalities naturally crosscut such modularization direction. For those, structuring the application architecture around network boundaries is purely accidental and does not help reasoning about programs.

   Recently, multitier programming has been proposed as a programming paradigm that enables code that belongs to different peers to be developed together, in the same compilation unit. The compiler then splits the code and generates the required deployment components.

   In this work we explore the relation between multitier programming and active objects. Multitier programming can be considered a programming paradigm based on active objects with a focus on application domains where functionalities span multiple active objects, and allows such functionalities to be encapsulated into a single object. The multitier approach keeps the asynchronous model of active objects and actors but provides a holistic view of distributed components and their interactions. Multitier programming addresses the use cases where separating components into different active objects or actors hinders encapsulation and modularization across functional boundaries. In such use cases, multitier programming can increase the level of abstraction, improve software design, simplify code maintenance, aid program comprehension and enable formal reasoning. A number of features of active objects are directly visible to programmers also in the multitier programming, resulting in an interesting combination of language abstractions available to developers.

8. PLF
   Propel
   

   Type-Checking CRDTs with Propel

   George Zakhour, Pascal Weisenburger, Guido Salvaneschi

   Presentation at the 2nd Workshop on Programming Local-First Software (PLF), 2023

   Abstract PDF

   Conflict-free Replicated Data Types (CRDTs) are modern distributed data types that allow replicating data to different devices in a distributed system and enable local copies to diverge until they are merged with other replicas ensuring eventual consistency. CRDTs play a vital role in building local-first applications, i.e., applications where devices can always progress their local state independently while also enabling seamless collaboration among devices without being blocked by devices that are (temporarily) unreachable on the network. CRDTs enable keeping replicated data consistent while guaranteeing the absence of conflicts among replicas. CRDTs come in two flavors: state-based and operation-based (op-based). For correct operation, state-based CRDTs rely on a merge function for two states that is commutative, associative and idempotent, while operation-based CRDTs rely on an application function for operations on the state that commutes with itself.

   However ensuring that such algebraic properties are satisfied by implementations is left to the programmer, resulting in a process that is complex and error-prone. While techniques based on testing, automatic verification of models, and mechanized or handwritten proofs are available, we lack an approach that is able to verify such properties on concrete CRDT implementations.

   In this talk the first author will present the first type system that captures the algebraic properties required by a correct CRDT implementation. The type system is designed in Propel, it can reason about programs and derive proofs of such properties with complex rules such as case analysis and induction: sum types guide the case analysis and algebraic properties in function types enable induction. Propel’s key feature is its capacity to reason about algebraic properties (a) in terms of rewrite rules and (b) to derive the equality or inequality of expressions from the properties.

9. OOPSLA
   ScalaLoci
   

   Type-Safe Dynamic Placement with First-Class Placed Values

   George Zakhour, Pascal Weisenburger, Guido Salvaneschi

   Proceedings of the ACM on Programming Languages 7 (OOPSLA2), 2023

   Abstract PDF Supp Code Website

   Several distributed programming language solutions have been proposed to reason about the placement of data, computations, and peers interaction. Such solutions include, among the others, multitier programming, choreographic programming and various approaches based on behavioral types. These methods statically ensure safety properties thanks to a complete knowledge about placement of data and computation at compile time. In distributed systems, however, dynamic placement of computation and data is crucial to enable performance optimizations, e.g., driven by data locality or in presence of a number of other constraints such as security and compliance regarding data storage location. Unfortunately, in existing programming languages, dynamic placement conflicts with static reasoning about distributed programs: the flexibility required by dynamic placement hinders statically tracking the location of data and computation.

   In this paper we present Dyno, a programming language that enables static reasoning about dynamic placement. Dyno features a type system where values are explicitly placed, but in contrast to existing approaches, placed values are also first class, ensuring that they can be passed around and referred to from other locations. Building on top of this mechanism, we provide a novel interpretation of dynamic placement as unions of placement types. We formalize type soundness, placement correctness (as part of type soundness) and architecture conformance. In case studies and benchmarks, our evaluation shows that Dyno enables static reasoning about programs even in presence of dynamic placement, ensuring type safety and placement correctness of programs at negligible performance cost. We reimplement an Android app with 7K LOC in Dyno, find a bug in the existing implementation, and show that the app’s approach is representative of a common way to implement dynamic placement found in over 100 apps in a large open-source app store.

10. TOPLAS
    

    Prisma: A Tierless Language for Enforcing Contract-Client Protocols in Decentralized Applications

    David Richter, David Kretzler, Pascal Weisenburger, Guido Salvaneschi, Sebastian Faust, Mira Mezini

    ACM Transactions on Programming Languages and Systems 45 (3), 2023

    Abstract PDF

    Decentralized applications (dApps) consist of smart contracts that run on blockchains and clients that model collaborating parties. dApps are used to model financial and legal business functionality. Today, contracts and clients are written as separate programs – in different programming languages – communicating via send and receive operations. This makes distributed program flow awkward to express and reason about, increasing the potential for mismatches in the client-contract interface, which can be exploited by malicious clients, potentially leading to huge financial losses.

    In this paper, we present Prisma, a language for tierless decentralized applications, where the contract and its clients are defined in one unit and pairs of send and receive actions that “belong together” are encapsulated into a single direct-style operation, which is executed differently by sending and receiving parties. This enables expressing distributed program flow via standard control flow and renders mismatching communication impossible. We prove formally that our compiler preserves program behavior in presence of an attacker controlling the client code. We systematically compare Prisma with mainstream and advanced programming models for dApps and provide empirical evidence for its expressiveness and performance.

11. ECOOP
    

    A Direct-Style Effect Notation for Sequential and Parallel Programs

    David Richter, Timon Böhler, Pascal Weisenburger, Mira Mezini

    In Proceedings of the 37th European Conference on Object-Oriented Programming (ECOOP), Leibniz International Proceedings in Informatics (LIPIcs), 2023

    Abstract PDF Supp

    Modeling sequential and parallel composition of effectful computations has been investigated in a variety of languages for a long time. In particular, the popular do-notation provides a lightweight effect embedding for any instance of a monad. Idiom bracket notation, on the other hand, provides an embedding for applicatives. First, while monads force effects to be executed sequentially, ignoring potential for parallelism, applicatives do not support sequential effects. Composing sequential with parallel effects remains an open problem. This is even more of an issue as real programs consist of a combination of both sequential and parallel segments. Second, common notations do not support invoking effects in direct-style, instead forcing a rigid structure upon the code.

    In this paper, we propose a mixed applicative/monadic notation that retains parallelism where possible, but allows sequentiality where necessary. We leverage a direct-style notation where sequentiality or parallelism is derived from the structure of the code. We provide a mechanisation of our effectful language in Coq and prove that our compilation approach retains the parallelism of the source program.

12. PLDI
    Propel
    

    Type-Checking CRDT Convergence

    George Zakhour, Pascal Weisenburger, Guido Salvaneschi

    Proceedings of the ACM on Programming Languages 7 (PLDI), 2023

    Abstract PDF Supp Code Website

    Conflict-free Replicated Data Types (CRDTs) are a recent approach for keeping replicated data consistent while guaranteeing the absence of conflicts among replicas. For correct operation, CRDTs rely on a merge function that is commutative, associative and idempotent. Ensuring that such algebraic properties are satisfied by implementations, however, is left to the programmer, resulting in a process that is complex and error-prone. While techniques based on testing, automatic verification of a model, and mechanized or handwritten proofs are available, we lack an approach that is able to verify such properties on concrete CRDT implementations.

    In this paper, we present Propel, a programming language with a type system that captures the algebraic properties required by a correct CRDT implementation. The Propel type system deduces such properties by case analysis and induction: sum types guide the case analysis and algebraic properties in function types enable induction for free. Propel’s key feature is its capacity to reason about algebraic properties (a) in terms of rewrite rules and (b) to derive the equality or inequality of expressions from the properties. We provide an implementation of Propel as a Scala embedding, we implement several CRDTs, verify them with Propel and compare the verification process with four state-of-the-art verification tools. Our evaluation shows that Propel is able to automatically deduce the properties that are relevant for common CRDT implementations found in open-source libraries even in cases in which competitors timeout.

13. IEEE Software
    µs
    

    Decentralizing Infrastructure as Code

    Daniel Sokolowski, Pascal Weisenburger, Guido Salvaneschi

    IEEE Software 40 (1), 2023

    Abstract PDF

    Infrastructure as Code (IaC) automates deployments for single teams, falling short of decentralized deployments across groups. We need mature IaC solutions that embrace and consolidate software engineering principles to enable testing and automation advances for decentralized organizations.

14. ECOOP
    

    Prisma: A Tierless Language for Enforcing Contract-Client Protocols in Decentralized Applications (Extended Abstract)

    David Richter, David Kretzler, Pascal Weisenburger, Guido Salvaneschi, Sebastian Faust, Mira Mezini

    In Proceedings of the 36th European Conference on Object-Oriented Programming (ECOOP), Leibniz International Proceedings in Informatics (LIPIcs), 2022

    Abstract PDF Supp

    Decentralized applications (dApps) consist of smart contracts that run on blockchains and clients that model collaborating parties. dApps are used to model financial and legal business functionality. Today, contracts and clients are written as separate programs – in different programming languages – communicating via send and receive operations. This makes distributed program flow awkward to express and reason about, increasing the potential for mismatches in the client-contract interface, which can be exploited by malicious clients, potentially leading to huge financial losses.

    In this paper, we present Prisma, a language for tierless decentralized applications, where the contract and its clients are defined in one unit and pairs of send and receive actions that “belong together” are encapsulated into a single direct–style operation, which is executed differently by sending and receiving parties. This enables expressing distributed program flow via standard control flow and renders mismatching communication impossible. We prove formally that our compiler preserves program behavior in presence of an attacker controlling the client code. We systematically compare Prisma with mainstream and advanced programming models for dApps and provide empirical evidence for its expressiveness and performance.

15. ICSE
    

    Change Is the Only Constant: Dynamic Updates for Workflows

    Daniel Sokolowski, Pascal Weisenburger, Guido Salvaneschi

    In Proceedings of the 44th International Conference on Software Engineering, ICSE, 2022

    Abstract PDF Supp

    Software systems must be updated regularly to address changing requirements and urgent issues like security-related bugs. Traditionally, updates are performed by shutting down the system to replace certain components. In modern software organizations, updates are increasingly frequent—up to multiple times per day—hence, shutting down the entire system is unacceptable. Safe dynamic software updating (DSU) enables component updates while the system is running by determining when the update can occur without causing errors. Safe DSU is crucial, especially for long-running or frequently executed asynchronous transactions (workflows), e.g., user-interactive sessions and order fulfillment processes. Unfortunately, previous research is limited to synchronous transaction models and does not address this case.

    In this work, we propose a unified model for safe DSU in workflows. We discuss how state-of-the-art DSU solutions fit into this model and show that they incur significant overhead. To improve the performance, we introduce Essential Safety, a novel safe DSU approach that leverages the notion of non-essential changes, i.e., semantics preserving updates. In 106 realistic collaborative BPMN workflows, Essential Safety reduces the delay of workflow completions, on average, by 47.8% compared to the state of the art. We show that the distinction of essential and non-essential changes plays a crucial role in this reduction and that, as suggested in literature, non-essential changes are frequent: at least 60% and often more than 90% of systems’ updates in eight monorepos we analyze.

16. JCSS
    

    TCEP: Transitions in Operator Placement to Adapt to Dynamic Network Environments

    Manisha Luthra, Boris Koldehofe, Niels Danger, Pascal Weisenburger, Guido Salvaneschi, Ioannis Stavrakakis

    Journal of Computer and System Sciences 122, 2021

    Abstract PDF

    Distributed Complex Event Processing (DCEP) is a commonly used paradigm to detect and act on situational changes of many applications, including the Internet of Things (IoT). DCEP achieves this using a simple specification of analytical tasks on data streams called operators and their distributed execution on a set of infrastructure. The adaptivity of DCEP to the dynamics of IoT applications is essential and very challenging in the face of changing demands concerning Quality of Service. In our previous work, we addressed this issue by enabling transitions, which allow for the adaptive use of operator placement mechanisms. In this article, we extend the transition methodology by optimizing the costs of transition and analyzing the behavior using multiple operator placement mechanisms. Furthermore, we provide an extensive evaluation on the costs of transition imposed by operator migrations and learning, as it can inflict overhead on the performance if operated uncoordinatedly.

17. ESEC/FSE
    µs
    

    Automating Serverless Deployments for DevOps Organizations

    Daniel Sokolowski, Pascal Weisenburger, Guido Salvaneschi

    In Proceedings of the 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE, 2021

    Abstract PDF Supp Code

    DevOps unifies software development and operations in cross-functional teams to improve software delivery and operations (SDO) performance. Ideally, cross-functional DevOps teams independently deploy their services, but the correct operation of a service often demands other services, requiring coordination to ensure the correct deployment order. This issue is currently solved either with a central deployment or manual out-of-band communication across teams, e.g., via phone, chat, or email. Unfortunately, both contradict the independence of teams, hindering SDO performance – the reason why DevOps is adopted in the first place.

    In this work, we conduct a study on 73 IT professionals, showing that, in practice, they resort to manual coordination for correct deployments even if they expect better SDO performance with fully automated approaches. To address this issue, we propose μs ([mju:z] “muse”), a novel IaC system automating deployment coordination in a fully decentralized fashion, still retaining compatibility with DevOps practice – in contrast to today’s solutions. We implement µs, demonstrate that it effectively enables automated coordination, introduces negligible definition overhead, has no performance overhead, and is broadly applicable, as shown by the migration of 64 third-party IaC projects.

18. ECOOP
    ScalaLoci
    

    Multiparty Languages: The Choreographic and Multitier Cases

    Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, David Richter, Guido Salvaneschi, Pascal Weisenburger

    In Proceedings of the 35th European Conference on Object-Oriented Programming (ECOOP), Leibniz International Proceedings in Informatics (LIPIcs), 2021

    Abstract PDF

    Choreographic languages aim to express multiparty communication protocols, by providing primitives that make interaction manifest. Multitier languages enable programming computation that spans across several tiers of a distributed system, by supporting primitives that allow computation to change the location of execution. Rooted into different theoretical underpinnings—respectively process calculi and lambda calculus—the two paradigms have been investigated independently by different research communities with little or no contact. As a result, the link between the two paradigms has remained hidden for long.

    In this paper, we show that choreographic languages and multitier languages are surprisingly similar. We substantiate our claim by isolating the core abstractions that differentiate the two approaches and by providing algorithms that translate one into the other in a straightforward way. We believe that this work paves the way for joint research and cross-fertilisation among the two communities.

19. OOPSLA
    ConSysT
    

    Rethinking Safe Consistency in Distributed Object-Oriented Programming

    Mirko Köhler, Nafise Eskandani, Pascal Weisenburger, Alessandro Margara, Guido Salvaneschi

    Proceedings of the ACM on Programming Languages 4 (OOPSLA), 2020

    Abstract PDF

    Large scale distributed systems require to embrace the trade off between consistency and availability, accepting lower levels of consistency to guarantee higher availability. Existing programming languages are, however, agnostic to this compromise, resulting in consistency guarantees that are the same for the whole application and are implicitly adopted from the middleware or hardcoded in configuration files.

    In this paper, we propose to integrate availability in the design of an object-oriented language, allowing developers to specify different consistency and isolation constraints in the same application at the granularity of single objects. We investigate how availability levels interact with object structure and define a type system that preserves correct program behavior. Our evaluation shows that our solution performs efficiently and improves the design of distributed applications.

20. CSUR
    ScalaLoci
    

    A Survey of Multitier Programming

    Pascal Weisenburger, Johannes Wirth, Guido Salvaneschi

    ACM Computing Surveys 53 (4), 2020

    Abstract PDF

    Multitier programming deals with developing the components that pertain to different tiers in the system (e.g., client and server), mixing them in the same compilation unit. In this paradigm, the code for different tiers is then either generated at run time or it results from the compiler splitting the codebase into components that belong to different tiers based on user annotations, static analysis, types, or a combination of these. In the Web context, multitier languages aim at reducing the distinction between client and server code, by translating the code that is to be executed on the clients to JavaScript or by executing JavaScript on the server, too. Ultimately, the goal of the multitier approach is to improve program comprehension, simplify maintenance and enable formal reasoning about the properties of the whole distributed application.

    A number of multitier research languages have been proposed over the last decade, which support various degrees of multitier programming and explore different design tradeoffs. In this article, we provide an overview of the existing solutions, discuss their positioning in the design space, and outline open research problems.

21. ‹Programming›
    ScalaLoci
    

    Implementing a Language for Distributed Systems: Choices and Experiences with Type Level and Macro Programming in Scala

    Pascal Weisenburger, Guido Salvaneschi

    The Art, Science, and Engineering of Programming 4 (3), 2020

    Abstract PDF Code Website

    Multitier programming languages reduce the complexity of developing distributed systems by developing the distributed system in a single coherent code base. The compiler or the runtime separate the code for the components of the distributed system, enabling abstraction over low level implementation details such as data representation, serialization and network protocols. Our ScalaLoci language allows developers to declare the different components and their architectural relation at the type level, allowing static reasoning about about distribution and remote communication and guaranteeing static type safety across components. The compiler splits the multitier program into the component-specific code and automatically generates the communication boilerplate. Communication between components can be modeled by declaratively specifying data flows between components using reactive programming.

    In this paper, we report on the implementation of our design and our experience with embedding our language features into Scala as a host language. We show how a combination of Scala’s advanced type level programming and its macro system can be used to enrich the language with new abstractions. We comment on the challenges we encountered and the solutions we developed for our current implementation and outline suggestions for an improved macro system to support the such use cases of embedding of domain-specific abstractions.

22. ScalaLoci
    

    A Programming Language for Distributed Systems

    Pascal Weisenburger

    Doctoral dissertation, Technische Universität Darmstadt, 2020

    Abstract

    Today’s software, including many everyday services, such as online streaming, search engines and social networks, is widely distributed, running on top of a network of interconnected computers. Such distributed applications are traditionally developed as separate modules for each component in the distributed system. These modules react to events, like user input or messages from the network, and in turn produce new events for the other modules. Separation into different modules is problematic because combining modules is notoriously hard and requires extensive and time-consuming integration and manual implementation of communication forces programmers to program complex event-based communication schemes among hosts ? an activity which is often low-level and error-prone. The combination of the two results in obscure distributed data flows scattered among multiple modules, hindering reasoning about the system as a whole. For these reasons, despite most software today is distributed, the design and development of distributed systems remains surprisingly challenging.

    We present the ScalaLoci distributed programming language, our approach for taming the complexity of developing distributed applications via specialized programming language support. ScalaLoci addresses the issues above with a coherent model based on placement types that enables reasoning about distributed data flows otherwise scattered across multiple modules, supporting multiple software architectures via dedicated language features and abstracting over low-level communication details and data conversions.

    ScalaLoci does not force developers to modularize software along network boundaries as is traditionally the case when developing distributed systems. Instead, we propose a module system that supports encapsulating each (cross-host) functionality and defining it over abstract peer types. As a result, we disentangle modularization and distribution and we enable the definition of a distributed system as a composition of ScalaLoci modules, each representing a subsystem.

    Our case studies on distributed algorithms, distributed data structures, as well as on real-world distributed streaming engines show that ScalaLoci simplifies developing distributed systems, reduces error-prone communication code and favors early detection of bugs. As we demonstrate, the ScalaLoci module system allows the definition of reusable patterns of interaction in distributed software and enables separating the modularization and distribution concerns, properly separating functionalities in distributed systems.

23. REBLS
    

    GRASS: Generic Reactive Application-Specific Scheduling

    Marcel Blöcher, Matthias Eichholz, Pascal Weisenburger, Patrick Eugster, Mira Mezini, Guido Salvaneschi

    In Proceedings of the 6th ACM SIGPLAN International Workshop on Reactive and Event-Based Languages and Systems, REBLS, 2019

    Abstract PDF

    High resource utilization is important to operate compute infrastructures and data centers efficiently. High utilization is achieved by multiplexing several applications over the same physical infrastructure. Yet, with this approach, the different requirements of each application have to be taken into account when scheduling resources.

    We propose GRASS, a reactive domain-specific abstraction that allows specifying application-tailored resource scheduling policies. We demonstrate how the declarative approach of GRASS enables extension and composition of scheduling policies. Our evaluation shows the performance benefits of considering application-specific information in a composition of scheduling policies that adapt at run time.

24. GHTC
    

    Smart Street Lights and Mobile Citizen Apps for Resilient Communication in a Digital City

    Lars Baumgärtner, Jonas Höchst, Patrick Lampe, Ragnar Mogk, Artur Sterz, Pascal Weisenburger, Mira Mezini, Bernd Freisleben

    In Proceedings of the 2019 IEEE Global Humanitarian Technology Conference, GHTC, 2019

    Abstract PDF

    While information and communication technology is crucial for the operation of urban infrastructures and the well-being of its inhabitants, current technology is quite vulnerable to disruptions of various kinds. In future smart cities, a more resilient urban infrastructure is imperative to handle the increasing number of hazardous situations. We present a novel resilient communication approach based on smart street lights as part of the public infrastructure. It supports people in their everyday life and adapts its functionality to the challenges of emergency situations. Our approach relies on various environmental sensors and in-situ processing for automatic situation assessment, and a range of communication mechanisms for maintaining a communication network. Furthermore, resilience is not only achieved based on infrastructure deployed by a digital city’s municipality, but also based on integrating citizens through software that runs on their mobile devices. Web-based zero-installation and platform-agnostic apps can switch to device-to-device communication to continue benefiting people even during a disaster situation. Our approach, featuring a covert channel for professional responders and a zero-installation app, is evaluated through a prototypical implementation based on a commercially available street light.

25. ECOOP
    ScalaLoci
    

    Multitier Modules

    Pascal Weisenburger, Guido Salvaneschi

    In Proceedings of the 33rd European Conference on Object-Oriented Programming (ECOOP), Leibniz International Proceedings in Informatics (LIPIcs), 2019

    Abstract PDF Code Website

    Multitier programming languages address the complexity of developing distributed systems abstracting over low level implementation details such as data representation, serialization and network protocols. Since the functionalities of different peers can be defined in the same compilation unit, multitier languages do not force developers to modularize software along network boundaries. Unfortunately, combining the code for all tiers into the same compilation unit poses a scalability challenge or forces developers to resort to traditional modularization abstractions that are agnostic to the multitier nature of the language.

    In this paper, we address this issue with a module system for multitier languages. Our module system supports encapsulating each (cross-peer) functionality and defining it over abstract peer types. As a result, we disentangle modularization and distribution and we enable the definition of a distributed system as a composition of multitier modules, each representing a subsystem. Our case studies on distributed algorithms, distributed data structures, as well as on the Apache Flink task distribution system, show that multitier modules allow the definition of reusable (abstract) patterns of interaction in distributed software and enable separating the modularization and distribution concerns, properly separating functionalities in distributed systems.

26. DEBS
    ScalaLoci
    

    Tutorial: Developing Distributed Systems with Multitier Programming

    Pascal Weisenburger, Guido Salvaneschi

    In Proceedings of the 13th ACM International Conference on Distributed and Event-Based Systems, DEBS, 2019

    Abstract PDF

    Developing distributed systems is a complex task that requires to program different peers, often using several languages on different platforms, writing communication code and handling data serialization and conversion.

    We show how the multitier programming paradigm can alleviate these issues, supporting a development model where all peers in the system can be written in the same language and coexist in the same compilation units, communication code is automatically inserted by the compiler and the language abstracts over data conversion and serialization. We present multitier programming abstractions, discuss their applicability step by step for the development of small applications and discuss larger case studies on distributed stream processing, like Apache Flink and Apache Gearpump.

27. OOPSLA
    ScalaLoci
    

    Distributed System Development with ScalaLoci

    Pascal Weisenburger, Mirko Köhler, Guido Salvaneschi

    Proceedings of the ACM on Programming Languages 2 (OOPSLA), 2018

    Abstract PDF Code Website

    Distributed applications are traditionally developed as separate modules, often in different languages, which react to events, like user input, and in turn produce new events for the other modules. Separation into components requires time-consuming integration. Manual implementation of communication forces programmers to deal with low-level details. The combination of the two results in obscure distributed data flows scattered among multiple modules, hindering reasoning about the system as a whole. The ScalaLoci distributed programming language addresses these issues with a coherent model based on placement types that enables reasoning about distributed data flows, supporting multiple software architectures via dedicated language features and abstracting over low-level communication details and data conversions. As we show, ScalaLoci simplifies developing distributed systems, reduces error-prone communication code and favors early detection of bugs.

28. FTfJP
    ScalaLoci
    

    Static Latency Tracking with Placement Types

    Pascal Weisenburger, Tobias Reinhard, Guido Salvaneschi

    In Companion Proceedings for the ISSTA/ECOOP 2018 Workshops, ISSTA/ECOOP Companion, 2018

    Abstract PDF

    Large-scale distributed applications, e.g., in geodistributed data centers, pose a performance challenge to developers which need to take high cross-data-center latency communication cost into account. We present a preliminary investigation of a type system that tracks latency and makes the cost of remote calls explicit, raising developers’ awareness of communication overhead.

29. DEBS
    

    TCEP: Adapting to Dynamic User Environments by Enabling Transitions between Operator Placement Mechanisms

    Manisha Luthra, Boris Koldehofe, Pascal Weisenburger, Guido Salvaneschi, Raheel Arif

    In Proceedings of the 12th ACM International Conference on Distributed and Event-Based Systems, DEBS, 2018

    Abstract PDF

    Operator placement has a profound impact on the performance of a distributed complex event processing system (DCEP). Since the behavior of a placement mechanism strongly depends on its environment; a single placement mechanism is often not enough to fulfill stringent performance requirements under environmental changes. In this paper, we show how DCEP can benefit from the adaptive use of multiple placement mechanisms. We propose TCEP, a DCEP system to integrate multiple placement mechanisms. By enabling transitions, TCEP can seamlessly exchange distinct operator mechanisms at runtime. We make two main contributions that are highly important for a cost-efficient transition: i) a transition strategy for efficiently scheduling state migrations and ii) a lightweight learning algorithm to adaptively select an appropriate placement mechanism as a consequence of a transition. Our evaluations for important decentralized placement mechanisms in the context of an IoT scenario show that transitions can better fulfill QoS demands in a dynamic environment. Thereby efficient scheduling of state migrations can help to faster complete transitions by up to 94%.

30. SEAMS
    

    Quality-Aware Runtime Adaptation in Complex Event Processing

    Pascal Weisenburger, Manisha Luthra, Boris Koldehofe, Guido Salvaneschi

    In Proceedings of the 12th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS, 2017

    Abstract PDF

    Complex event processing (CEP) is a fundamental paradigm for a software system to self-adapt to environmental changes. CEP provides efficient means to detect (complex) events corresponding to environmental changes by performing a real-time analysis on many, possibly heterogeneous, data sources. The way current CEP systems detect events is determined at design time without accounting for dynamic changes of the environment monitored by the CEP system. This can lead to situations where the performance, quality and reliability of event detection significantly drop (e.g., due to mobility) since initial assumptions of the environment are violated or stated too general. In this paper, we propose AdaptiveCEP, a CEP system that is able to self-adapt to detected changes in environmental conditions. We propose a CEP query language that allows specifying changes in the behavior of the CEP system and its mechanisms in detecting events dependent on environmental conditions. This way, AdaptiveCEP can select the best-suited configurations for given quality demands. In our evaluation, we show by means of a reference concept how the flexibility exposed by the query language helps to achieve significant performance gains.

31. SPLASH DS
    ScalaLoci
    

    Multitier Reactive Abstractions

    Pascal Weisenburger

    In Companion Proceedings of the 2016 ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity, SPLASH Companion, 2016

    Abstract PDF

    Distributed applications are traditionally developed using separate modules for each component in the distributed system, which can even be written in different programming languages. Those modules react on events such as user input, which are produced by other modules, and may in turn produce new events to be handled by different modules. Thus, most distributed applications are reactive in nature. Distributed event-based data flow makes it is hard to reason about the system and therefore makes the development of distributed systems challenging.

    In this paper, we present language abstractions for distributed reactive programming easing the development of such applications and supporting various distributed architectures.