From Concurrent State Machines to Reliable Multi-threaded Java Code
Dan Zhang
promotor: prof. dr. M.G.J. van den Brand (TU/e)
copromotors: dr. R. Kuiper (TU/e) and dr. D. Bosnacki (TU/e)
Eindhoven University of Technology
Date: 12 April 2018
Thesis: PDF
Summary
Model transformation is a powerful concept in model-driven software engineering. Starting with an initial model written in a domain-specific modeling language (DSML), other artifacts such as additional models, source code and test scripts can be produced via a chain of transformations. The initial model is typically written at a conveniently high level of abstraction, allowing the user to reason about complex system behavior in an intuitive way. The model transformations are supposed to preserve the correctness of the initial model, thereby realizing a framework where the generated artifacts are correct by construction. A question that naturally arises for model-to-code transformations is how to guarantee that the functional properties of the input models are preserved in the generated code. We distinguish generic and model specific code and concentrate on the former. We consider this question for a framework that implements the transformation from the concurrent DSML slco to multi-threaded Java code. In this context, we identify and address several challenges involving the robustness and correctness of generated code.
Our main contributions are as follows:
First, we start our research by studying the challenges and choices of implementing and verifying model-to-code transformations. We explore possibilities to mimic each slco concept with a counterpart programmed in Java. We also work on the implementation details which are not defined at the slco model level but have to be considered at the Java level (e.g., synchronization constructs and exception handling mechanisms). Furthermore, to obtain good implementations, we take quality aspects (e.g., modularity, efficiency, robustness) into account when implementing slco models. This consideration of quality aspects imposes additional challenges, e.g., functional and quality issues are often intertwined. Finally, we discuss challenges regarding the verification of the correctness of produced Java code and the transformation itself in terms of a formal logic and proof support.
Second, we develop an automated model-to-code transformation from slco models to multi-threaded Java programs, which is implemented in the Epsilon Generation Language (EGL) using Eclipse. The transformation rules are defined by means of templates. The generator applies transformation rules to all the meta-model objects, which results in generation of the corresponding Java code. This Java code is constructed by combining specific code implementing the behavior of the input model with generic code implementing model independent slco concepts. By making a distinction between generic and specific code, proving the correctness of model-to-code transformations can be done more efficiently.
Third, we provide a protection mechanism to access shared variables to preserve atomicity of slco statements in the Java implementation. This generic mechanism is used in our framework, but the solution is reusable to safely implement atomic operations in concurrent systems. We give its generic specification based on separation logic and verify it using VeriFast. We also show the feasibility to verify the atomicity of statements, focusing on the slco assignment statement. Moreover, we prove with VeriFast that our mechanism does not introduce lock-deadlocks. As an added value, we prove that in our generated programs there is no need for reentrant locks, which allows us to simplify the formal specification of the Java locks in our mechanism.
Fourth, we specify and perform automated verification of a Java implementation of the slco channel data type. To this end, we introduce a new schema that supports fine grained concurrency and procedure-modularity. We demonstrate this approach by specifying and verifying the channel construct using the separation logic based tool VeriFast. Our results show that such tool-assisted formal verification is a viable technique, supporting object orientation, concurrency via threads, and parameterized verification.
Fifth, we ensure the robustness of generated code by applying the exception handling mechanism called failbox to the code generation. To this end, we implement the mechanism failbox in Java and also improve it by eliminating the assumption required in the original failbox implementation. This assumption is eliminated in an incremental manner through several increasingly more robust implementations. For each implementation we analyze the vulnerabilities and argue the remedies in the next implementation.
Last, we present a testing approach to investigate whether the vulnerabilities of each implementation of failbox are realistic and the remedies proposed in the next implementation are effective. This testing approach enables us to generate asynchronous exceptions in a controlled manner for concurrent programs. The tests are repeatable in that they give the same results for runs that may differ in scheduling, even on different platforms.
To summarize, we identify several challenges on the correctness and robustness of Java code generated from concurrent state machines. To address these challenges, we introduce an approach where code is verified in a modular fashion using VeriFast and robustness is provided by an improved failbox mechanism. Techniques and approaches presented in this thesis enable the automated generation of reliable multi-threaded Java programs from slco models specifying concurrent systems at a high level of abstraction.