WebAssembly has established itself as a portable compilation target across a wide variety of environments, from browsers and cloud platforms to hardware-constrained devices such as microcontrollers.Its formal specification enables developers to reliably target a broad range of runtimes while compiler toolchains and runtime developers rely on the same formal model.Yet debugging support for WebAssembly remains at an early stage.Source maps often lack sufficient context for debugging, whereas DWARF offers rich type, scope, and location data that developers need for effective debugging.However, adding DWARF support requires non-trivial, timeconsuming runtime-specific efforts that must be repeated independently for each runtime.As a result, the set of debugging features available across runtimes is highly fragmented, while bugs that manifest exclusively in environments without debugging support cannot be analyzed at all.In this paper, we present DWasm, a runtime-independent debugger for WebAssembly.DWasm is realized as a binary transformation pass that instruments the target application with debugging support, without being implemented as part of a concrete runtime engine.By decoupling the debugger from the runtime, DWasm brings portable, DWARFbased debugging across WebAssembly environments.This approach further reduces tool development costs and enables debugging features to be customized for the applicationruntime combination at hand.For our benchmark programs, DWasm exhibits 2x memory overhead, which is low when compared with state-of-the-art debuggers for WebAssembly.In contrast, we observe a performance overhead consistently over 300x, where the shadow-execution instrumentation dominates the added overhead.

The CAP theorem demonstrates a trade-off between consistency and availability (and, by extension, latency) in systems where network partitions are unavoidable, such as in cloud computing and local-first software. While adopting weak consistency can preserve availability, it may result in inconsistencies that compromise application correctness. Replicated data types provide a principled, coordination-free approach to guarantee convergence but do not consider application invariants. Existing methods for maintaining invariants in replicated systems either rely on coordination - undermining the benefits of weak consistency - or suffer from limited applicability. This paper introduces the No-Op framework, a generic approach for enforcing consistency without coordination while guaranteeing both convergence and invariant preservation. The core idea of the No-Op approach is to resolve conflicts among concurrent operations by prioritising one operation over the other according to programmer-defined conflict resolution policies. This prioritisation transforms the less-preferred operation into a no-side-effect operation, ensuring conflict-free execution. We formalise the model underlying the No-Op framework and introduce a replication protocol built upon it, accompanied by a formal proof of correctness for both the framework and the protocol. Furthermore, we demonstrate the framework’s applicability by showcasing the design of widely used replicated data types and the preservation of a wide range of application invariants.

Dynamic program analyses help in understanding a program’s runtime behavior and detect issues related to security, program comprehension, or profiling. Instrumentation platforms aid analysis developers by offering a high-level API to write the analysis, and inserting the analysis into the target program. However, current instrumentation platforms for WebAssembly (Wasm) restrict analysis portability because they require concrete runtime environments. Moreover, their analysis API only allows the development of analyses that observe the target program but cannot modify it. As a result, many popular dynamic analyses present for other languages, such as runtime hardening, virtual patching or runtime optimization, cannot currently be implemented for Wasm atop a dynamic analysis platform. Instead, they need to be built manually, which requires knowledge of low-level details of the Wasm’s semantics and instruction set, and how to safely manipulate it. This paper introduces Wastrumentation, the first dynamic analysis platform for WebAssembly that supports intercession. Our solution, based on source code instrumentation, weaves the analysis code directly into the target program code. Inlining the analysis into the target’s source code avoids dependencies on the runtime environment, making analyses portable across Wasm VMs. Moreover, it enables the implementation of analyses in any Wasm-compatible language. We evaluate our solution in two ways. First, we compare it against a state-of-the-art source code instrumentation platform using the WasmR3 benchmarks. The results show improved memory consumption and competitive performance overhead. Second, we develop an extensive portfolio of dynamic analyses, including novel analyses previously unattainable with source code instrumentation platforms, such as memoization, safe heap access, and the removal of NaN non-determinism.

ABSTRACT Introduction Distributed system programmers rely on Replicated Data Types (RDTs), which resemble sequential data types but incorporate conflict resolution strategies to guarantee convergence when conflicts occur. The semantics of RDTs depend on the underlying conflict resolution strategy, but these cannot be customized. Moreover, ensuring state convergence alone is not enough because the resulting state may break application‐specific invariants. Although some approaches support application‐level invariants atop existing RDTs, they do not help build the RDT in the first place. As a result, custom RDTs are implemented using ad hoc approaches, which are known to be error‐prone and result in brittle systems. We previously proposed Explicitly Consistent Replicated Objects (ECROs) to address these issues, enabling programmers to build custom RDTs by augmenting sequential data types with a distributed specification. However, the specification requires a complete first‐order logic formalization of the data type and its operations, which is hard to develop. Furthermore, subtle errors in the specification may result in runtime anomalies such as state divergence and broken invariants. Methods To tackle these problems, we combine the ECRO programming model with automated program verification. The result is EFx, a minimalist object‐oriented programming language whose core consists of a contract system that simplifies the development of RDTs. EFx does not require tedious first‐order logic specifications because it analyses the data type's implementation, thereby preventing runtime anomalies due to errors in the specification. Results We reconstruct the original portfolio of ECROs in EFx to validate our approach. We consistently achieve a 2x to 4x reduction of the code size. Additionally, we implement several applications, such as the RUBiS auction system, the SmallBank benchmark, a distributed voting game, and an airline reservation system. Conclusion Our evaluation shows that EFx simplifies the development of RDTs.

Modern distributed applications increasingly replicate data to guarantee high availability and optimal user experience. Conflict-free Replicated Data Types (CRDTs) are a family of data types specially designed for highly available systems that guarantee some form of eventual consistency. Designing CRDTs is very difficult because it requires devising designs that guarantee convergence in the presence of conflicting operations. Even though design patterns and structured frameworks have emerged to aid developers with this problem, they mostly focus on statically structured data; nesting and dynamically changing the structure of a CRDT remains to be an open issue. This paper explores support for nested CRDTs in a structured and systematic way. To this end, we define an approach for building nested CRDTs based on the work of pure operation-based CRDTs, resulting in nested pure operation-based CRDTs. We add constructs to control the nesting of CRDTs into a pure operation-based CRDT framework and show how several well-known CRDT designs can be defined in our framework. We provide an implementation of nested pure operation-based CRDTs as an extension to the Flec, an existing TypeScript-based framework for pure operation-based CRDTs. We validate our approach, 1) by implementing a portfolio of nested data structures, 2) by implementing and verifying our approach in the VeriFx language, and 3) by implementing a real-world application scenario and comparing its network usage against an implementation in the closest related work, Automerge. We show that the framework is general enough to nest well-known CRDT designs like maps and lists, and its performance in terms of network traffic is comparable to the state of the art.

Distributed systems adopt weak consistency to ensure high availability and low latency, but state convergence is hard to guarantee due to conflicts. Experts carefully design replicated data types (RDTs) that resemble sequential data types and embed conflict resolution mechanisms that ensure convergence. Designing RDTs is challenging as their correctness depends on subtleties such as the ordering of concurrent operations. Currently, researchers manually verify RDTs, either by paper proofs or using proof assistants. Unfortunately, paper proofs are subject to reasoning flaws and mechanized proofs verify a formalization instead of a real-world implementation. Furthermore, writing mechanized proofs is reserved for verification experts and is extremely time-consuming. To simplify the design, implementation, and verification of RDTs, we propose VeriFx, a specialized programming language for RDTs with automated proof capabilities. VeriFx lets programmers implement RDTs atop functional collections and express correctness properties that are verified automatically. Verified RDTs can be transpiled to mainstream languages (currently Scala and JavaScript). VeriFx provides libraries for implementing and verifying Conflict-free Replicated Data Types (CRDTs) and Operational Transformation (OT) functions. These libraries implement the general execution model of those approaches and define their correctness properties. We use the libraries to implement and verify an extensive portfolio of 51 CRDTs, 16 of which are used in industrial databases, and reproduce a study on the correctness of OT functions.

Debugging embedded systems is difficult due to the restricted resources available, and the hard to reproduce bugs. Moreover, few debugging facilities are available for constrained devices. To address this, we build upon a recent technique for big data applications, called out-of-place debugging.

The NODE.JS runtime, in combination with Node Package Manager (NPM), is a popular ecosystem for building server-side web applications. Both JavaScript’s flexible and dynamic character and the vast amount of NPM libraries available can speed up the development of web applications. However, JavaScript and NODE.JS lack security mechanisms and abstractions. Despite the numerous language-based approaches proposed to protect JavaScript applications, no work supports application-level and business-level security properties. This means that in order to achieve both application-level and business-level security, developers are forced to rely on multiple different, unintegrated and incompatible tools and mechanisms.In this paper, we present BRIGADIER1, an interactive security testing framework for NODE.JS applications that enables the specification of both application-level and business-level security policies. Brigadier provides developers with a Datalog-based policy specification language that features close interoperability with running JavaScript programs under test. Input JavaScript programs are instrumented to emit relevant application events sent to a Datalog engine resulting from the compilation of the policies. We exhibit Brigadier’s expressiveness by implementing three case studies from the literature. We also assess Brigadier’s performance overhead on server-side applications. In our benchmarks, we observed a slowdown factor ranging from∼1.2x to ∼3x, which is acceptable for a testing scenario.

Debugging IoT applications is challenging due to the hardware constraints of IoT devices, making advanced techniques like record-replay debugging impractical. As a result, programmers often rely on manual resets or inefficient and time-consuming debugging techniques such as printf. Although simulators can help in that regard, their applicability is limited because they fall short of accurately simulating and reproducing the runtime conditions where bugs appear. In this work, we explore a novel debugging approach called event-based out-of-place debugging in which developers can capture a remotely running program and debug it locally on a (more powerful) machine. Our approach thus provides rich debugging features (e.g., step-back) that normally would not run on the hardware restricted devices. Two different strategies are offered to deal with resources which cannot be easily transferred (e.g., sensors): pull-based (akin to remote debugging), or push-based (where data updates are pushed to developer’s machine during the debug session). We present EDWARD, an event-based out-of-place debugger prototype, implemented by extending the WARDuino WebAssembly microcontroller Virtual Machine, that has been integrated into Visual Studio Code. To validate our approach, we show how our debugger helps uncover IoT bugs representative of real-world applications through several use-case applications. Initial benchmarks show that event-based out-of-place debugging can drastically reduce debugging latency.

Apache Spark is a framework widely used for writing Big Data analytics applications that offers a scalable and fault-tolerant model based on rescheduling failing tasks on other nodes. While this is well-suited for hardware and infrastructure errors, it is not for application errors as they will reappear in the rescheduled tasks. As a result, applications are killed, losing all the progress and forcing developers to restart them from scratch. Despite the popularity of such a failure-recovery model, understanding and debugging Spark-like applications remain challenging. When an error occurs, developers need to analyze huge log files or undergo time-consuming replays to find the bug. To address these concerns, we present an online debugging approach tailored to Big Data analytics applications. Our approach includes local debugging of remote parallel exceptions through dynamic local checkpoints, extended with domain-specific debugging operations and live code updating functionality. To deal with data-cleaning errors, we extend our model to easily allow developers to automatically ignore exceptions that happen at runtime. We validate our solution through performance benchmarks that show how our debugging approach is comparable or better than state-of-the-art debugging solutions for Big Data. Furthermore, we conduct a user study to compare our approach with another state-of-the-art debugging approach, and results show a lower time to find the solution to a bug using our approach, as well as a generally good perception of the features of the debugger.

To ease the development of geo-distributed applications, replicated data types (RDTs) offer a familiar programming interface while ensuring state convergence, low latency, and high availability. However, RDTs are still designed exclusively by experts using ad-hoc solutions that are error-prone and result in brittle systems. Recent works statically detect conflicting operations on existing data types and coordinate those at runtime to guarantee convergence and preserve application invariants. However, these approaches are too conservative, imposing coordination on a large number of operations. In this work, we propose a principled approach to design and implement efficient RDTs taking into account application invariants. Developers extend sequential data types with a distributed specification, which together form an RDT. We statically analyze the specification to detect conflicts and unravel their cause. This information is then used at runtime to serialize concurrent operations safely and efficiently. Our approach derives a correct RDT from any sequential data type without changes to the data type's implementation and with minimal coordination. We implement our approach in Scala and develop an extensive portfolio of RDTs. The evaluation shows that our approach provides performance similar to conflict-free replicated data types for commutative operations, and considerably improves the performance of non-commutative operations, compared to existing solutions.

Debugging applications that execute within a framework is not always easy: the call-stack offered to developers is often a mix-up of stack frames that belong to different frameworks, introducing an unnecessary noise that prevents developers from focusing on the debugging task. Moreover, relevant application code is not always available in the call-stack because it may have already returned, or is available in another thread. In such cases, manually gathering all relevant information from these different sources is not only cumbersome but also costly.

Modern distributed applications increasingly replicate data to guarantee both high availability of systems and optimal user experience. Conflict-Free Replicated Data Types (CRDTs) are a family of data types specially designed for highly available systems that guarantee some form of eventual consistency. To ensure state convergence between replicas, CRDT implementations need to keep track of additional meta-data. This is not a scalable strategy, as a growing amount of meta-data has to be kept.

Many frameworks exist for programmers to develop and deploy Big Data applications such as Hadoop Map/Reduce and Apache Spark. However, very little debugging support is currently provided in those frameworks. When an error occurs, developers are lost in trying to understand what has happened from the information provided in log files. Recently, new solutions allow developers to record & replay the application execution, but replaying is not always affordable when hours of computation need to be re-executed. In this paper, we present an online approach that allows developers to debug Big Data applications in isolation by moving the debugging session to an external process when a halting point is reached. We introduce IDRA MR , our prototype implementation in Pharo. IDRA MR centralizes the debugging of parallel applications by introducing novel debugging concepts, such as composite debugging events, and the ability to dynamically update both the code of the debugged application and the same configuration of the running framework. We validate our approach by debugging both application and configuration failures for two driving scenarios. The scenarios are implemented and executed using Port, our Map/Reduce framework for Pharo, also introduced in this paper.

Summary OpenSmalltalk‐VM is a virtual machine (VM) for languages in the Smalltalk family (eg, Squeak and Pharo), which is itself written in a subset of Smalltalk that can easily be translated to C. VM development is done in Smalltalk, an activity we call “simulation.” The production VM is then derived by translating the core VM code to C. As a result, two execution models coexist: simulation, where the Smalltalk code is executed on top of a Smalltalk VM, and production, where the same code is compiled to an executable through a C compiler. The whole VM execution can be simulated: the heap is represented as a huge byte array, the VM code is executed as Smalltalk, and the native code generated by the just‐in‐time (JIT) compiler is executed by a processor simulator. All the Smalltalk development tools, such as the debugger, are then available while simulating. In addition, in simulation, it is also possible to use debugging features such as single stepping in the machine code generated by the JIT compiler. The Smalltalk development tools combined with the simulation debugging features provide developers with a productive environment in which to extend and debug the VM. In this article, we detail the VM simulation infrastructure and report our experiences developing and debugging VM features within it such as the garbage collector and the JIT compiler.

To keep applications highly responsive, garbage collectors (GCs) try to minimize interruptions of the application threads. While pauses due to non moving GCs can be drastically reduced through concurrent or incremental strategies, compaction pauses remain a big problem.

Many of today’s software systems are parallel or concurrent. With the rise of Node.js and more generally event-loop architectures, many systems need to handle concurrency. However, its non-deterministic behavior makes it hard to reproduce bugs. Today’s interactive debuggers unfortunately do not support developers in debugging non-deterministic issues. They only allow us to explore a single execution path. Therefore, some bugs may never be reproduced in the debugging session, because the right conditions are not triggered. As a solution, we propose multiverse debugging, a new approach for debugging non-deterministic programs that allows developers to observe all possible execution paths of a parallel program and debug it interactively. We introduce the concepts of multiverse breakpoints and stepping, which can halt a program in different execution paths, i.e. universes. We apply multiverse debugging to AmbientTalk, an actor-based language, resulting in Voyager, a multiverse debugger implemented on top of the AmbientTalk operational semantics. We provide a proof of non-interference, i.e., we prove that observing the behavior of a program by the debugger does not affect the behavior of that program and vice versa. Multiverse debugging establishes the foundation for debugging non-deterministic programs interactively, which we believe can aid the development of parallel and concurrent systems.

The actor model is popular for many types of server applications. Efficient snapshotting of applications is crucial in the deployment of pre-initialized applications or moving running applications to different machines, e.g for debugging purposes. A key issue is that snapshotting blocks all other operations. In modern latency-sensitive applications, stopping the application to persist its state needs to be avoided, because users may not tolerate the increased request latency. In order to minimize the impact of snapshotting on request latency, our approach persists the application’s state asynchronously by capturing partial heaps, completing snapshots step by step. Additionally, our solution is transparent and supports arbitrary object graphs. We prototyped our snapshotting approach on top of the Truffle/Graal platform and evaluated it with the Savina benchmarks and the Acme Air microservice application. When performing a snapshot every thousand Acme Air requests, the number of slow requests ( 0.007% of all requests) with latency above 100ms increases by 5.43%. Our Savina microbenchmark results detail how different utilization patterns impact snapshotting cost. To the best of our knowledge, this is the first system that enables asynchronous snapshotting of actor applications, i.e. without stop-the-world synchronization, and thereby minimizes the impact on latency. We thus believe it enables new deployment and debugging options for actor systems.

Developing JavaScript and web applications with confidentiality and integrity guarantees is challenging. Information flow control enables the enforcement of such guarantees. However, the integration of this technique into software tools used by developers in their workflow is missing. In this paper we present GUARDIAML, a machine learning-assisted dynamic information flow control tool for JavaScript web applications. GUARDIAML enables developers to detect unwanted information flow from sensitive sources to public sinks. It can handle the DOM and interaction with internal and external libraries and services. Because the specification of sources and sinks can be tedious, GUARDIAML assists in this process by suggesting the tagging of sources and sinks via a machine learning component.

Dynamic analyses are commonly implemented by instrumenting the program under analysis. Examples of such analyses for JavaScript range from checkers of user- defined invariants to concolic testers. For a full-stack JavaScript program, these analyses would benefit from reasoning about the state of the client-side and server-side processes it is comprised of. Lifting a dynamic analysis so that it supports full-stack programs can be challenging. It involves distributed communication to maintain the analysis state across all processes, which has to be deadlock-free. In this paper, we advocate maintaining distributed analysis state in a centralized analysis process instead — which is communicated with from the processes under analysis. The approach is supported by a dynamic analysis platform that provides abstractions for this communication. We evaluate the approach through a case study. We use the platform to build a distributed origin analysis, capable of tracking the expressions from which values originate from across process boundaries, and deploy it on collaborative drawing application. The results show that our approach greatly simplifies the lifting process at the cost of a computational overhead. We deem this overhead acceptable for analyses intended for use at development time.

Today's complex software systems combine high-level concurrency models. Each model is used to solve a specific set of problems. Unfortunately, debuggers support only the low-level notions of threads and shared memory, forcing developers to reason about these notions instead of the high-level concurrency models they chose.

We present Linvail, a novel instrumentation platform for developing dynamic analyses of JavaScript programs. Linvail is particularly well-suited to implementing shadow executions which involve tagging runtime values with analysis-specific data. In contrast to existing instrumentation platforms, Linvail is capable of tracking both tagged objects and tagged primitive values during their entire life-time in a behavior-preserving manner. To demonstrate the expressiveness of our platform, we present the implementation of several state-of-the-art analyses. Our experiments demonstrate that Linvail's accuracy comes at the price of a performance overhead, but we believe that real-world applications will remain usable under analysis.

In this paper we argue the need for orchestration support for participatory campaigns to achieve campaign quality, and automatisation of said support to achieve scalability, both issues contributing to stakeholder usability. This goes further than providing support for defining campaigns, an issue tackled in prior work. We provide a formal definition for a campaign by extracting commonalities from the state of the art and expertise in organising noise mapping campaigns. Next, we formalise how to ensure campaigns end successfully, and translate this formal notion into an operational recipe for dynamic orchestration. We then present a framework for automatising campaign definition, monitoring and orchestration which relies on workflow technology. The framework is validated by re-enacting several campaigns previously run through manual orchestration and quantifying the increased efficiency.

The evolution of smartphones has given rise to urban-area applications: applications that communicate in a city by means of the public (moving) infrastructure (e.g., buses and trams). In this setting, applications need to communicate with and discover each other using intermediaries that move around the city and transfer data between them. This requires programmers to scatter code that deals with routing messages to the correct place and deal with network failures all over their programs. Our approach allows the programmer to specify urban-area applications in a high-level manner without the burden of directly encoding communication using intermediaries. We present this as a translation from a high-level object-oriented programming paradigm to a low-level communication mechanism. This translation allows the programmer to restrict routing of messages to, for example, a certain number of hops, geographic areas, or even types of carrier devices. In addition, we show how high-level group messaging can be efficiently represented in the low-level communication. Finally, we document our experiences in setting up a small-scale real-world urban-area application.

SUMMARY The iPhone SDK provides a powerful platform for the development of applications that make use of iPhone capabilities, such as sensors, GPS, Wi‐Fi, or Bluetooth connectivity. We observe that so far the development of iPhone applications has mostly been restricted to using Objective‐C. However, developing applications in plain Objective‐C on the iPhone OS suffers from limitations, such as the need for explicit memory management and lack of syntactic extension mechanism. Moreover, when developing distributed applications in Objective‐C, programmers have to manually deal with distribution concerns, such as service discovery, remote communication, and failure handling. In this paper, we discuss our experience in porting the Scheme programming language to the iPhone OS and how it can be used together with Objective‐C to develop iPhone applications. To support the interaction between Scheme programs and the underlying iPhone APIs, we have implemented a language symbiosis layer that enables programmers to access the iPhone SDK libraries from Scheme. In addition, we have designed high‐level distribution constructs to ease the development of distributed iPhone applications in an event‐driven style. We validate and discuss these constructs with a series of examples, including an iPod controller, a maps application, and a distributed multiplayer Scrabble‐like game. We discuss the lessons learned from this experience for other programming language ports to mobile platforms. Copyright © 2011 John Wiley & Sons, Ltd.

Abstract This paper introduces a novel mechanism to perform intercession (a form of reflection) in an object‐oriented programming language with the goal of making the language extensible from within itself. The proposed mechanism builds upon a mirror‐based architecture, leading to a reusable reflective application programming interface that cleanly separates interface from implementation details. However, support for intercession has been limited in contemporary mirror‐based architectures. This is due to the fact that mirror‐based architectures only support reflection explicitly triggered by metaprograms, while intercession requires reflection implicitly triggered by the language interpreter. This work reconciles mirrors with intercession in the context of an actor‐based, object‐oriented programming language named AmbientTalk. We describe this language's full reflective architecture, highlighting its novel mirror‐based approach to reflect upon both objects and concurrently executing actors. Subsequently, we apply AmbientTalk's mirror‐based reflection to implement two language features, which crucially depend on intercession, to wit future‐type message passing and leased object references. Copyright © 2008 John Wiley & Sons, Ltd.