We present work in progress on, veri ed, transformation of a modeling language based on communicating concurrent state machines, slco, to Java. Some concurrency related challenges, related to atomicity and non-standard fairness issues, are pointed out. We discuss solutions based on Java synchronization concepts. ? This work was sponsored by the China Scholarship Council (CSC) ?? This work was done with nancial support from the Netherlands Organisation for Scienti c Research (NWO).
Model-Driven Software Engineering (MDSE) is gaining popularity as a methodology for developing software in an e cient way. In many cases the models can be veri ed which leads to higher quality software. In MDSE, an abstract model is made increasingly more detailed through model-to-model transformations, until the model can be transformed to source code. This allows detecting defects in the early stages of the development, which can signi cantly reduce production costs and improve end product quality.
One of the challenges in MDSE is maintaining correctness during the
development. The correctness of model-to-model transformations is one of the research
topics of our group [6{8]. In this paper the correctness of model-to-code
transformations is addressed. We investigate automated Java code generation from
models in the domain speci c language Simple Language of Communicating
Objects (slco) [
SLCO In slco, systems consisting of concurrent, communicating objects can be described using an intuitive graphical syntax. The objects are instances of classes, and connected by channels, over which they send and receive signals. They are connected to the channels via their ports. slco o ers three types of channels: synchronous, asynchronous lossless, and asynchronous lossy channels. Furthermore, each channel is suited to transfer signals of a prede ned type.
The behaviour of objects is speci ed using state machines, such as in Figure 1. As can be seen in the
gure, each transition has a source and target state, and a list of statements that are executed when the transition is red.
A transition is enabled if the rst of these statements is Fig. 1. Behaviour diagram of an slco model enabled. slco supports a variety of statement types. For communication between objects, there are statements for sending and receiving signals. The statement send T (s) to InOut , for instance, sends a signal named T with a single argument s via port InOut . Its counterpart receive T (s) from InOut receives a signal named T from port InOut and stores the value of the argument in variable s. Statements such as receive P ([[false]]) from In1 o er a form of conditional signal reception. Only those signals whose argument is equal to false will be accepted. There is also a more general form of conditional signal reception. For example, statement receive Q(m j m 0) from In2 only accepts those signals whose argument is at least equal to 0. Boolean expressions, such as m == 6 , denote statements that block until the expression holds. Time is incorporated in slco by means of delay statements. For example, the statement after 5 ms blocks until 5 ms have passed. Assignment statements, such as m := m + 1 , are used to assign values to variables. Variables either belong to an object or a state machine. The variables that belong to an object are accessible by all state machines that are part of the object.
Transformation from SLCO to Java The transformation from an slco
model to Java is performed in two stages. First the textual slco model is
automatically transformed into an intermediate model, which is then translated
to Java. Recently we created a platform for the second stage in the Epsilon
Generation Language (EGL) [
State Machines Since slco state machines represent concurrent processes, each state machine is mapped to a di erent thread in the Java implementation. We use switch statements to represent the behavior of the state machine (Listing 1.1). Each case corresponds to one state of the state machine and comprises a sequence of statements corresponding to the actions of a related outgoing state transition. If a state has more than one transition, nested switch statements are added in the generated code with a separate case for each transition.
Listing 1.1. Part of generated code for the state machine 1 currentState = "Com0"; 2 while(true){ 3 switch(currentState){ 4 case "Com0": 5 String transitions[] = {"Com02Com1","Com02Com2"}; 6 ... 7 int idx = new Random().nextInt(transitions.length); 8 String nextTransition = transitions[idx]; 9 ... 10 switch(nextTransition){ 11 case "Com02Com1": 12 ...//check whether the transition Com02Com1 is enabled or not 13 } 14 case "Com1": 15 ... 16 } 17 }
Shared Variables Since shared variables can be accessed and modi ed by multiple state machines in one object, we need to consider synchronization constructs. In our current implementation we use one writing lock and one reading lock to control the access for all shared variables in one object. Both the reading and writing locks operate in fair mode, using an approximate arrival-order policy. A boolean expression statement using a reading lock is shown in Listing 1.2.
Listing 1.2. Part of generated code for the Boolean expression statement 1 boolean isExecutedExpression = false; 2 while(!isExecutedExpression){ 3 r.lock(); 4 try{ 5 if((m.value==6)){ 6 isExecutedExpression = true; 7 } 8 } finally { r.unlock(); } 9 } 10 ...
Channels Because lossy channels in slco are an undesired aspect of physical connections, these are not transformed to Java; hence the framework just supports the synchronous and asynchronous lossless channel. slco's asynchronous channels have bu er capacity 1. The sender/receiver blocks when the channel is full/empty - this is provided by a BlockingQueue with a bu er capacity of 1 (from the package java.util.concurrent). In case of conditional reception from an slco channel, the element will only be consumed if the value satis es the condition. This requires that the head of the queue is inspected without taking the element, which is provided by BlockingQueue. slco's synchronous channels enable handshake-like synchronization between state machines. Our current implementation again uses the BlockingQueue, with additional ad hoc synchronization code.
In Listing 1.3 we give the generated Java code for sending a signal message of state machine Com via port InOut as shown in Fig. 1. Notice that we add the wait() method of Java to synchronize sending and receiving parties, if the channel between two state machines is synchronous.
Listing 1.3. Part of generated code of channels for sending signal message 1 synchronized(port_InOut.channel.queue){ 2 port_InOut.channel.queue.put(new SignalMessage("T",new Object[]{s})); 3 if(port_InOut.channel.isSynchronousChannel){ 4 port_InOut.channel.queue.wait(); 5 }... 6 } 3
The challenges in the transformation from slco to Java as well as in the veri cation of it mainly originate from the di erences between the modeling-oriented primitives in slco and their implementation-oriented counterparts in Java. Shared variables { atomicity In slco assignments where multiple shared variables are involved are atomic, therefore we use Java variables together with locks to guard the assignments. Instead of the built-in locks we use ReentrantReadWriteLock from the package java.util.concurrent.locks with concurrent read access, which improves performance. Furthermore, in slco conditions on a transition may involve several shared variables. The aforementioned package enables to create a condition object for each condition on a transition, that can be used to notify waiting processes, which gives better performance than checking with busy-waiting. Our current implementation uses ReentrantReadWriteLock, but with a simple busy wait to simulate the slco blocking. Using the condition objects whilst maintaining the slco semantics is the next step.
Channels { synchronization Other synchronization primitives from the package java.util.concurrent are under investigation to replace the current ad hoc synchronization code.
Choice between transitions { external/internal In case of several possibly blocking outgoing transitions of a state in slco, the state machine will only block if all outgoing transitions are blocked. (This applies to shared variable access as well as channel operations.) In a naive implementation, however, the disabledness of a transition can only be assessed by initiating its execution and then blocking, and waiting for the transition becoming enabled. Essentially, this means that an external choice is turned into an internal choice, which is undesired. Here we face a similar challenge as with conditions or assignments using several shared variables. This may be solved in a similar manner, namely with a condition object dedicated to the state and cooperating processes that notify the waiting process when one of the reasons for blocking might have changed.
We have solutions for speci c cases and are investigating a generic solution for all transitions that involve blocking and is orthogonal to other concurrency aspects like conditional reading from a channel, synchronization of channels, etc. Fairness { interleaving, resolving con ict The slco speci cation approach raises non-standard fairness issues. In early usage of slco, no fairness was assumed for slco speci cations. If properties depended upon fairness, this meant taking this into account for the implementation. The challenge is to advance the formal rigor of the slco-approach by formally expressing fairness and have the generated code together with the JVM ensure this fairness.
We use an interleaving semantics for slco with weak fairness: if at some time point a transition becomes continuously enabled, this transition will at some later time point be taken: in linear time temporal logic 2(2enabled(t) ! taken(t)). Because the granularity in Java is much ner than in slco, more progress is enforced by weak fairness in slco than in Java. Therefore we need stronger fairness in Java. We aim to achieve this through a combination of fairness in scheduling threads, obtainable by choosing the right JVM, and fair locks, obtainable from the package java.util.concurrent.locks.
Veri cation We aim to partially verify the transformation. Our rst approach
is that the generated code uses generic code that we provide as a library of
implementations for, e.g., channels. We annotate and verify this generic code.
To deal with pointers and concurrency in Java we will use Separation Logic [
In the context of automated Java code generation we identi ed several challenges involving shared memory communication and fairness. Our initial ndings imply that the veri cation of the generic Java code implementing shared memory communication for safety properties is feasible using separation logic. As one of the anonymous reviewers observed, it might be useful to identify Java patterns for correctly capturing concurrent model semantics. Besides code generation, this can be used as a basis for developing e cient simulation, formal veri cation and other analysis tools.