A Formal Model of Resource Sharing Conflicts in Multithreaded Java ? Nadezhda Baklanova and Martin Strecker Institut de Recherche en Informatique de Toulouse (IRIT), Université de Toulouse {nadezhda.baklanova,martin.strecker}@irit.fr Abstract. We present a tool for analysing resource sharing conflicts 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 verified 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. Keywords. resource sharing, Java, timed automata, model checking Key terms. Model, Development, ConcurrentComputation, FormalMethod, QualityAssuranceProcess 1 Introduction 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 im- portant. 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 algo- rithms for linked lists, described for example in [4,11], are very complex, difficult to implement and, consequently, hard to verify. 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 (possi- bly infinitely 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-BLAN- 0310) A Formal Model of Resource Sharing Conflicts in Multithreaded Java 551 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 different moments of time. This is the motivation for our work: we develop a tool for checking resource sharing conflicts in concurrent Java programs based on the statement execution time. This gives a “time-triggered” [6] flavor to our approach of concurrent system design: resource access conflicts are resolved by temporal coordination at system assembly time, rather than during runtime via locking or via retries (as in wait-free algorithms). 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 (Sec- tion 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 verification 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 finished publication. 2 Informal Overview To show the main idea, we present an example of a concurrent Java program. It is a primitive producer-consumer buffer 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. private class Run1 implements Runnable { public void run () { int value , i ; // @ 1 @ // i =0; while (i <10) { synchronized ( res ) { // @ 2 @ // value = Calendar . getInstance () . get ( Calendar . MILLISECOND ) ; // @ 5 @ // res . set ( value ) ; } Thread . sleep (10) ; // @ 2 @ // i ++; 552 N. Baklanova and M. Strecker } } } private class Run2 implements Runnable { public void run () { int value , i ; // @ 1 @ // i =0; Thread . sleep (9) ; while (i <10) { synchronized ( res ) { // @ 4 @ // value = res . get () ; } Thread . sleep (8) ; // @ 1 @ // i ++; } } } One of the possible executions is shown in Figure 1. 01 8 20 Fig. 1: Possible execution flow. Black areas represent execution without locks, blue and green areas - execution within a critical section, grey areas - sleeping, white areas - waiting for processor time. After having translated this program to a system of timed automata we run the Uppaal model checker to determine possible resource sharing conflicts. The checked formula is A[]∀(i : int[0, objN umber − 1])∀(j : int[0, autN umber − 1])waitSet[i][j] < 1, (1) where waitSet is an array of boolean flags 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 conflicts are possible. A Formal Model of Resource Sharing Conflicts in Multithreaded Java 553 3 Timed Automata Model Timed automata are a common tool for verifying concurrent systems; the under- lying theory is described in [1]. We formalize the basic semantics of an extension of timed automata used in the Uppaal model checker. The formalized syntax and semantics are adapted from [3]. 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 final node. type-synonym ( 0n, 0a) edge = 0n × cconstr × 0a list × id set × 0n An invariant is a condition on a node which must be satisfied when an au- tomaton 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 defined 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 | Transition 0a list Accordingly, the timed automata semantics has two rules: delay and tran- sition. 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 satisfied. 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 final nodes must be satisfied 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. 554 N. Baklanova and M. Strecker varv 0 = varv (|cval := add (cval varv ) d |) varv |= invs l varv 0 |= invs l l ∈ nodes (nodes, init, edges, invs) ` (l , varv ) −Timestep d → (l , varv 0) (l , g, a, r , l 0) ∈ edges varv |= g varv 0 = eval-stmts varv a(|cval := reset (cval varv ) r |) varv 0 |= invs l 0 l ∈ nodes l 0 ∈ 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 [2]. Handshaking allows to synchronize two automata so that both take an edge simultaneously. (s 1 , g 1 , a, cs 1 , s 1 0) ∈ edges 1 (s 2 , g 2 , a, cs 2 , s 2 0) ∈ edges 2 a ∈ getEdgeActions edges 1 ∩ getEdgeActions edges 2 ((s 1 , s 2 ), g 1 d∧e g 2 , a, cs 1 ∪ cs 2 , s 1 0, s 2 0) ∈ edges-shaking edges 1 edges 2 (s 1 , g, a, cs, s 1 0) ∈ edges 1 a ∈ getEdgeActions edges 1 a ∈ / getEdgeActions edges 2 s 2 ∈ getEdgeNodes edges 2 ((s 1 , s 2 ), g, a, cs, s 1 0, s 2 ) ∈ edges-shaking edges 1 edges 2 (s 2 , g, a, cs, s 2 0) ∈ edges 2 a ∈ getEdgeActions edges 2 a ∈ / getEdgeActions edges 1 s 1 ∈ getEdgeNodes edges 1 ((s 1 , s 2 ), g, a, cs, s 1 , s 2 0) ∈ edges-shaking edges 1 edges 2 4 Java Model The look of the Java semantics has been inspired by the Jinja project [5] and its multithreaded extension JinjaThreads [7]. The Java execution flow is modeled by three transition relations: evaluation, scheduler and platform. The evaluation semantics is the semantics of a single thread, the scheduler semantics is respon- sible for thread scheduling, and the platform semantics formalizes the notion of time advancement. Taking into account the passage of time is the essential increment wrt. the above-mentioned semantics. Following Jinja, we do not distinguish expressions and statements; their datatype is the following: datatype expr = Val val | Var vname | VarAssign vname expr | Cond expr expr expr | While expr expr A Formal Model of Resource Sharing Conflicts in Multithreaded Java 555 | Annot annot expr | Sync expr expr | 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 fixed 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(|ev-st-local := ev-st-local s(vr 7→ vl )|)) 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) 556 N. Baklanova and M. Strecker 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 [ResourceSharingConflict], s) locked a fs fs ` (Sync (Val (Addr a)) (Val v ), s) −unlock-action a fs 0 → (Val Unit, s) 5 Abstracting Java to Timed Automata We consider two models of program execution. The first 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 Specification of Java [8]) specifies the behavior for monoprocessor systems only. 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 conflicts. 5.1 General principles We suppose that the translated program has a fixed number of threads and shared fields, all of them defined statically. The initialization code for threads and shared fields must be contained in the main method. The classes implement- ing Runnable interface must be nested classes in the class containing the main method. The required program structure is shown in the figure 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 final automaton. Annotated state- ment 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. A Formal Model of Resource Sharing Conflicts in Multithreaded Java 557 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 ... } Fig. 2: Required program structure 5.2 Parallel model 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. 5.3 Sequential model 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 finishing 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. 558 N. Baklanova and M. Strecker START start1 START run[i]? run[i]? execTime[i]=, c[i]=0 final1_start2 MIDDLE MIDDLE c[i]<=execTime[i] c[i]>=execTime[i] schedule! schedule! execTime[i]=0 FINAL final2 FINAL (a) Assignment (b) Sequence (c) Annotation auxIf start1 auxIf start1 schedule! schedule! run[i]? run[i]? START final1 START final1_final2 run[i]? run[i]? schedule! schedule! auxElse auxElse start2 (d) Condition I (e) Condition II Fig. 3: Building blocks for automata. Elements added on the current step are red; blue and green elements have been generated in the previous step. 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 an- notated one takes time for execution. (b) Sequence (3b). Having two automata with start and final 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 A Formal Model of Resource Sharing Conflicts in Multithreaded Java 559 start1 final1 run[i]? schedule! _monitor[j]-- schedule! auxIn auxOut auxLoop schedule! _monitor[j]==0 run[i]? run[i]? start1 _monitor[j]++, waitSet[j][i]=0 FINAL START START schedule! run[i]? auxWait _monitor[j]>0 FINAL run[i]? auxEnd waitSet[j][i]=true schedule! (a) Lock (b) Loop MIDDLE c[i]>=execTime[i] schedule! run[i]? execTime[i]=0 START auxSleep auxWake FINAL run[i]? schedule! execTime[i]=, c[i]=0 (c) Sleeping Fig. 4: Building blocks for automata. Elements added on the current step are red; blue and green elements have been generated in the previous step. 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 final 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. 560 N. Baklanova and M. Strecker (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 final 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 automa- ton for annotated statement with additional elements for returning control to the scheduler during sleeping. There are three meaningful and two aux- iliary 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 Scheduler 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 sched- uler stays in the state runThread. When the thread has finished 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 dead- line for an action performing by a thread has passed, another one assumes that the deadline has not been reached yet. In the first case the flag isEligible[i] is set to true, and the thread with index i can be scheduled for execution. Oth- erwise, isEligible[i] is set to false, and the thread with index i cannot be scheduled. A Formal Model of Resource Sharing Conflicts in Multithreaded Java 561 c[0]>=execTime[0]&&!isUpdated[0] c[1]>=execTime[1]&&!isUpdated[1] isEligible[0]=true, isEligible[1]=true, isUpdated[0]=true, isUpdated[1]=true, updateAllStatuses() updateAllStatuses() c[0]