Automated Analysis of Parametric Timing
Contents
1. A K a Intuitively Pre 7 U describes the set of backward reachable states in n gt 0 steps At the n th iteration the back ward reachability procedure computes the formula BR r U Vio Pre r U representing the set of states which are backward reachable from the states in U with at most n steps While computing BR r U the procedure also checks whether the system is unsafe by establishing if the formula I A Pre r U is satisfiable modulo PTS safety test or whether a fix point has been reached by checking if BR r U gt BR 1 r U is PTS valid or equivalently if the for mula BR 7 U nBR 1 7 U is PTS unsatisfiable fiz point test If a safety test is positive the procedure returns UNSAFE if this does not happen and a fixed point is reached the procedure returns SAFE The essential requirement in order to mechanize the procedure which might be non terminating for various known general reasons is the closure of 3 formulae under preimage computation In this way in fact a formula in the sequence BRo BR is an J formula and we need to check the satisfiability of conjunctions of 3 and V formulae which is decidable by using a general result in 10 Let K be an 3 formula while it is easy to show that Pre L K is equiva lent to an 3 formula for any location transition L it is unfortunately impossible to prove it for Pre E K Although the existential variable can be eliminated2. for Algorithm 3 we just want to check that such bounds are correct by using MCMT Thus we want to check that if some process is in the trying region and no process is in the critical region then before p C G time units have passed some process enters the critical region The first idea is the following i we add an absolute clock abSclock and a boolean flag k to the specification the Boolean flag k is permanently turned to t rue as soon as one process reaches the critical region ii we initialize the system by putting abs igck 0 k false and by saying that no process is in critical region and that the process having N as an id is in the trying region N is a new parameter of type INT subject to the constraint N gt 0 iii we consider unsafe the states in which abs iocx gt p C G and k false For various reasons the above idea is not correct indeed MCMT returns UNSAFE if you implement it even if the chosen bound p C G is correct We need to identify these reasons and make the suitable adjustments to our plan The reason for a first adjustment is clear MCMT adopts the stopping failures model due to the presence of universal quantifiers in transitions guards and in the stopping failures model deadlock freedom does not hold as a trivial coun terexample consider the run in which a process 7 sets the shared register x to i and then crashes thus preventing any other process to access the critical region fo
3. if j i then 2 else pc j A PR E ee x shared register initially 0 pce Aj if j i then 0 else peel i delay positive integer constant peli 3 A peeji gt 1 Av in L4 Ji pe dj if j i then 4 else pe j A repeat forever pce Aj if j i then 0 else pc j 1 remainder exit peli 4A peeli gt F Awl a2A 2 ifs 0 then goto L Ls Ji pe dj if j i then 5 else pe j A 3 1 4 DT eI pc Aj if j i then 0 else pc j 4 pause delay ae 5 if 2 4ithen goto L pelt 5A peli gt 1 Ar tAx g 6 critical entry Le Ji pe dj if j i then 6 else pc j A T oritical etit pch Aj if j i then 0 else pc j 8 x 0 peli 5 A pecli gt 1 Az i Ng g 9 remainder entryi L7 Ji pc Aj if j i then 2 else pe j A end repeat pc Aj if j i then 0 else pcefj pelt 6 A pecli gt 1 Aw Ls Ji pe Aj if j i then 7 else pe j A pc Aj if j i then 0 else pc j peli 7A pcefi gt 1 Av g Lg Ji pe Aj if j i then 8 else pc j A pch Aj if j i then 0 else pc j peli 8 A pecli gt 1 Az 0 Lio Ji pc Aj if j i then 9 else pe j A pc Aj if j i then 0 else pc j pe i 9 Aa 0 Lii Ji pe Aj if j i then 1 else pe j A pch Aj if j i then 0 else pc j Fig 2 Algorithm 2 pseudo code and location transitions pce above abbreviat
4. reachable state needs not to be definable however we can overapproximate it by using suitable lemmata This is in a sense the strategy of 15 suitable lemmata describing seemingly interesting properties of the reachable states are invented then they are formally proved and finally they are used when proving the correctness of time bounds for deadlock free dom In our experiments we proposed two lemmata for Algorithm 2 and three lemmata for Algorithm 3 such lemmata are checked by using MCMT itself in a total amount of time of 8 95 sec for Algorithm 2 and 236 51 sec for Algorithm 3 and then they are added as system axioms to the specification file of the time bounds for deadlock freedom we shall see below how to automatically synthe size the lemmata In other words we try to prove that the deadlock freedom property and the related time bound for the access to the critical region apply to all the states that satisfy the lemmata we found independently on whether such states are really reachable or not But now another problem arises MCMT diverges In fact termination is not guaranteed at all because we are outside the scope of decidability results known from the literature However the divergence source is limited and we can fruit fully apply a well know model checking technique namely acceleration this will be our third and last adjustment The point is that the sequence of the two transitions formed by line code L for a fi
5. c1 lt c2 and to C lt co c1 thus any gt M has this property 4 In our situation we have c 1 and c2 C thus Proposition 1 applies for C gt tland M gt 1 C 1 If we put M 1 C 1 the above Proposition indicates an accelerated transition solving our divergence problem we say that a transition is accelerated if after adding it to the current set of transitions the new runs that arise are obtained from old runs by replacing a sequence of steps by a single new step Still there is the problem that the atom e gt G4 is not linear hence it cannot be handled by the backhand SMT solver of McMT in addition the case C 1 is not covered In our experiments we used the transition Hide gt 1 peli L A pcctock t gt 1 A A V t pelj RM U 2 gt pcetock J lt C A A Vj pe y 2 gt pectock J e lt G A TAN abs rook abSclock te A pCroor AZ LE j i then 0 else Pceocklj By the above Proposition this transition is an accelerated transition in case 1 gt oy and C gt 1 that is only in case C gt 2 otherwise it may introduce spurious runs However since we luckily succeeded in proving time bounds for deadlock freedom in this way these time bounds apply to the general case too trivially if they apply to honest and possibly spurious runs they in particular apply to all honest runs Notice also that whenever we check tightness of these time
6. is of the kind i1 N A w t j alti alj k abSciock N Taking into consideration 9 and the instantiation algorithm for PTS satisfia bility given in 10 the PTS unsatisfiability of 10 means that the formula Yli J alis alg false 0 11 i gt peli Try 11 iEii j is not PTS satisfiable The idea is to check whether the negation of this formula can be used as a lemma i e if it is an overapproximation of the set of reachable states To check this it is sufficient to run MCMT on the problem having the standard initialization of Algorithm 2 resp 3 and having precisely 11 as an unsafe formula If the tool returns UNSAFE then the bound p C G is not correct because composing the two traces leading to the unsafe sets of states we have a counterexample showing that the time bound can be violated If the tool returns SAFE then we can repeat our attempt of verifying the time bound but in the new run we add the negation of 11 as a system axiom As a consequence the formula 10 is not satisfiable anymore and the tool won t exit if Ji i afi k absctock N is produced Of course the tool may still produce an UNSAFE outcome in which case the procedure must be repeated In the end provided divergence does not arise the tool either synthesizes enough lemmata and certifies that the time bound is correct or it finds a counterexample for it Time Bounds Synthesis The above procedure works independen
7. any execution if some process is in the trying region and no process is in the critical region then eventually some process enters the critical region Algorithm 1 enjoys property MEX but not DF Two timing constraints are crucial for Algorithms 2 and 3 15 TC1 the time interval between successive steps of a process i should be contained in c1 c2 for 0 lt c lt c2 lt 00 when i is in its trying or exit region and TC2 delay gt C c2 c where C is called the time uncertainty If TC1 TC2 are satisfied then both Algorithms 2 3 satisfy MEX and DF otherwise Algorithm 2 satisfies only property DF and Algorithm 3 satisfies only property MEX Since ideally timing based algorithms should guarantee mutual exclusion regardless of the timing constraints in this sense Algorithm 3 is better designed than Algorithms 1 and 2 Algorithm 1 can be formalized by a parameterized timed system T 0 pe x y global x global y pc 1 9 Z 271 0 where I Vi pc i 1 Ay 0 and the integers 1 9 stands for the labels 0b Oa in the pseudo code LT contains the location transition corresponding to the various instructions in the pseudo code The tuple of parameters and the set of time elapsing formulae of m are empty since time plays no role for an asynchronous algorithm like the Algorithm 1 Algorithm h 2 3 is formalized by a parameterized timed system of the form mp p an A h In LTn TE
8. bounds MCMT returns UNSAFE hence it does not diverge and we do not need the accelerated transition at all B The formalization of Algorithm 2 We report the full formalization of Algorithm 2 the Fischer protocol as a parameterized timed system a p a Ax I LT TE We have p C F G a PC PCclock Ax G gt F F gt C C gt 1 pc 1 9 global x Vi pcctock i OF I Vi pcii 1 Az 0 The location transition formulae in LT are derived from the pseudo code of Algorithm 2 and are reported in Figure 2 the names of the locations from Figure 1 have been renamed progressively as 1 9 to make comparison with location transitions easier The time elapsing transition TE is specified as follows t g Apd pe A Vida A pe AJ pcclj e gt 0 WwW where g is the conjunction of the following two conditions peli A 1A peli 4 4A peli 6A pelj 49 gt peeli lt C pelj 4 pe j e lt G the two conditions give upper bounds for the time a process can stay in a location from the trying or exit region peli 1 Aa z L Ji pe dj if j i then 2 else pe j A pc Aj if j i then 0 else pc j peli 2Apefi gt 1 Ax 0Az 2A Lo Ji pe dj if j i then 3 else pe j A pc Aj if j i then 0 else pcefj Algorithm 2 peli 2 Apel gt 1 Ax 40Ax 2A Lg Ji pe dj
9. maintained In the rest of the paper abusing notation we shall write a instead of afi or alj etc to emphasize that the exact value of the index used to dereference a constant array is immaterial System axioms Constraints on parameters p linear inequalities and the like are included in the set Ax of system axioms these axioms are added to the theory PTS and used in the satisfiability tests modulo PTS mentioned in next Section Obvious invariants known to the user e g the fact that the values of the clocks are always nonnegative the above assertions pc 1 global a etc can be introduced as further system axioms in MCMT specification files so that the tool can make use of them too Initial state formula We assume I a to be a V formula Location transition formulae We assume L a a to be of the form Lu i dx ali A a Aj Upd j i ali aly 1 aga where 7 is a variable of sort INDEX z is a conjunction of literals and the Upd are functions defined by cases i e by suitably nested if then else expressions whose conditionals are again conjunctions of literals To keep the technicalities to a minimum and since this is sufficient for the systems considered in this paper we consider only one existentially quantified variable i in 1 However the discussion can be generalized to location transitions with two quantified variables which are supported by MCMT and allow one to model a wid
10. the timing constraints We have illustrated our approach on the Lynch Shavit algorithm To the best of our knowledge it is the first time that a formal and automatic analysis of this algorithms is performed Key to the automated verification of deadlock freedom is the use of acceleration to avoid non termination combined with the automated synthesis of invariants to be used as lemmata in the main proof to realize a fully automated analysis procedure Related Work To the best of our knowledge analysis techniques for the ver ification of parameterized systems seldom consider the two dimensions of the parameters as we do here For example 9 17 consider only finite state pro cesses while 3 presents a method for the verification of a parametric number of timed automata with real valued clocks Our notion of parameterized timed systems is strictly more general than that in 9 17 by allowing for arithmetic variables and that of 3 by allowing for location invariants see Section 2 in timed transitions There is also a substantial body of work on the analysis of safety properties for parameterized systems with an arbitrary number of processes operating on bounded and unbounded variables see e g 13 14 20 These methods are not targeted to the verification of timing based algorithms and consider only safety properties whereas we also tackle the problem of verifying a restricted class of liveness properties The approach in 8 uses SMT t
11. timing constraints and deadlock freedom with timing constraints In Table 1 we check with McmMT that Algorithm 3 has the mutual exclusion property even without timing constraints rows 5 6 MCMT implements only a rudimentary form of abstraction which might be used during invariant search Since mutual exclusion for Algorithm 3 does not depend on timing information at all one can try to ask the tool to abstract away any timing information with this proof strategy mutual exclusion without timing constraints is established much quicker compare lines 7 and 6 from Table 1 We just mention that it is possible to quickly check with MCMT also other lemmata from 15 e g those that are used as ingredients for the proof of the deadlock freedom property 6 Automated Verification of Deadlock Freedom Algorithms 2 and 3 have the deadlock freedom property interestingly time bounds for waiting time are independent on the size of the network and can be expressed as linear polynomials p C G involving the parameters G and C This raises the possibility of verifying deadlock freedom using MCMT even if MCMT can only accept safety problems We first show how to do it with manual intervention and then we fully automatize the whole procedure by synthesizing both invariants and polynomial bounds 6 1 Verification We first suppose that we already know the linear polynomials giving the time bounds p C G 2 x G 5x C for Algorithm 2 and p C G 2 G 9 C
12. Automated Analysis of Parametric Timing Based Mutual Exclusion Algorithms R Bruttomesso A Carioni S Ghilardi and S Ranise 1 Universita degli Studi di Milano Milan Italy FBK Fondazione Bruno Kessler Trento Italy Abstract Deadlock free algorithms that ensure mutual exclusion cru cially depend on timing assumptions In this paper we describe our expe rience in automatically verifying mutual exclusion and deadlock freedom of the Fischer and Lynch Shavit algorithms using the model checker modulo theories MCMT First we explain how to specify timing based algorithms in the MCMT input language as symbolic transition systems Then we show how the tool can verify all the safety properties used by Lynch and Shavit to establish mutual exclusion regardless of the num ber of processes in the system Finally we verify deadlock freedom by following a reduction to safety problems with lemmata synthesis and using acceleration to avoid divergence We also show how to automati cally synthesize the bounds on the waiting time of a process to enter the critical section 1 Introduction In distributed systems deadlock free algorithms that ensure mutual exclusion crucially depend on timing assumptions For example the one proposed by Fis cher cannot guarantee mutual exclusion when all the steps of a process do not take time in a fixed interval while that proposed by Lynch and Shavit 15 guar antees that mutual exclusion is nev
13. Satisfiability Modulo Theories SMT techniques that cope with both kinds of parameters uniformly Although the reachability problem for parameterized timed systems is undecidable our experiments show that MCMT terminates when analyzing mutual exclusion and all the other safety properties considered in 15 for all the three algorithms Section 5 Interestingly safety properties can also be used to automatically verify deadlock freedom by reducing the analysis of the liveness property to reachability problems as outlined below The key observation is that the bound on the waiting time to enter the critical section is independent of the number n of processes in the system Thus deadlock freedom reduces to show that it is impossible starting from a reachable state of the system to reach the states where an interval of time has passed which is longer than the bound without recording the event that a process has entered the critical section In order to make the tool converge on these new problems we use acceleration techniques The role of lemmata is crucial to specify invariants overapproximat ing the notion of a reachable state first Section 6 1 we show how MCMT is able to check the invariants identified in 15 and use them as lemmata to prove deadlock freedom Then Section 6 2 we explain a technique to automatically synthesize such lemmata again by using MCMT and we report about our findings in its application for the fully automated ve
14. by using a standard quantifier elimination procedure for Linear Real arithmetic the main difficulty is posed by the universal guard in 2 namely Vj j alj In fact it is known see e g 2 that universal conditions are difficult to ana lyze automatically and require approximation techniques In MCMT the system is approximated by using the stopping failures model 16 similar to the ap proximate model of 1 2 According to this model processes can crash at any time and crashed processes remain so In this way the approximated system ad mits more runs than the original one and thus satisfies fewer safety properties As a consequence if the approximated system enjoys a safety property then we are entitled to conclude that also the original system does so In fact establish ing a safety property for the approximate system means that the system enjoys that property in a fault tolerant way i e even in presence of failures This will be the case for all safety properties considered in this paper and also for the deadlock freedom properties modulo some provisoes discussed in Section 6 below For a detailed description of how MCMT implements the stopping failures model and for information on how to check whether an unsafety trace applies to the original system the reader is pointed to 4 again all unsafety traces found in the experiments of this paper can be proved to apply to the original version of the system wi
15. e class of systems as observed in 10 Time elapsing transition We assume E a a to be of the form de 20 Vj gal alj Ab b c j clj 2 where g is a quantifier free formula is a variable of sort REAL and equality of tuples of variables is interpreted as the conjunction of componentwise equal ities The universal guard Vj c j alj is typically used to model a location invariant 3 Reachability for Parameterized Timed Systems Let m p a Ax I Lp a a n E a a be a parameterized timed system and U a be an 3 formula i e a formula of the form 3i i a i Assuming that the unsafe formula is an 3 formula allows us to express the complement of a large class of safety properties as these can usually be encoded as V formulae For example if location 4 is the critical section location the set of unsafe states violating the mutual exclusion property can be expressed by the 3 formula Jii i2 i1 i2 A pelii 4 A pcli2 4 saying that two distinct processes are in the critical section at the same time Given 7 and U a the symbolic backward reachability procedure iteratively computes the set of backward reachable states BR a as follows Preliminarily let us put r a a V Ln a a V E a a define also for n gt 0 the n pre image of a formula K a as Pre t K K and Pre t r K Pre r Pre r K where Pre 7 K da r a a
16. echniques to verify systems with several dimensions in the parameters but it only supports invariant checking or bounded model checking In 5 7 19 SAL is used to model check several timed systems In contrast to our approach that is fully automatic these approaches require some amount of user interaction which is reasonable given the large size of some of the sys tems especially those in 5 The model checker Uppaal 22 is capable of auto matically checking both safety and liveness of timed automata without timing parameters An extension of Uppaal described in 12 is capable of synthesizing linear parameter constraints for the correctness of the timed automata Both of these approaches are not parametric in the number of processes Our approach is parametric both in the number of processes and in the time constraints but does not attempt to perform the synthesis of linear arithmetic constraints al though in principle this would possible and we leave it to future work Here we focus on the automated synthesis of invariants to be used as lemmata in proving deadlock freedom In our previous work on MCMT 6 10 we have only considered safety proper ties of parametric systems while here we verify also a restricted class of liveness properties Furthermore the analysis presented here is much more fine grained than that in 6 because for instance specific time interval bounds are consid ered for each step of the protocols and not just
17. er violated even when the timing constraints are not satisfied As witnessed by the pen and paper proofs in 15 the veri fication of such a class of algorithms is a subtle and time consuming activity This is so because of the following two main difficulties First the verification should be done regardless of the number n of processes in the systems i e it must be parametric in n Second the waiting time of a process to enter the critical section is usually specified by means of a linear polynomial that is para metric in c and c2 where c1 c2 is the interval time in which any other step can be executed Hence for such a class of timing based systems there are two meanings of the word parametric This in turn implies that these systems have at least two dimensions along which they are infinite state To over come these difficulties we first introduce a class of symbolic transition systems called parameterized timed systems that support the declarative specification of timing based systems that are parametric in both the number of processes and the timing constraints Section 2 by using certain classes of formulae We also sketch how the three algorithms for mutual exclusion in 15 can be formally described as parameterized timed systems Section 4 Then we explain how to automatically solve reachability problems for parametric timed systems by using the Model Checker Modulo Theories McMT 11 Section 3 The tool uses
18. es PCelock
19. for few relevant locations This additional precision in the formalization significantly increases the difficulty of the verification tasks References 1 2 10 11 12 13 14 15 16 17 18 19 20 21 22 P A Abdulla G Delzanno N B Henda and A Rezine Regular model checking without transducers In TACAS volume 4424 of LNCS pages 721 736 2007 P A Abdulla G Delzanno and A Rezine Parameterized verification of infinite state processes with global conditions In CAV LNCS pages 145 157 2007 Parosh Aziz Abdulla and Bengt Jonsson Model checking of systems with many identical timed processes Theoretical Computer Science pages 241 264 2003 F Alberti S Ghilardi E Pagani S Ranise and G P Rossi Universal Guards Relativization of Quantifiers and Failure Models in Model Checking Modulo The ories JSAT 8 29 61 2012 Available at http jsat ewi tudelft nl content volume8 JSAT8_2_Alberti pdf G Brown and L Pike Easy Parameterized Verification of Biphase and 8N1 Pro tocols In TACAS pages 58 72 2006 A Carioni S Ghilardi and S Ranise MCMT in the Land of Parametrized Timed Automata In Proc of VERIFY 10 2010 B Dutertre and M Sorea Timed systems in sal Technical Report SRI SDL 04 03 SRI International Menlo Park CA 2004 J Faber C Ihlemann S Jacobs and V Sofronie Stokkermans Automatic Ver ification of Parametric Specifications with Complex T
20. ion i adds pcgiocr i gt 1 to the guards of those location transition formulae that modify a control location inside the trying or the exit regions Condition ii adds a conjuct of the form 3 to the universal guard of the time elapsing formulae with B set to C for each location inside the trying or exit regions the only exception is for the location corresponding to the pause instruction i e line 2 in the pseudo code of Algorithms 2 and 3 The second clarification is about the absence of the parameter delay and the presence of the parameters F and G that do not occur in the pseudo code of Algorithms 2 and 3 The idea is to replace the obvious Non Linear Arithmetic constraint in the formulae of m for h 2 3 modelling pause delay with a linear one involving F and G In fact the naive encoding of pause delay would require the use of the non linear term delay C to count the the number of nullary operations that the process should wait before continuing its computa tions Fortunately as observed in 15 the key property of pause delay is that its duration is greater than the time uncertainty C Thus the two additional parameters F and G are used to model the minimum and maximum time span that a process can spend inside pause delay In this way the time constraint TC2 is encoded in m for h 2 3 by adding i the condition Pcetock li gt F to the guard of the transition location in LT modifying the control location
21. lated as follows I3 If y 1 then some process i is not inside the remainder region Since MCMT proceeds by refutation in order to be proved I3 should be negated and formalized as the unsafety condition y 1 A Vi pcli 0a 0b 4 which is not an existential formula i e it cannot be handled directly by MCMT However it is not difficult to build an existential formula whose negation implies the safety property represented by the negation of 4 The idea is to add a historical variable H that records the id of the process that set y to 1 last initially H 0 we use H to replace 4 with the weaker statement y 1 A Ji i HA pci 0a 0b 5 which corresponds to the invariant 13 Ify 1 then the process H that set y 1 last is not inside the remainder region We shall implicitly use similar tricks to transform some other safety lemma statements arising in our experiments Algorithm 2 As discussed in Section 4 mutual exclusion for Algorithm 2 depends on timing constraints This is confirmed by MCMT as reported in the rows 2 3 of Table 1 Also it appears that checking mutual exclusion with the help of Lemma 4 1 I1 as suggested by 15 yields a substantial performance improvement see row 4 MEX I1 in order to use a Lemma MCMT first verifies it and then adds it to the set of system axioms Algorithm 3 Algorithm 3 combines the previous two and guarantees both mutual exclusion even without
22. n where p C F G az pc PCciock Z a3 PC PCclock Y Ax Ax U pc 1 9 Azs Ax U pc 1 13 global y with Ax G gt F F gt C C gt 1 global x Vi pcctock gt 0 h Vi pc li 1 Az 0 3 Vi pcli 1Ax OAy 0 the location transition formulae in LT are derived from the pseudo code as for Algorithm 1 the time elapsing formulae in TE is of the form 2 and the matrix q of the universal guard is a conjunction of formulae of the form pelj q gt Pceiocklj lt Ba 3 saying that the location q has a bound B that cannot be violated if Pcetock is updated to pcciock j Recall that transitions of the form 1 should have set the special clock variable pcciock j to 0 as soon as the process j enters location q Two clarifications about the role of the parameters C F and G are mandatory the full formalization of Algorithm 2 is reported in Appendix B First observe that without loss of generality it is possible to assume c 1 in this way we will be able to use only Linear Arithmetic constraints as prescribed by the definition of parameterized timed system of Section 2 Thus we have C co c c2 Because of the timing constraint TC1 a process is forced to remain in a location belonging to the trying or exit regions for at least 1 and at most C time units This is encoded in m for h 2 3 with the two following conditions i ii Condit
23. nite and known number of processes If the guard is satisfied both the data and clock variables of the involved processes are updated for example the value of some clocks may be reset Initially all the processes are in a distinguished initial state and their clock variables are set to zero The value of the clocks is always positive and ranges over R thereby modeling a continuous flow of the time In the rest of this section we explain how parameterized timed systems can be specified in the formal framework of 10 underlying the infinite state model checker MCMT 11 The idea is to use guarded assignment transition systems whereby state variables are functions mapping a subset of the integers used as identifiers of the processes to either a finite subset of the integers representing the locations of the automaton or an infinite set of time points representing the values of the clocks For simplicity we provide only an abstract characterization of the fragment of the MCMT input language that will be used to specify the class of parameterized timed systems the concrete syntax can be found in the on line user manual available at 21 Formalization We use multi sorted first order logic extended with the ternary expression constructor if then else We consider a sort INDEX for indexes of arrays the sorts INT and REAL for elements of arrays ARRAYiyr and ARRAYpgaz for arrays indexed over INDEX and storing elements of sort INT and REAL
24. o that backward search does not terminate The acceleration technique consists in inserting a single extra transition V gt m Tn for some M in the specification file if this operation succeeds the termination problems caused by the preimages of the mn would be solved The key question is whether transitions Tn are definable in the format allowed for MCMT transitions An answer is supplied by the following C1 Proposition 1 Suppose that co gt c and that M gt equivalent to TEE Then Vn gt m Tn is Hite gt Mee pelt L A Pccockli gt c1 A A Vj t pelj RM U 2 gt pectock j lt c2 A A Vj pelj 2 gt pectock j e lt G A A abs toon WSclock E A PC rock AJ if j i then 0 else pCciock j Proof All what we need is to show for every e that n e Meaq amp An gt Miei n c1 c2 s t lek k 1 Since the right to left side is obvious it is sufficient to prove the inclusion M c1 00 C U n c1 n c2 12 n gt M in fact if 12 holds for any gt M x c there is some n gt M such that n c lt E lt n c and we can take 1 En e n To show 12 it is sufficient to prove that for gt M the intervals c1 c2 and 1 c1 1 co overlap i e are such that 1 c c1 c2 However since c is positive 2 1 c1 c1 c2 is equivalent to 1
25. opologies In IFM volume 6396 of LNCS pages 152 167 2010 Yi Fang Nir Piterman Amir Pnueli and Lenore D Zuck Liveness with invisible ranking Software Tools for Technology 8 3 261 279 2006 S Ghilardi and S Ranise Backward reachability of array based systems by SMT solving termination and invariant synthesis LMCS 6 4 2010 Available at http www 1lmcs online org ojs viewarticle php id 694 amp layout abstract S Ghilardi and S Ranise MCMT A Model Checker Modulo Theories In Proc of IJCAR 2010 LNCS 2010 T Hune J Romijn M Stoelinga and F W Vaandrager Linear Parametric Model Checking of Timed Automata In TACAS pages 189 203 2001 S Krstic Parameterized system verification with guard strengthening and param eter abstraction In AVIS 2005 S K Lahiri and R E Bryant Predicate abstraction with indexed predicates ACM Transactions on Computational Logic TOCL 9 1 2007 N A Lynch and N Shavit Timing based mutual exclusion In Proc of IEEE Real Time Systems Symposium pages 2 11 1992 Nancy A Lynch Distributed Algorithms Morgan Kaufmann 1996 A Pnueli S Ruath and L D Zuck Automatic deductive verification with invis ible invariants In Proc of TACAS 2001 volume 2031 of LNCS 2001 S Ranise and C Tinelli The SMT LIB Standard Version 1 2 Technical report 2006 Available at http www SMT LIB org papers W Steiner and B Dutertre Automated Formal Verification of the TTEtherne
26. paper The constants in the tuple p are called real valued parameters and will be used to represent time bounds of a parameterized timed system which can be subject to some constraints such as being strictly positive or one being larger than another All the elements in p do not change their values over any run of the parameterized timed system State variables The tuple a is partitioned into two disjoint tuples b and c of sort ARRAYzyr and ARRAYpga_ respectively The variables in b are the data variables and those in c are the clock variables Concerning data variables we assume that there exists a distinguished variable pc short for program counter mapping indexes to a finite known set of integers that represent the control locations of an automaton Without loss of generality we assume pc to be con strained by Vi 1 lt pc A peli lt abbreviated as pc 1 4 for some given value gt 1 corresponding to the number of control locations The updates to the clock variables in c model the flow of time We assume that the tuple c con tains a distinguished variable PCelock that measures the time a process is staying in a given location Thus pcciock is initialized to zero and reset every time the corresponding location is changed In our framework a shared data or clock variable a is modeled as a constant array i e a is initialized and updated so that the invariant Vi j a i alj abbreviated as global a is
27. q and ii a conjunct of the form 3 in the universal guard of the time elapsing formulae in TE with B set to G where q is the control location associated to the pause instruction i e line 2 in the pseudo code of Algorithms 2 and 3 5 Automated Verification of Mutual Exclusion We begin by reporting the results of our experiments on verifying the mutual exclusion and other safety properties of the three algorithms All the specification files and scripts used in our experiments can be downloaded from the web page http www oprover org memt_lynch_shavit html Protocol Property Result Time s Notes Lamport MEX safe 0 04 MEX safe 2 64 T c specified Fischer MEX unsafe 3 73 T c not specified MEX I1 safe 0 02 0 17 0 19 Invariant added MEX safe 24 39 T c specified Lynch Shavit MEX safe 353 91 T c not specified MEX abstr safe 8 56 Uses MCMT s abstraction Table 1 Mutual exclusion experiments Experiments were run on an Intel i7 2 70 GHz running Ubuntu Linux 11 10 32 bits Algorithm 1 As it is clear from Table 1 MCMT verifies instantaneously the mutual exclusion MEX property of Algorithm 1 Although the related results are not shown in the Table the same applies to the three properties of Lemma 3 2 of 15 which are used as helper properties to derive theorems in the original paper We briefly discuss Property I3 because it is not a safety property It is formu
28. respec tively We assume the availability of the arithmetic symbols of Linear Arithmetic e g and lt and of the binary symbols _ ryr ARRAYiyr INDEX INT and Jrean ARRAYprat INDEX REAL to denote the array dereferencing operations by abuse of notation we omit the subscript INT or REAL when this is clear from the context Semantically we shall consider the class of structures where i INDEX is interpreted as a finite subset of the integers ii INT is interpreted as Z REAL as R and the usual arithmetic symbols have their standard meanings and iii ARRAY and ARRAYpgar are interpreted as the set of functions from a finite subset of the integers to Z and R respectively and _ _ is interpreted as function application According to the SMT LIB standard 18 a pair comprising a set of symbols and a class of structures also called models identifies a theory the theory described above will be called PTS in the rest of the paper If i is a tuple of variables of sort INDEX and a a tuple of array variables afi is a tuple comprising all terms of the kind a i for a a i i when writing o i al we mean that is a quantifier free formula that the 2 s are the only variables of sort INDEX occurring in and that all the variables of sort INT or REAL occurring in have been replaced by the terms ali of the corresponding sorts A V formula is a formula of the kind Vid i a i and an 3 formula is a formula of
29. rever However crashes can be tolerated without losing deadlock freedom provided some key actors do not crash there is a limited albeit sufficient pos sibility to tell this to MCMT Notice that whenever MCMT adopts the stopping failures models it automatically relativizes quantifiers to non crashed processes see 4 for details Recall also that a process that crashes is crashed forever as a consequence processes that are existentially quantified in the unsafety for mula cannot be crashed Thus the proposal is to use as unsafety formula the disjunction of the following three existential sentences Jii Sie ii N tg AT i2 A k false abSclock gt aC G 6 ii i1 N Az i Ak false dA absciock gt p C G 7 ii i1 NAx O0OAkK false absciock gt p C G 8 WwW W In this way we are guaranteed that process N i e the one who was trying to access the critical region from the very beginning does not get crashed and that in case an undesired state is reached it will be reached either with an uninitialized shared register or with the shared register set to the id of a non crashed process This is much weaker than saying that there are no crash failures at all but it is sufficient for our problems Still MCMT gives UNSAFE and now comes the reason for our second ad justment we need to constrain the initial states to be reachable states of our Algorithms 2 and 3 The notion of
30. rification of deadlock freedom 2 Parameterized Timed Systems The notion of parameterized time system is an extension of that of parametrised timed network in 3 with shared variables and universal conditions in the time elapsing transitions Informally a parameterized timed system is formed by a collection of finitely many identical processes Each process is a finite state au tomaton extended with data and clock variables that may be local or shared There are two kinds of transitions one modelling the passing of time specified by incrementing the clocks of the same amount of time and another one in which data variables are updated and a given number of processes usually 1 or 2 synchronize and change their states simultaneously Transitions of the first kind called time elapsing may be guarded by universal conditions on the val ues of the clocks i e by predicates involving the values of a finite but unknown number of clocks If the guard is satisfied all the clock variables are added of the same amount of time while the values stored in the data variables are left unchanged Universal conditions in time elapsing transitions allow us to model the so called location invariants i e guards forcing a process to leave a certain location before a fixed amount of time has passed Transitions of the second kind called location are guarded by existential conditions on the data and clock variables i e by predicates involving a fi
31. t Synchronization Quality In Proc of the NASA Formal Methods Symposium 2011 M Talupur and M Tuttle Going with the flow Parameterized verification using message flows In Proc of FMCAD 08 page 2008 MCMT web site http www dsi unimi it ghilardi mcmt Uppaal http www uppaal com A The accelerated transition In this Appendix we discuss the formal details concerning the accelerated tran sitions we introduced in our experiments Let us analyze the following sequence of steps in Algorithm 2 or 3 a process i with local clock pcctock i gt c executes the line code L then time has an increment by c1 c2 then i executes line L again then time has another increment c1 c2 etc etc If this is done n times the result is the following composed transition let us call it Tn Ji Jei En pcli L A pectock i gt c1 A Ager ci lt Ek lt c2 A A Vj i pelj g RM U 2 gt pectock J dip Ek lt c2 A A Vj pelj 2 gt pectock j 2 Ek lt G A A ab icek Sctock Do Ek A pC rook AQ LE j i then 0 else pcetock j 32 x for simplicity we omitted the updates of the arrays like the location array pc which are updated identically we also generically called RM the locations in the remainder region Now during MCMT runs for our deadlock freedom problems existential formulae K such that the formulae Pre t K are more and more informative varying n arise s
32. the kind Ji i a i A parameterized timed system pts is a tuple p a Az I L a a E a a where p is a tuple of parameters a is a tuple of state variables Ax is a finite set of system axioms I is the initial state formula L is a finite set of location transitions and E is a time elapsing transition Intuitively a and a denote the values of the state variables immediately before and after respectively of the execution of a transition We also assume the following proviso on the components of the pts Parameters The tuple p is composed of an array constant id of sort ARRAYqyr and a tuple p of constants of sort REAL The constant id maps indexes to a finite unknown set of integers to allow for indirect dereference of arrays by integers We assume id to be injective i e it satisfies Vi j d i id j gt i 7 and its co domain to be the set of positive integers i e it also satisfies Vi id i gt 0 In other words zd is a casting function from integers to indexes for more details on the role of id the reader is pointed to 4 In the rest of the paper for the sake of simplicity we will simply write 7 in place of id i this syntactic sugar is also allowed by MCMT input language and omit to list id among the parameters in p The fact that 0 and negative integers cannot be considered as identifiers will turn out to be useful in the specification of the algorithms considered in this
33. thout failures We just point out that after moving to the stopping failures model the desired closure property of 3 formulae under preimages holds 4 The Lynch Shavit Algorithm Lynch and Shavit 15 develop a time based algorithm for mutual exclusion by combining two other algorithms for mutual exclusion a Lamport style asyn chronous algorithm see e g 16 and the well known Fischer s timed mutual exclusion algorithm The three algorithms presented in 15 consist of a finite but unknown number n of identical processes running concurrently Each pro cess is composed of four regions of code remainder the region of code not concerned with Process i the access to critical resources trying the region of code where the process tries to acquire access to the critical region critical the region of code with exclusive access critical region exit the region of code where the process exits exit region from the critical region end repeat repeat forever remainder region trying region Algorithm 1 x y shared registers initially y 0 repeat forever Ob remainder exit L x i Algorithm 2 x shared register initially 0 delay positive integer constant repeat forever Ob remainder exit L if 40 then goto L Algorithm 3 x y shared registers initially 0 delay positive integer constant repeat forever Ob remainder exit L if 40 then goto L 1 if
34. tly on the fact whether the time bound we suggest to the tool is correct or not thus it is possible to use it in order to get the optimal polynomial p C G In fact what we are looking for is a linear polynomial a x C 8 G with positive integers coefficients we can just begin with a 1 8 1 and then increment the values with a dichotomic search as soon as we get a counterexample The statistics of our experiments for values close to the optimum are reported in Table 2 Protocol a B Bound Holds Iterations Time s 2 2 NO I 62 06 2 4 NO 5 110 68 Fischer 2 5 YES 8 155 56 2 6 YES 6 130 69 2 10 YES 3 51 25 252 NO 1 224 74 2 8 NO 11 5764 42 Lynch Shavit 2 9 YES 16 27995 78 2 10 YES 10 6935 91 2 14 YES 3 974 06 Table 2 Time bounds synthesis The table reports the attempts of checking a poly nome with given a and coefficients The optimal values found 2 5 for Fischer and 2 9 for Lynch Shavit coincide with the known theoretical optimal bounds Experiments were run on an Intel i7 2 70 GHz running Ubuntu Linux 11 10 32 bits 7 Discussion We have described how mutual exclusion and deadlock freedom of a class of timing based algorithms can be specified and automatically verified by the model checker MCMT We have highlighted how two kinds of being parametric are sup ported by our framework namely with respect to the number of processes in the system and the symbolic constants in
35. xed process 7 and time elapsing can be indefinitely applied we need to insert a further transition modeling n executions of this sequence for an arbitrary n This is definable in the format accepted by MCMT details are shown in the Appendix A below After this last adjustment MCMT is able to check the time bounds in 80 97 sec and in 1374 38 sec for Algorithms 2 and 3 respectively 6 2 Synthesis The insertion of the accelerated transition is the only manual intervention that is actually needed In fact both the lemmata used to overapproximate the set of reachable states and the polynomial p C G can be synthesized Invariant Synthesis Suppose first the polynomial p C G is fixed let us run MCMT on our Algorithm 2 or 3 with the unsafety formula given by the dis junction of 6 8 and with the initial formula I a abSclock k given by the statement suggested in 6 1 ii namely absciock 0 A k false A Vi i N gt pei Try 9 here pcli Try abbreviates a disjunction saying that pc i is equal to one of the locations of the trying region The tool returns UNSAFE by producing an 4 formula P Ji i ali k absctock N which means that that during the safety check the formula Jig i ali k abSclock N A I a abSclock k 10 is reported to be PTS satisfiable Now notice that 6 8 all contain the con junct i1 N which is not modified during the calculus of preimages thus i alt k abSciock N
36. y 0 then goto L ke gi lo ge 2 y 1 2 pause delay 2 pause delay 3 if i then goto L 3 if x i then goto L 3 if x i then goto L 4a critical entryi 4a critical entryi Start of Critical Region 4b critical exit 4b critical exit 4 if y 0 then goto L 5 y 0 5 a0 5 y Te Oa remainder entry Oa remainder entry 6 if x i then goto L end repeat end repeat Ta critical entry Tb critical exit 8 y 0 End of Critical Region 9 x2 0 Oa remainder entryi end repeat 1 2 3 Fig 1 The three Algorithms from 15 code for process i 1 Lamport s Style Mutual Exclusion 2 Fisher s Timed Mutual Exclusion 3 Lynch Shavit s Combined Mutual Exclusion The pseudo code of a process i belonging to the three algorithms taken verbatim from 15 is shown in Figure 1 Algorithm 1 is asynchronous while Algorithms 2 and 3 are timing based the time interval between successive steps of a process i is assumed to range in some interval of time when 7 is in its trying or exit region The instruction pause k causes the process to delay by a number k 1 of steps Intuitively pause k is equivalent to a sequence of k 1 no operations The idea is to choose values for time parameters in Algorithms 2 and 3 so as to guarantee the two key properties Mutual Exclusion MEX in any reachable state at most one process is in its critical region Deadlock Freedom DF in
Download Pdf Manuals
Related Search