We present a tool for analysing resource sharing con icts in multithreaded Java programs. We consider two models of execution: purely parallel one and sequential execution on a single processor. A Java program is translated into a system of timed automata which is veri ed by the model checker Uppaal. We also present our work in progress on formalisation of Real-Time Java semantics and the semantics of timed automata.
Along with increasing usage of multithreaded programming, a strong need of
sound algorithms arises. The problem is even more important in programming
of embedded and real-time systems where liveness conditions are extremely
important. To certify that no thread would starve or would be deadlocked, lock-free
and wait-free algorithms have been developed. Lock-free algorithms do not use
critical sections or locking and allow to avoid thread waiting for getting access to
a mutual exclusion object. Nevertheless, only one thread is guaranteed to make
progress. Wait-free algorithms prevent starvation by guaranteeing a stronger
property: all threads are guaranteed to make progress, eventually. Such
algorithms for linked lists, described for example in [
What is worse, these algorithms seem to be incompatible with hard real-time requirements: the progress guarantees are not bounded in time. Thus, a lock-free insertion of an element into a linked list by a thread may need several (possibly in nitely many) retries because the thread can be disturbed by concurrent threads. Under these conditions, it is not possible to predict how much time is needed before the thread succeeds. ? Part of this research has been supported by the project Verisync (ANR-10-BLAN0310)
Critical sections are used in many applications in order to ensure concurrent
access to objects although if the scheduling order is wisely planned, locks are not
necessary since threads access objects at di erent moments of time. This is the
motivation for our work: we develop a tool for checking resource sharing con icts
in concurrent Java programs based on the statement execution time. This gives a
\time-triggered" [
We assume that a program is annotated with WCET information known from external sources. The checker translates a Java program into a timed automaton which is then model checked by a tool for timed automata (concretely, Uppaal).
In this paper, after an informal introduction (Section 2), we present a formal semantics of the components of the translation, namely Timed Automata (Section 3) and a multi-threaded, timed version of Java (Section 4). Then we describe the mechanism of the concrete translator written in OCaml (Section 5) and give some preliminary correctness arguments (Section 6) { the formal veri cation still remains to be done. The conclusions (Section 7) discuss some restrictions of our current approach and possibilities to lift them.
Status of the present document: We give a glimpse at several aspects of our formalisation, which is far from being coherent. Therefore, this paper is rather a basis for discussion than a nished publication. 2
To show the main idea, we present an example of a concurrent Java program. It is a primitive producer-consumer bu er with one producer and one consumer where both producer and consumer are invoked periodically. The program is annotated with information about statement execution time in //@ ... @// comments. One of the possible executions is shown in Figure 1.
0 1 8 20
After having translated this program to a system of timed automata we run the Uppaal model checker to determine possible resource sharing con icts. The checked formula is
A[]8(i : int[0; objN umber 1])8(j : int[0; autN umber 1])waitSet[i][j] < 1; (1) where waitSet is an array of boolean ags indicating whether a thread waits for a lock of a particular object. If all array members in all moments of time are false, no thread waits for a lock therefore no resource sharing con icts are possible.
Timed automata are a common tool for verifying concurrent systems; the
underlying theory is described in [
An automaton edge is composed of a starting node, a condition under which the edge may be taken (guard), an action, clocks to reset and a nal node. type-synonym ( 0n; 0a) edge = 0n cconstr 0a list id set 0n
An invariant is a condition on a node which must be satis ed when an automaton is in this node. type-synonym 0n inv = 0n ) cconstr
An automaton consists of a set of nodes, a starting node, a set of edges and an invariant function. type-synonym ( 0n; 0a) ta = 0n set 0n ( 0n; 0a) edge set 0n inv
We use the model checker Uppaal which proposes an extension of classical timed automata with variables. A full state comprises a node and a valuation function. There are two types of variables: integer (aval ) and boolean (bval ), and clock variables which have a special semantic status in timed automata. The available transitions can be de ned knowing given this state. record valuation= aval :: id )nat bval :: id )bool cval :: id )time type-synonym 0n state = 0n
valuation
A timed automaton can perform two types of transitions: timed delay and edge taking. If an automaton takes an edge, variables may be updated or clocks may be reset to 0. The Transition constructor takes a list of variable and clock updates as an argument. datatype 0a ta-action = Timestep time j Transition 0a list
Accordingly, the timed automata semantics has two rules: delay and transition. If an automaton is delayed, it stays in the same node, and values of all clocks are increased to the value d. The invariant of the current node must be satis ed.
If an automaton takes a transition, the node is changed, and clock values remain unchanged unless they are reset to 0. The invariants of both starting and nal nodes must be satis ed as well as the guard of the taken transition. If the action of the transition involves variable updates, the valuation function is updated as well. This is done by the function application eval-stmts varv a.
varv 0 = varv (jcval := add (cval varv ) d j) varv j= invs l varv 0 j= invs l l 2 nodes (nodes; init ; edges; invs) ` (l ; varv ) Timestep d ! (l ; varv 0) varv j= g
(l ; g; a; r ; l 0) 2 edges varv 0 = eval-stmts varv a(jcval := reset (cval varv ) r j) varv 0 j= invs l 0 l 2 nodes l 0 2 nodes (nodes; init ; edges; invs) ` (l ; varv ) Transition a! (l 0; varv 0)
A network of timed automata is a product automaton with exceptions in case
of handshaking actions [
(s1; g1; a; cs1; s1 0) 2 edges1 (s2; g2; a; cs2; s2 0) 2 edges2
a 2 getEdgeActions edges1 \ getEdgeActions edges2 ((s1; s2); g1 d^e g2; a; cs1 [ cs2; s1 0; s2 0) 2 edges-shaking edges1 edges2 (s1; g; a; cs; s1 0) 2 edges1 a 2= getEdgeActions edges2 a 2 getEdgeActions edges1 s2 2 getEdgeNodes edges2 ((s1; s2); g; a; cs; s1 0; s2) 2 edges-shaking edges1 edges2 (s2; g; a; cs; s2 0) 2 edges2 a 2= getEdgeActions edges1 a 2 getEdgeActions edges2 s1 2 getEdgeNodes edges1 ((s1; s2); g; a; cs; s1; s2 0) 2 edges-shaking edges1 edges2 4
The look of the Java semantics has been inspired by the Jinja project [
Following Jinja, we do not distinguish expressions and statements; their datatype is the following: datatype expr = Val val j Var vname j VarAssign vname expr j Cond expr expr expr j While expr expr j Annot annot expr j Sync expr expr j Sleep expr ... and others.
The system state is large and complex; it stores local information of all threads such as local variable values and expression to be evaluated, shared objects, time, actions to be carried out by the platform, locks and wait sets. Given this state and scheduler logic, the further execution order is deterministic. record full-state = threads :: id ) schedulable option | threads pool th-info :: thread-id ) thread-state option | expression to be evaluated and state sc-info :: schedule-info | locks and thread statuses pl-info :: platform-info | global time gl-info :: heap | heap state ws-info :: waitSet | wait sets running-th :: thread-id | currently running thread pending-act :: action | action to be carried out by platform
Evaluation semantics depends solely on local and heap variables therefore we use the reduced variant of full state for thread evaluation step. record eval-state = ev-st-heap :: heap ev-st-local :: locals
When a thread expression is reduced, the duration of the performed action is not taken into account on the evaluation step, so the action type is passed further to the platform step where time advances according to the action. For now we assume that any action of a particular type takes a xed amount of time for execution.
The evaluation rules take an expression and a local state and translate them to the new pair of expression and state and also emit an action for the platform step. Here are some examples of evaluation rules.
fs ` (e; s) act ! (e 0; s 0) fs ` (VarAssign vr e; s) act ! (VarAssign vr e 0; s 0) fs ` (VarAssign vr (Val vl ); s) EvalAct (exec-time VarAssignAct )! (Val Unit ; s(jev-st-local := ev-st-local s(vr 7! vl )j))
Several rules use information about locks and wait sets that is not included in the local state therefore they pull it from the full state.
: locked a fs fs ` (Sync (Val (Addr a)) e; s) lock-action a fs 0 ! (Sync (Val (Addr a)) e; s) locked a fs
fst (the (sc-lk-status (sc-info fs) a)) 6= runnint-th fs fs ` (Sync (Val (Addr a)) e; s) lock-action a fs 0 ! (Throw [ResourceSharingCon ict ]; s) locked a fs fs ` (Sync (Val (Addr a)) (Val v ); s)
unlock-action a fs 0 ! (Val Unit ; s)
5
We consider two models of program execution. The rst one is purely parallel, i.e.
each thread is assumed to execute on its own processor so that no thread waits
for CPU time. Another model is the sequential one when a program executes
on a single processor. The parallel model is easier, however, it does not seem to
be realistic. The sequential model represents the realistic situation for real-time
Java applications since the RTSJ (Real-Time Speci cation of Java [
The translated Java programs must be annotated with timing information about execution time of the following statement. The translation uses timing annotations to produce timed automata which model the program. The obtained system is model checked for possible resource sharing con icts. 5.1
We suppose that the translated program has a xed number of threads and shared elds, all of them de ned statically. The initialization code for threads and shared elds must be contained in the main method. The classes implementing Runnable interface must be nested classes in the class containing the main method. The required program structure is shown in the gure 2.
Each thread created in the program is translated into one automaton, and one more additional automaton modeling the Java scheduler is added to the generated system.
Java statements are translated into building blocks for condition statement, loop etc. which are assembled to obtain the nal automaton. Annotated statement is translated into its own block. Method calls and wait/notify statements are not translated for now.
The timed automata system contains an array of object monitors representing acquired locks on shared objects. When a thread acquires a lock of an object, the monitor corresponding to this object is incremented, and when the lock is released, the monitor is decremented.
There is a number of checks which are performed before on the program source code which guarantee correctness of the generated model. One of the most critical is the requirement that the whole parse tree must be annotated, i.e. for any leaf of the AST there is a timing annotation somewhere above this leaf. With this requirement the behavior of the generated system can be determined in each moment of time. public class Main {
Res1 field1 ; // shared fields declaration public static void main ( String [] args ){
Run1 r1 ; // declarations of Runnable object instances Thread t1 , t2 ; // thread declarations r1 = new Run1 () ; // Runnable objects initialization field1 = new Res1 () ; // shared fields initialization t1 = new Thread ( null ,r1 ," t1 "); // thread creation t1 . start () ; // thread start } private class Run1 implements Runnable { public void run () { // thread logic implementation
... }
} } private class Res1 { // resouce classes
... }
In the parallel model threads are supposed not to wait for processor time if they want to execute a statement. However, threads can wait for a lock if they need one which has been taken by another thread. Since this model is not very realistic we concentrate on the sequential model further.
In the sequential model we assume that at every moment of time only one thread or scheduler can execute. Threads which do not execute in a particular moment of time wait for processor time. Also threads can wait for a lock; waiting does not consume CPU time.
Automata communicate with the scheduler through channels: if the scheduler has selected one thread, it sends a message to it so the thread starts executing. After nishing its execution, the thread sends a message to the scheduler, and the next scheduling cycle starts. The scheduler uses channels run[i] to call the i-th automaton, and the automata use the channel scheduler to give the control back to the scheduler.
There is an array of clocks c[i], each of them corresponding to one thread automaton. These clocks are used to calculate time of annotated statements execution or sleeping time. There is also one clock cGlobal used for tracking global time.
final2
FINAL (a) Assignment (b) Sequence
(c) Annotation auxIf
start1
START
The building blocks and their translation are the following for the sequential model: (a) Assignment (3a). Three new states and two transitions between them are added. The transition from START to MIDDLE listens to the channel run[i], and the transition from MIDDLE to FINAL calls the channel schedule. The state MIDDLE is urgent since we assume that any statement except the annotated one takes time for execution. (b) Sequence (3b). Having two automata with start and nal states called start1, start2 and final1, final2 correspondingly, the states final1 and start2 are merged. (c) Annotation (3c). Three new states and two transition between them are added. The transition from START to MIDDLE listens to the channel run[i], sets the variable execTime[i] to the value of the current annotation and resets the clock c[i] to 0. The transition from MIDDLE to FINAL calls the channel schedule and resets the variable execTime[i] back to 0. The state MIDDLE has an invariant forbidding the automaton to stay in this state if the value of the clock c[i] bypasses execTime[i]. The transition from MIDDLE start1 to FINAL has a guard enabling this transition only if the value of c[i] is greater or equal to execTime[i]. The invariant and the guard ensure that the automaton would be in the MIDDLE state as long as the annotation claims. (d) Condition (3d,3e). Three new states and four transitions are added. If both if and else branches are presented, the nal states of automata representing the branch internals are merged. The states auxIf and auxElse are auxiliary states introduced to divide listening and calling transitions therefore they are made committed. Two transitions from START to auxIf and auxElse listen to the channel run[i], and the transitions from auxIf to start1 and from auxElse to start2 (or to final1 in case of absence of the else branch) call the channel schedule. (e) Lock (4a). Two meaningful states and two auxiliary states are added. The transition from START listens to the channel run[i] and has a guard checking whether a lock for the object in the argument of the synchronized statement is not taken by other threads. (f) Loop (4b). Two meaningful states and two auxiliary states are added. One transition from the START goes to the next loop iteration, another one exits the loop. Both transitions from START to auxLoop and auxEnd listen to the channel run[i]. The transitions from auxLoop to start1 and from auxEnd to FINAL call the channel schedule. Both auxLoop and auxEnd are made committed. The nal state of the automaton corresponding to the loop body is merged with the START state. (g) Sleeping (4c). The automaton for sleep statement resembles the automaton for annotated statement with additional elements for returning control to the scheduler during sleeping. There are three meaningful and two auxiliary states with transitions connecting them into a chain. The auxiliary states, auxSleep and auxWake, are committed. The transition from START to auxSleep listens to the channel run[i], sets the variable execTime[i] to the duration of sleeping period and resets the clock c[i] to 0. The transition from auxSleep to MIDDLE calls the channel schedule so that the scheduler can schedule other threads. The transition from MIDDLE to auxWake listens to the channel run[i] and has a guard enabling this transition only if c[i] is greater or equal to execTime[i]. The update on this channel resets the value of execTime[i] back to 0. Unlike the automaton for the annotated statement, there is no invariant in the MIDDLE state because a thread is not obliged to continue its execution right after it has woken up. It may wait for processor time before. The transition from auxWake to FINAL calls the schedule channel. 5.4
The Java scheduler maintains thread statuses and grants permission to execute to threads. The scheduler model has three states: scheduling, runThread, wait. The scheduler starts in the state scheduling which has transitions for updating thread eligibility statuses. When all thread statuses are updated, the scheduler moves to the state runThread calling the channel run[i] for some thread with index i which is eligible for execution. While the thread is executing, the scheduler stays in the state runThread. When the thread has nished its execution, it calls a channel schedule, and the scheduler returns back to the scheduling state, and the new scheduling cycle starts. If there was no thread eligible for execution, the scheduler goes to the wait state where it can stay for some time and repeat scheduling.
Each thread gets two transitions for status updates. One assumes that a
deadline for an action performing by a thread has passed, another one assumes that
the deadline has not been reached yet. In the rst case the ag isEligible[i]
is set to true, and the thread with index i can be scheduled for execution.
Otherwise, isEligible[i] is set to false, and the thread with index i cannot be
scheduled.
c[
schedule?
resetStatusUpdated()
resetStatusUpdated()
wait
runThread
c[
Each thread automaton starts in the scheduling state; after being scheduling scheduled it can go to one of the three states below. A thread is in the state //@ time @// executing if there is an assignment or deadline passed an annotated statement to be executed. A thread goes to the sleeping executing state if it has met a sleep call; if a thread wants to acquire a lock but it sleep(time) cannot because another thread owns deadline passed it, the active thread has to go to the blocked state and wait until another sleeping thread releases the lock.
wait for lock The listed states are general, and lock acquired automata may perform several internal steps while staying in the same blocked generalized state.
Based on the state classi cation above, the simulation function can be Fig. 6: Thread model used by the trans- easily built by mapping states of Java lation. semantics to states of TA semantics belonging to the same class. This is a preliminary thought concerning a construction of the simulation function. 6.1
We are in the process of carrying out a formal correctness proof. In the foreseeable future, we will concentrate on the following ingredients: 1. We will de ne a simulation relation between the TA semantics (Section 3) and the Java execution semantics (Section 4). Both semantics are instances of timed transition systems. 2. We show that for each thread i, the Java execution semantics of thread i is simulated by the execution semantics of the TA obtained from abstracting (Section 5) the thread. Thus: Let Ji be the code executed by thread i. Let T Ai = abstr(Ji) be the automaton obtained by the abstraction function sketched in Section 5. Then we show that Ji T Ai. 3. We establish an analogous simulation relation between the Java code of the scheduler JS and the corresponding timed automaton T AS (Figure 5), and show JS T AS.
Future work will concentrate on establishing a correspondence between timed
transition systems (TTSs), logics, and simulation, in the following sense:
1. We will formalize a notion of execution trace of a TTS, formalize an
appropriate temporal logic and establish the traditional model relation between
traces and formulae of the temporal logic. In this context, we hope to be
able to extend previous work described in [
This paper describes work in progress. The generation of Timed Automata out of Java code is still undergoing major changes, and the precise de nition of a correctness statement and its proof still have to be done.
We may however comment on some fundamental assumptions of our approach, which may in part seem unrealistic.
{ Obtaining WCET annotations: In the examples of this paper, the WCET
annotations are ctitious values. There are WCET analysis tools especially
geared at Java [
Acknowledgements. We are grateful to Marie Du ot-Kremer, Pascal Fontaine and Stephan Merz (Loria) and Jan-Georg Smaus (Irit) for discussions about this work.