No Arabic abstract
Context: The algorithms for generating a safe fluent API are actively studied these years. A safe fluent API is the fluent API that reports incorrect chaining of the API methods as a type error to the API users. Although such a safe property improves the productivity of its users, the construction of a safe fluent API is too complicated for the developers. The generation algorithms are studied to reduce the development cost of a safe fluent API. The study on the generation would benefit a number of programmers since a fluent API is a popular design in the real world. Inquiry: The generation of a generic fluent API has been left untackled. A generic fluent API refers to the fluent API that provides generic methods (methods that contain type parameters in their definitions). The Stream API in Java is an example of such a generic API. The recent research on the safe fluent API generation rather focuses on the grammar class that the algorithm can deal with for syntax checking. The key idea of the previous study is to use nested generics to represent a stack structure for the parser built on top of the type system. In that idea, the role of a type parameter was limited to internally representing a stack element of that parser on the type system. The library developers could not use type parameters to include a generic method in their API so that the semantic constraints for their API would be statically checked, for example, the type constraint on the items passed through a stream. Approach: We propose an algorithm to generate a generic fluent API. Our translation algorithm is modeled as the construction of deterministic finite automaton (DFA) with type parameter information. Each state of the DFA holds information about which type parameters are already bound in that state. This information is used to identify whether a method invocation in a chain newly binds a type to a type parameter, or refers to a previously bound type. The identification is required since a type parameter in a chain is bound at a particular method invocation, and that bound type is referred to in the following method invocations. Our algorithm constructs the DFA by analyzing the binding time of type parameters and their propagation among the states in a DFA that is naively constructed from the given grammar. Knowledge and Importance: Our algorithm helps library developers to develop a generic fluent API. The ability to generate a generic fluent API is essential to bring the safe fluent API generation to the real world since the use of type parameters is a common technique in the library API design. By our algorithm, the generation of a safe fluent API will be ready for practical use. Grounding: We implemented a generator named Protocool to demonstrate our algorithm. We also generated several libraries using Protocool to show the ability and the limitations of our algorithm.
We propose SessionC#, a lightweight session typed library for safe concurrent/distributed programming. The key features are (1) the improved fluent interface which enables writing communication in chained method calls, by exploiting C#s out variables, and (2) amalgamation of session delegation with async/await, which materialises session cancellation in a limited form, which we call session intervention. We show the effectiveness of our proposal via a Bitcoin miner application.
Testing networked systems is challenging. The client or server side cannot be tested by itself. We present a solution using tool Modbat that generates test cases for Javas network library java.nio, where we test both blocking and non-blocking network functions. Our test model can dynamically simulate actions in multiple worker and client threads, thanks to a carefully orchestrated design that covers non-determinism while ensuring progress.
We introduce a fully automated static analysis that takes a sequential Java bytecode program P as input and attempts to prove that there exists an infinite execution of P. The technique consists in compiling P into a constraint logic program P_CLP and in proving non-termination of P_CLP; when P consists of instructions that are exactly compiled into constraints, the non-termination of P_CLP entails that of P. Our approach can handle method calls; to the best of our knowledge, it is the first static approach for Java bytecode able to prove the existence of infinite recursions. We have implemented our technique inside the Julia analyser. We have compared the results of Julia on a set of 113 programs with those provided by AProVE and Invel, the only freely usable non-termination analysers comparable to ours that we are aware of. Only Julia could detect non-termination due to infinite recursion.
The current demands for seamless connections with the surrounding environment make software more reactive. For example, such demands are evident in systems consisting of the Internet of Things. Such systems include a set of reactive values that are periodically updated in response to external or internal events to form a dataflow in the sense that such updates are propagated to other reactive values. Two effective approaches for realizing such reactive values have been proposed: the event mechanisms in event-based programming and the signals in functional-reactive programming. These two approaches are now becoming mixed in several languages such as Flapjax and REScala, which makes these languages notably expressive for modularizing the implementation of reactive software. For example, REScala provides a rich API that consists of functions converting events to signals and vice versa. In this paper, we explore another, simpler approach in the design space of reactive programming languages: the event mechanism is harmonized with signals, resulting in a simplified programming interface that is mostly based on signals. Based on this approach, we realize SignalJ, a simple extension of Java with events and signals. Our notable findings are (1) an event can be represented as an update of a signal and (2) such an effectful signal can be represented using annotations instead of introducing types and constructors for signals to further simplify the language. Another contribution of this paper is the formal model of SignalJ. As both mechanisms of events and signals may interfere with each other, this mixing sometimes results in surprising behavior. For example, the functional behavior of signals is affected by the imperative features of events. Thus, understanding the formal model of this mixing is actually important. The core calculus, Featherweight SignalJ (FSJ), was developed as an extension of Featherweight Java, and proofs are provided to ensure the soundness of FSJ.
We present an efficient and expressive tool for the instrumentation of Java programs at the bytecode-level. BISM (Bytecode-Level Instrumentation for Software Monitoring) is a light-weight Java bytecode instrumentation tool that features an expressive high-level control-flow-aware instrumentation language. The language is inspired by the aspect-oriented programming paradigm in modularizing instrumentation into separate transformers, that encapsulate joinpoint selection and advice inlining. BISM allows capturing joinpoints ranging from bytecode instructions to methods execution and provides comprehensive static and dynamic context information. It runs in two instrumentation modes: build-time and load-time. BISM also provides a mechanism to compose transformers and automatically detect their collision in the base program. Transformers in a composition can control the visibility of their advice and other instructions from the base program. We show several example applications for BISM and demonstrate its effectiveness using three experiments: a security scenario, a financial transaction system, and a general runtime verification case. The results show that BISM instrumentation incurs low runtime and memory overheads.