Home

Liveness with Invisible Ranking*

Contents

1. 1 Computing the universal invariant according to the previous methods we obtain o Vi at_fo 1 V chan i which is inductive but insufficient in order to establish the existence of a helpful transition for every pending state in N natural where N gt 1 chan array 1 N of boolean where chan i i 2 loop forever do 0 if chan i then chan i chan i amp 1 0 1 go to 0 1 await chan i Critical Fig 4 1 Program CHANNEL RING 4 1 Generalizing project generalize We provide a sketch of the extension that enables com putation of a V 3 construct by obtaining a Vi u i 3j e 3 invisible invariant As before we pick a value No instantiate S No and use the pron etel endis proce dure to derive an inductive V assertion y Vi u i As a byproduct of project amp generalize we compute reach o the set of states reachable in S No Being inductive and implied by the initial condition the assertion is an over approximation of reach In order to isolate the anticipated assertion e j we first compute the differ ence between the concrete reachable set and y denoted here by o4 Obviously we proceed only if o4 is non empty Then we project amp generalize by replacing in dex 1 by k az below Finally we negate the result to get the proposed existential invariant o3 below Algorithm ar uli A r dth s ag a l K Q3 703 We use 3k o k as the c
2. can access some but not all of its neighbor index bool array entries Then it suffices to find processes that agree on the part of the state observable by their neighbors and not the complete state Chains of Consecutive Free Variables If in addition to N 1 there are longer or other chains of consecutive values the bound is reduced accordingly since there are less gaps to collapse E g when there is a N 1 N 1 combination the K 1 in the bound can be replaced by K 2 6 38 Example Dining Philosophers We demonstrate the use of the modest model theorem by validating accessibility for a classical solution to the dining philosophers problem using rule DISTRANK Consider program DINE that offers a solution to the dining philosophers problem for any N philosophers The program uses semaphores for forks In this program N 1 philosophers processes P 1 P N 1 reach first for their left forks and then for their right forks while P N reaches first for its right fork and only then for its left fork Program DINE is presented in Fig 6 1 The semaphore instructions request x and re lease x appearing in the program stand respectively for when z 1 do z 0 and x 1 Conse quently the transition associated with request x is compassionate indicating that if a process is requesting a semaphore that is available infinitely often it obtains it infinitely many times
3. As outlined in Section 2 4 we transform the BFTS into a compassion free BFTS by adding two new boolean arrays nur and nvr each nvr i corresponding to the request of process i at location 6 Appendix A 3 describes the BFTS we associate with Program DINE The progress property of the original system is 1 gt O z 3 which is proved in two steps the first establishing that 2 1 O a z 2 and the second establishing that z z 2 2 O a z 3 For simplicity of pre sentation we restrict discussion to the latter progress property Since P N differs from P 1 P N 1 and since it accesses y 1 which is also accessed by and y N which is also accessed by P N 1 we choose some z in the range 2 N 2 and prove progress of 2 The progress property of the other three processes can be established separately and similarly Taking into ac count the translation into a compassion free system the property we attempt to prove is 2 2 gt O a z 23 V Err 2 lt z2 lt N 2 where Vi 1 A wi nvri i V Err Viza n i 1 2 2 y i nvra i 1 v a N 21 nvrilN V 2 2 y N nvra N 6 4 Automatic Generation of Symbolic Assertions Following the guidelines in Section 3 we instantiate the program DINE according to the small model theorem compute the auxiliary concrete constructs for the instan tiation and abstract them Here
4. The initial values are determined as follows for each i 1 k the initial value of nur is taken to be T iff is disabled at all positions of Next we consider a step from position j to position j 1 If s V Z sj 1 V then we let 1 Nvr S Nvr That is if at least one system variable of system 5S is modified in step j then all the Nvr variables preserve their values On the other hand if step j is a stuttering step ie s V s 41 V we search for a transition C such that S nvri F but is disabled at all posi tions beyond j If there exists such a transition let m be such a transition with the minimal index We set S 41 nvr T and 8 4 nvr 8 nvr for all L Z m If there does not exist a 7 such as described above we let again 41 Nur 8 Nvr Since as previously observed all computations con tain infinitely many stuttering steps the above definition guarantees that nur eventually turns T iff 7 eventually becomes continuously disabled Furthermore we never have a state in which 7 is enabled while nvr T In the other direction consider an Err free computa tion c of S We claim that o c l y is a computation of S Suppose by contradiction that some 7 C is en abled infinitely often but taken only finitely often in Then it must be the case that f2 7 is enabled infinitely often in As 7 is taken finitely often in c it must be the case that nur is s
5. 3 l 1 3 il Applying this procedure to TOKEN RING 6 we ob tain the symbolic helpful assertions described in Appen dix A 2 3 2 4 Computing Concrete and Abstract i s As before we begin by computing the concrete rank ing functions i We observe that g i should equal 1 on every state for which 7 i is helpful and should de crease from 1 to 0 on any transition that causes a helpful Tk i to become unhelpful Furthermore i can never increase It follows that i should equal 1 on every pending state from which there exists a pending path to a pending state satisfying hf i Thus we compute og li pend or EU hg i where EU is the existential until CTL operator This formula identifies all states from which there exists an r free path to an hg 2 state Having found the concrete i we obtain the ab stract 1 by using project amp generalize as follows for each k 0 m we let 1 1 1 1 and i c 3 1 gt 1 3 o i The abstract ranking function obtained by applying this procedure to TOKEN RING 6 are described in Ap pendix A 2 9 8 Validating the Premises Having computed internally the necessary auxiliary con structs and checking the invariance of o it only remains to check that the six premises of rule DISTRANK are all valid for any value of N Here we use the small model theorem stated in Theorem 2 1 which allows us to check
6. i 4 1 tloc j tloc 4 toc i lt gt 2 toc lt j tloc 4 A Note that this computation is very similar to the sym bolic computation of the predecessor of an assertion where map 2 i 4 j serves as a transition relation In deed we use the same module used by a symbolic model checker for carrying out this computation Yi Fang et al Liveness with Invisible Ranking 9 3 2 2 Computing Concrete and Abstract pend Compute the assertion pend Po q r o po r characterizing all the states that can be reached from a reachable q r state by an r free path Then we take pend2 pend 1 1 and pend i pend l 1 3 i Thus for TOKEN RING 6 pend 1 1 We therefore take pend 1 1 and pend i at amp 1 at_ o i V tloc i Finally pend pend AViA1 pend i yielding Vizl at o 1 i V tloc i pend 1 1 3 2 3 Computing Concrete and Abstract hj i s We compute the concrete helpful assertions h i This is based on the following analysis Assume that set is an assertion characterizing a set of states and let 7 be some just transition We wish to identify the subset of states within set for which the transition 7 is an escape transition That is any application of this transition to a state takes us out of set Consider the fix point equa tion setn En r A AX V set
7. their validity for all values of N lt No for the cutoff value of No which is specified in the theorem First we have to ascertain that all premises have the required VJ form For auxiliary constructs of the form we have stip ulated in this Section this is straightforward Next we consider the value of No required in each of the premises and take the maximum Note that once y is known to be inductive we can freely add it to the left hand side of each premise which we do for the case of Premises D5 D6 and D7 that unlike others do not include any inductive component Usually the most complicated premise is D2 and this is the one which determines the value of No For pro 10 Yi Fang et al Liveness with Invisible Ranking gram TOKEN RING this premise has the form where we renamed the quantified variables to remove any naming conflicts Vc pend c Va pend a 2 3i 41 V3 j1 3 i1 j 01 which is logically equivalent to Vi i1 c Ja j 5 gt rv pena e The index variables which are universally quantified or appear free in the formula above are i 71 c tloc 1 N whose count is 6 It is therefore sufficient to take No 6 Having determined the size of No it is straightforward to compute the premises of S N for all N No and check that they are valid using BDD symbolic methods We cannot use the same form of auxiliary constructs to automatically verify algorithm BAK
8. we chose an instanti ation of No 6 obviously we need No gt 4 it seems safer to allow at least a chain of three that does not de pend on the special three hence we obtained 6 For the progress property we chose z 3 and attempt to prove 7 3 2 a 3 3 Due to the structure of Program DINE process P i depends only on its neigh bors thus we expect the auxiliary constructs to include only assertions that refer to two neighboring process at the same time We chose to focus on pairs of the form 4 401 We first compute y i i 1 which is the abstrac tion of the set of reachable states We distinguish be tween three cases i 1 i N and i 2 N 1 For the first we take reach l 1 6 N 1 6 project the concrete reach on 1 and 6 and generalize to 1 and N for the second we take o reach 6 gt N 5 gt N 1 ie project the concrete reach on 6 and 5 and generalize to N and N 1 and for the third we take o4 y reach 3 gt i 2 i 1 i e project the concrete reach on 3 and 2 and generalize to i and i 1 The abstract pending sets we obtain are in Ap pendix A 3 We then define Pa pA vA A Vi d 1 N p t t 1 and define pend o A m 3 2 For the helpful sets and the 6 s we obtain as ex pected assertions of the type p i 1 The assertions are described in Appendix A 3 14 Yi Fang et al Liveness with Invisible R
9. 6 2 and demonstrate its applica tion in Subsection 6 3 6 1 Modest Model Theorem Consider a parameterized BFTS S N with no data vari ables or arrays Let the formula q Vidj R i j be an V3 formula where R i j is a restricted assertion aug mented by operators 1 and 61 which refers to quanti fied index variables i and j We show that if there exists some model that does not satisfy this assertion then there exists a model smaller than a certain bound that This is in fact the way that assertions containing 1 and 1 are handled in APR 01 A simple conversion of this type is given in Example 2 1 3 This assumption is here for simplicity s sake and can be re moved at the cost of increasing the bound 12 Yi Fang et al Liveness with Invisible Ranking does not satisfy it The proof follows by contracting a model that does not satisfy y to a smaller model that does not satisfy y In order to decrease the size of the model again we count the number of existentially quan tified variables in the negation of y This time as R may contain 61 and O1 we ensure that in the smaller model each of these variables refers to a different process and in addition also pay attention to the way we handle the chain of processes between every two existentially quan tified processes Let K be the number of universally quantified index variables index constants including 1 and N and free index variable
10. AX set 3 1 The equation states that every state must satisfy set En r every p successor of a state is either a state or lies outside of set and every 7 successor of a state lies outside of set Note that the expressions AX v and AX w can be computed by po v and 7 7 o respectively By taking the maximal solution of the fix point equa tion 3 1 denoted v set En r aset A AX set we compute the subset of states within set for which 7 is helpful Following is an algorithm that computes the concrete helpful assertions 7 i corresponding to the just tran sitions of system S No For simplicity we will use T T No as a single parameter Let set En r A mazxfiz set r vd vcn AX set for each 7 T No do h 0 set pend _ for all 7 T No s t maxfiz set T 40 do hr h V masfix set T set set ah The for all r 7 No iteration terminates when it is no longer possible to find a r 7 No that satis fies the non emptiness requirement The iteration may choose the same more than once When the iteration terminates set is 0 i e for each of the states covered under pend there exists a helpful justice requirement that causes it to progress Having found the concrete hg i we compute the ab stract hf i by using project amp generalize as follows for each k 0 m we let h2 1 hg 1 1 1 and Ag i h
11. Consider a BFTS S with set of transitions 7 N 0 m x N as in Subsection 3 1 For every state in S N define a pre order lt over 7 From the totality of lt every S N state has some 7 i 7 which is minimal accord ing to lt We replace premise D4 in DISTRANK with a premise stating that for every pending state s the tran sition that is minimal in s is also helpful at s We call the new rule PRERANK and to avoid confusion name its premises RI R7 Thus PRERANK is exactly like Drs TRANK with the addition of a pre order 4 X 27 7 premises ascertaining that the relation lt is a pre order R8 R10 and replacement of D4 by In order to au tomate the application of PRERANK we need to be able to automatically generate the pre order relation lt As usual we first instantiate S No compute concrete lt o and then use the method project amp generalize to compute an abstract x The main problem is the computation of the concrete lt o We define s E lt if s H for the following CTL formula pend W hn V n 72 ERIS pend W where YV is the weak until or unless operator The intuition behind the first disjunct is that for a state s transition is helpful earlier than if every path departing from s doesn t reach h before it reaches The role of the second disjunct is to guarantee the totality of lt so that when becomes helpful ear
12. all processes other than P 1 We take q i to be the generalization of r obtained by replacing each reference to a local variable P 1 x by a reference to P i z The obtained q i is our candidate for the body of the inductive assertion y Vi q i We refer to this generalization procedure as project amp generalize For example when computing invisible invariants w is the set of reachable states of S No The procedure can be easily generalized to generate assertions of the type Vii 1 Having obtained a candidate for the assertion y we still have to check the validity of the premises of the proof rule we wish to employ Under the assumption that our assertional language is restricted to the predicates of equality and inequality between bounded range integer variables which is adequate for many of the parameter ized systems we considered we proved a small model theorem according to which for a certain type of as sertions there exists a small bound No such that such an assertion is valid for every N iff it is valid for all N lt No This enables using BDD techniques to check the validity of such an assertion The cases covered by the theorem are those whose premises can be written in the form Vi3j v i 1 where v i 1 is a quantifier free as sertion that may refer only to the global variables and the local variables of P i and P j V3 assertions for short Being able to validate the premises on S No has th
13. assertions Related Work This is the full version of FPPZ04b FPPZ04a See ZP04 for a survey on the method of invisible constructs and an earlier version of invisible ranking The problem of uniform verification of parameterized systems is undecidable AK86 One approach to remedy this situation pursued e g in EK00 is to look for re stricted families of parameterized systems for which the problem becomes decidable Unfortunately the proposed restrictions are very severe and exclude many useful sys tems such as asynchronous systems where processes com municate by shared variables Another approach is to look for sound but incom plete methods Representative works of this approach include methods based on explicit induction 5 network invariants that can be viewed as implicit in duction LHR97 abstraction and approximation of net work invariants CGJ95 and other methods based on abstraction GZ98 Other methods include those rely ing on regular model checking e g JN00 that over come some of the complexity issues by employing ac celeration procedures methods based on symmetry re duction e g GS97 or compositional methods e g McM98 combining automatic abstraction with finite instantiation due to symmetry Some of these approaches such as the regular model checking approach are re stricted to particular architectures and may occasion ally fail to terminate Others requ
14. i We proceed to show that s o x To do so con sider an arbitrary assignment assigning to each vari able v j a value 1 N We will show that s a 8 H R i j If this can be shown for every arbi trary assignment f it follows that s o H Vj R i 1 That is s a x Consider the assignment interpreting each v j as r r 1 N1 iff amp v g r Since s a H x it follows that s o 8 E R i j By induction on the structure of the formula R i j we can show that every sub formula y R i j evaluates to T under the joint interpretation s 3 iff y evaluates to T under the in terpretation s a j We conclude that s a H x which leads to the result that is satisfied in the state 6 of system S N Thus s is obtained from s by leaving the values of the index variables in the range 1 m intact reducing the index variables larger than n by n m while main taining the assignments of their index bool vari ables Obviously 6 is a state of S N1 n m that sat isfies w 6 2 Calibrating No The bound computed in Theorem 6 1 may be quite large In some cases it can be reduced significantly as we ex plain below General bool s If there are index bool arrays for arbitrary finite bool L in the bound should be replaced by the product of the sizes of ranges of all
15. m 3 1 jA arll 4 2 3 v V i j lt 2 BV ylz lt yli vB Vylz lt vb Vali gt 2v o Fig A 3 Pre order for Program BAKERY
16. oe a erie 7 3 A at dum 2 pres nvr i nvr2 i h j T T 2 7 ead presul 1 mj 4 gli i N y I pres g ND A Stl pres m T m n 1 zn Q1 3 nvra j dico nvri j nvra j r j 1 2 2 nvre j 1 j lt 3 g j norli A pres rlil vl morali i C BU otis zu ddr mei nvra i 1 2 j pres n 5 y j nvr1 j nvra j mS Vig i5iely i i i 2 m li 3 A pres nors i nvra i z 14s NO Mb y i 1 A pres ylil 1 GEN gt INI VIN zresMD pres r i 1 nvri i 1 nvra i 1 mom 7 yli 1 7 Ber A nvr5 i pres n i yli nvr i pres x i 1 yli 1 nvri i 1 nvr2 i 1 as mj yi ner 7 nvrz Wi At 3A n i 4 rs i nvr i nvra i J pres n j yli nvr1 j nvr2 j o Acn Z i i 1 A m i 0 A pres nvri i nure i JA y i 1 a 1 y i 1 nvr1 i 1 nvr2 i 1 bei il vj neri j Tia Vj pres x j 7 7 7 JI ni Ta 2 a 0 Ta 3 Tia Fig A 2 BFTS for Program DINE y N 1 N 1 lt 2 tN 1 22 N 3 Pn um E os Yi Fang et al Liveness with Invisible Ranking ra eb feb Talj j z V r z 2Aa Atli 4 3 1 1 j zVaiz 1 Vi j mn z3 Vi j
17. require user guidance and interaction and place additional burden on the user The difficulties in the execution of these two tasks are the main reason why deductive verification is not used more widely A representative case is the verification of invariance properties using the proof rule INV of MP95 in order to prove that assertion r is an invariant of program P the rule requires coming up with an auxiliary assertion p that is inductive i e is implied by the initial condition and is preserved under every computation step and that strengthens implies r In PRZ01 APR 01 we introduced the method of invisible invariants that offers a method for automatic generation of the auxiliary assertion y for parameterized systems as well as an efficient algorithm for checking the validity of the premises of INV The generation of invisible auxiliary constructs is based on the following idea it is often the case that an auxiliary assertion for a parameterized system S N has the form Vi 1 N q or more generally Vi j q i 1 We construct an instance of the parameterized system taking a fixed value No for the parameter N For the finite state instantiation S No we compute using BDDs some assertion v that we wish to generalize to an 2 Yi Fang et al Liveness with Invisible Ranking assertion in the required form Let r1 be the projection of w on process P 1 obtained by discarding references to variables that are local to
18. space results for DINE took to validate each of the inductiveness of y and all the premises D1 D7 on the largest instantiation 128 philosophers Checking all instantiations 2 128 took less than 8 hours 7 Imposing Ordering on Transitions Sections 3 4 dealt with helpful transitions h i and ranking functions which depended only on the single in dex i In the previous section we showed how to extend this approach to the case in which h i may also depend on indices 181 and i81 In this section we study helpful assertions that depend on all j Z i Such multiple index helpful assertions appear quite frequently As a matter of fact most helpful assertions seem to be of the type h t Vj p i j where i is the index of the process which can take a helpful step and all other processes 1 satisfy some supporting conditions However such a helpful as sertion presents a problem when trying to verify premise D4 of rule DISTRANK since we obtain an 3V disjunct in the premise In this section we show a new proof rule for progress that allows us to order the helpful assertions in terms of the precedence of their helpfulness The help ful assertion is then the minimal in the ordering so that we can avoid the disjunction in the r h s of Premise D4 Yi Fang et al Liveness with Invisible Ranking 15 7 1 Pre Ordering Transitions A binary relation lt is a pre order over domain D if it is reflexive transitive and total
19. transitions Every transition T T is an assertion 7T V V relating the values V of the variables in state s X to the values V in an S successor state 5 X Given a state s X we say that s X is a r successor of s if 6 6 T V V where for each v V we interpret v as sfv and as s v We say that transition T is enabled in state s if it has some T successor otherwise we say that 7 is disabled in s Let En r denote the assertion JV r V V characterizing the set of states in which 7 is enabled and let p denote the disjunction of all transitions ie p V ez T The assertion p represents the otal transition relation of S e J C T A set of just transitions also called weakly fair transitions Informally 7 J rules out compu tations where is continuously enabled but taken only finitely many times e C CT A set of compassionate transitions also called strongly fair transitions Informally r C rules out computations where 7 is enabled infinitely many times but taken only finitely many times For technical reasons and with no loss of generality we assume that 7 always contains the idling transition To V V which preserves the values of all system variables Taking such a transition is often described as a stuttering step We also require that the idling transi tion is taken to be a just transition Let s 1 82 be an infinite sequence of state
20. two directions e Allowing expressions such as i 1 to appear both in the transition relation as well as the auxiliary con structs This is especially useful for ring algorithms where many of the assertions have a p i i 1 or p i 1 component e Allowing helpful assertions and ranking functions belonging to transitions of process i to be of the form h t Vj H i j where H i 1 is a quantifier free as sertion Such helpful assertions are common in un structured systems where whether a transition of one process is helpful depends on the states of all its neighbors Substituted in the standard proof rules for progress properties these assertions lead to premises that do not conform to the required V4 form and therefore cannot be validated using the small model theorem To handle the first extension we prove in Subsection 6 1 a modest model theorem The modest model theorem es tablishes that V3 premises containing i 1 subexpres sions can be validated on relatively small models The size of the models however is larger when compared to the small model theorem of PRZOI To handle the second extension we introduce a novel proof rule PRERANK The main difficulty with helpful assertions of the form h i Vj H i 1 is in the premise that claims that every pending state has some helpful transition enabled on it D3 of rule DISTRANK in Sec tion 2 Identifying such a helpful transition is the ha
21. variables by the joint interpretation s Since N gt No there exist some i lt k such that ui41 u gt L 1 We construct a state s in an instan tiation S N lt Ni such that s v The process is repeated until we obtain an instantiation that satis fies i where the u s are at most L 1 apart from one another Since uj 4 u gt L 1 there exist two pairs of adja cent indices between u and u 1 that agree on their lo cal array values i e there exist some m and n such that uj lt m lt n lt n 1 lt ui and for every boolean array a index bool we have a m afn and a m 1 a n 1 Intuitively removing all processes m 1 n does not impact any of the other processes whose indices are in U since the array values of their immediate neigh bors remain the same In particular since m 1 and n4 1 are identical processes m and n 1 maintain the same neighbors after the removal Once the processes are re moved the remaining processes are renumbered Formally let N N n m and define the func tion 1 N1 1 N such that g i i for i m and g t i n m for i gt n 1 It is easy to see that g is injective and onto hence g is well defined Consider the state s of system S N such that for every array a index bool we have s a i s a g i i e the value of a in state s at index i is the value of a in state s at index g
22. 3 is the critical section and location 4 is the exit section Note that y the ticket ar ray is of type index data and the program location array which we denote by 7 is of type index bool in N natural where N gt 1 local y array 1 N of 0 where y 0 loop forever do 0 NonCritical 1 y maximal value to y i while preserving order of elements viz await V i n gt vli Critical yli 0 Fig 2 3 Program BAKERY Note also that the ticket assignment statement at 1 is non deterministic and may modify the values of all tick ets Fig A 1 in Appendix A 1 describes the BFTS corre sponding to program BAKERY Let be an assertion over V and R be an assertion over VUV which can be viewed as a transition relation We denote by oo R the assertion characterizing all states which are R successors of a states We denote by ao R the states reachable by an R path of length zero or more from an o state In a symmetric way we denote by Roa the assertion characterizing all the states which are R predecessors of a states 2 9 The Small Model Theorem Let o Vi3j R i j be an V3 formula where R i j is a restricted assertion which refers to the state variables of a parameterized BFTS S N in addition to the quantified index variables i and j We show that if there exists some model that does not satisfy this assertion then there exists a model smaller than a certai
23. ERY N for every N Indeed it is straightforward to see that in order to conclude that 2 is helpful one has to consider help ful assertions of the form Vj i j In Section 7 we show how to obtain helpful assertions that relate to all processes and how to change the proof rule for such a case We can still use the simple proof rule in order to au tomatically verify algorithm BAKERY N However this requires the introduction of an auxiliary variable minid into the system which is the index of the process which holds the ticket with minimal value This is explained in detail in Section 5 We emphasize that the generation of all assertions is completely invisible so is the checking of the premises on the instantiated model While the user may see the assertions there is no need for the user to comprehend them In fact being generated using BDD techniques they are often incomprehensible 4 Cases Requiring an Existential Invariant In some cases V assertions i e assertions of the form Vi u i are insufficient for capturing all the relevant fea tures of the constructs p and pend and we need to consider assertions of the form Vi u i 3j e j In this section we describe how to obtain constructs that are boolean combinations of V assertions illustrating the procedure and its applications on program CHANNEL RING presented in Fig 4 1 In this program the location of the token is identified by the index 4 such that chan i
24. In PRZ01 APR 01 we obtain using project amp generalize candidate induc tive assertions for the set of reachable states that are V formulae checking their inductiveness required check ing validity of V3 formulae which can be accomplished using BDD techniques 2 4 Removing Compassion The proof rule we are employing to prove progress prop erties assumes an incompassionate system system with no compassionate transitions As outlined in KPP03 every FTS can be converted into an incompassionate FTS S V O 1 J where V V U nvr boolean 9 0 TZ U Amu Uf TET C rec 4 U Ufo TE JNC TEC where f1 f2 T T are defined by fi r T A ND T pres Nvr V Mor tam Nor nvr This transformation adds to the system variables for each compassionate transition r a new boolean variable nur The intended role of nur is non deterministically to identify a point in the computation beyond which 7 is never enabled The new transition relation includes two types of transitions For each original non compassionate transition a transition f 7 that behaves like 7 while preserving the values of all nur variables For each orig inal compassionate transition 7 C J contains a tran sition fo r that either takes and preserves all nvr variables or changes nur from F to T and preserves all other variables Intuitively as long as nur F f 7 is enabled a
25. Software Tools for Technology Transfer manuscript No will be inserted by the editor Liveness with Invisible Ranking Yi Fang Nir Piterman Amir Pnueli Lenore Zuck New York University New York e mail yifang amir cs nyu edu Weizmann Institute Rehovot Israel e mail firstname lastname weizmann ac il 3 University of Illinois at Chicago e mail lenore cs uic edu Received date Revised version date Abstract The method of Invisible Invariants was de veloped originally in order to verify safety properties of parameterized systems in a fully automatic manner The method is based on 1 a project amp generalize heuristic to generate auxiliary constructs for parameterized systems and 2 a small model theorem implying that it is suffi cient to check the validity of logical assertions of certain syntactic form on small instantiations of a parameterized system The approach can be generalized to any de ductive proof rule that 1 requires auxiliary constructs that can be generated by project generalize and 2 the premises resulting when using the constructs are of the form covered by the small model theorem The method of invisible ranking presented here gen eralizes the approach to liveness properties of parameter ized systems Starting with a proof rule and cases where the method can be applied almost as is the paper pro gresses to develop deductive proof rules for liveness and extend the small model th
26. V3 Lui 0 A li y vli 0 pend p4 at z 1 1 2 0 2 at_la z 69 2 9 7 heli 4 minid z A minid J 310 at_fa z A at_3 j 410 12 1 7 L Forj z Forj z 1 Selia 2 at 21 2 2 C z 3 2 3 0 C z 5 2 3 410 2 j 2 3 4 where z 7 A 1 2 at a z A ylz gt y j A at CA j Pre order relation for non minid version Let a j 2 ylz lt vU 6 ali 2 v i lt yf and y L j L y z lt y j The pre order is described in Fig A 3 A 2 Program TOKEN RING Symbolic Assertions aj MM hg 41 1 at i i tloc i Symbolic Ranking 66 1 0 Of L 11 0 dg i at 1 A 1 lt tloc i at_loif i V tloc i Of i at 4 1 A 1 lt tloc i at for lloc at i i1 i 611 1 lt tloc i o 4 i V tloc A ly 5 i A 8 Program DINE BFTS See Fig A 2 Abstract Pending Sets y N gt lt 2 p gt 1o N lt 2 Yi Fang et al Liveness with Invisible Ranking 19 y J f nri nura array 1 N of bool Symbolic Ranking and Helpful Sets For every j z T array 1 of 0 4 1 N 1 O Vi o ue h j F 19 E d h m j 1 2 2 1 io olim J m f ns la
27. andidate for an existential in variant In the table below we list the results of these computations for the case that reach equals precisely the conjunction AW w i A V EG j and the appli w 1 1 1 cation of project amp generalize to reach yields precisely u t reach l i w i Results when reach a Apu A ag w k E az w k gt e k fe w i Vje j Note that while we did not succeeded in precisely isolat ing e k we computed instead the implication w k e k However the conjunction Vi w i 3k w k gt e k is logically equivalent to the conjunction Vi w i A 3k e k This technique of obtaining an existential conjunct to an auxiliary assertion can be used for other auxiliary constructs Yi Fang et al Liveness with Invisible Ranking 11 in N local y natural where N gt 1 array 1 of 0 where y 0 minid natural where minid 1 loop forever do 0 NonCritical 1 y maximal value to yi while preserving order await Vj bee vU gt vli 3 Critical 4 y i 0 maintain V 0 v 0 lt y minid lt y 7 Fig 5 1 Program BAKERY with auxiliary variable minid 4 2 Verifying Progress of CHANNEL RING Applying the extended project amp generalize to CHANNEL RING we obtain for the set of reachable states the aux iliary construct at_lo 1 V chan i QA Biol ehani chan k A 3j chan j Usi
28. anking in N natural where N gt 1 local y array 1 N of bool where y 1 loop forever do NonCritical request y i request y i 1 Critical release yfi y i 1 N 1 Pli i loop forever do NonCritical request 1 request y N Critical release y 1 y N Ae Ne Fig 6 1 Program DINE Solution to the Dining Philosophers Problem Thus the proof of inductiveness of y as well as all premises of DISTRANK are now of the form covered by the modest model theorem We now compute the size of the instantiation needed Premises D1 D3 and D7 relate only to unprimed copies of the variables Other premises relate to both unprimed and primed copies of the variables When we use the modest model theorem as is the resulting figures are L 40 1600 5 possible locations one fork two nor variables all counted as current and next L 4 1 2 5 106 which results in a bound of about 107 processes In order to get a reasonable figure we use the following reductions e We syntactically analyze all the resulting assertions and find that only variables in V3 are referenced by both and o1 Variables in W are referenced only by 1 Thus we have to search only for two identical processes and not for two pairs of adjacent processes e The transition p is on the left hand side of the impli cation in all the premises that include primed vari ables D2 D4 D5 and D6 This im
29. by the ac tions of helpful transitions in the system In a para meterized system the set of transitions has the struc ture T N 0 m andi 1 N for some fixed m Typically 0 m enumerates the locations within each process For example in program TOKEN RING T N 0 2 and i 1 N where each transition r i is associated with location 0 2 within process i 1 N Requiring that 7 i is just guarantees that it is taken or disabled infinitely often thus that re i is not continuously enabled and never taken beyond some point Assertion y is an invariant assertion characterizing all the reachable states Assertion pend characterizes the states which can be reached from a reachable q state by an r free path For each transition T assertion h characterizes the states at which 7 is helpful These are the states s that have a r successor s and the transition from s to s leads to a progress towards the goal This progress is observed by immediately reaching the goal or a decrease in the ranking function as stated in premises D5 and D6 The ranking functions measure progress towards the goal The disabling of 7 is often 8 Yi Fang et al Liveness with Invisible Ranking caused by 7 being taken D6 but may also be caused by some condition turning false D5 We require decrease in ranking in both cases Premise D1 guarantees that any reachable q state satisfi
30. chs and P Raymond Au tomatic verification of parameterized linear net works of processes In 24th ACM Symposium on Principles of Programming Languages POPL 97 Paris 1997 K L McMillan Verification of an implementa tion of Tomasulo s algorithm by compositional model checking In A J Hu and M Y Vardi edi tors A J Hu and M Y Vardi editors Proc 10 Intl Conference on Computer Aided Verification CAV 98 volume 1427 of Lect Notes in Comp Sci Springer Verlag pages 110 121 1998 Z Manna and A Pnueli Completing the tem poral picture Theor Comp Sci 83 1 97 130 1991 Z Manna and A Pnueli Temporal Verification of Reactive Systems Safety Springer Verlag New York 1995 S Owre N Shankar and J M Rushby User guide for the PVS specification and verifica tion system draft Technical report Comp Sci Laboratory SRI International Menlo Park CA 1993 GS97 GZ98 JN00 KPP03 LHR97 McM98 MP91 OSR93 18 Yi Fang et al Liveness with Invisible Ranking ZOEE array 1 N of 0 p array 1 N of 0 4 O Vi n i 20 y i 20 To i Vjz i mpi OAn i 0 1 A pres n 5 yli 7 Tili Vj k i nfi 1 Arli 2A y i lt vi ON yj lt ylk y pres n 5 rli 2 ylj 0 V yl gt m i 3 pres U yli 1 n i 3 i 4 pres n j yr vij T i 4 i 0 wv i 0 M
31. ded by two boolean arrays hence we are justified in referring to it here and in future examples as a index bool array Strictly speaking the transition relation as presented above does not conform to the definition of a Boolean assertion since it contains the atomic formula tlo iG 1 However this can be rectified by a two stage reduction First we replace tlo i 1 by i lt N A tlo i 1 V i N 1 Then we replace the formula Vj i tloc i 1 by T t i1 Vj 655 ja 11 tloc i1 which guarantees that 7 i 1 Note that transition 1 is not listed as a just tran sition This allows process to remain forever in its non critical location 0 as long as it diligently transfers any incoming token to its right neighbor Also note that this system has an empty set of compassion transitions which we omitted from the presentation in Fig 2 2 Example 2 2 The Bakery Algorithm Consider program BAKERY in Fig 2 3 which is a vari ant of Lamport s original Bakery Algorithm that offers a solution to the mutual exclusion problem for any N processes In this version of the algorithm location 0 constitutes the non critical section which a process may nondeter ministically exit to the trying section at location 1 Lo cation 1 is the ticket assignment location Location 2 is the waiting phase where a process waits until it holds the minimal ticket Location
32. e additional important advantage that the user never sees the automatically generated auxiliary assertion q This assertion is produced as part of the procedure and is im mediately consumed in order to validate the premises of the rule Being generated by symbolic BDD techniques the representation of the auxiliary assertions is often extremely unreadable and non intuitive and it usually does not contribute to a better understanding of the pro gram or its proof Because the user never gets to see it we refer to this method as the method of invisible in variants As shown in PRZ01 APRt01 embedding a Vi q i candidate inductive invariant in INV results in premises that fall under the small model theorem In this paper we extend the method of invisible invariants to apply to proofs of the second most important class of properties the class of response properties Response properties are liveness properties that can be specified by the tempo ral formula q r also written as g Qr and guarantee that every q state is eventually followed by an r state To handle response properties we consider a cer tain variant of rule WELL MP91 which establishes the validity of response properties under the assumption of justice weak fairness As is well known to users of this and similar rules such a proof requires the generation of two kinds of auxiliary constructs helpful assertions hi that characterize for transition 7 th
33. e states from which the transition is helpful in promoting progress to wards the goal r and ranking functions which measure progress towards the goal In order to apply project amp generalize to the automatic generation of the ranking functions we propose a variant of rule WELL In this variant rule called DISTRANK we associate with each potentially helpful transition 7 an individual ranking function X 0 c mapping states to integers in a small range 0 c for some fixed small constant c The global ranking function can be obtained by forming the multi set In most of the examples we consider it suffices to take c 1 which allows us to view each as an assertion and generate it automatically using project amp generalize If when applying rule DISTRANK the auxiliary con structs h and have no quantifiers all the resulting premises are V3 premises and the small model theorem can be used One of the constructs required to be quan tifier free are the helpful assertions that characterize the set of states from which a given transition is helpful Many simple protocols have helpful assertions that are quantifier free or with the addition of some auxiliary variables can be transformed into protocols that have quantifier free helpful assertions Some protocols how ever cannot be proven with such restricted assertions To deal with such protocols we extend the method of invisible ranking in
34. each Oo 0p the assertion characteriz ing all states reachable within S No Compute y 1 reach 3 i by projecting reach on index 3 and then generalizing 3 to 7 That is maintaining only vari ables pertaining to process 3 and then replacing every reference to index 3 by a reference to index i For example in TOKEN RING 6 6 Po N atto i V tloc j j 1 where at o 1 j is an abbreviation for z j 0 1 The projection of y on j 3 yields at_o 1 3 V tloc 3 The generalization of 3 to yields 0 1 at Co 1 i V tloc i The assertion y is Vi p4 1 Note that when we generalize we should generalize not only the values of the variables local to P 3 but also the case that the global variable such as tloc has the value 3 The choice of 3 as the generic value is arbitrary Any other value would do as well but we prefer indices different from 1 N In this part we computed y i as the generalization of 3 into i in gc which is denoted by 1 yo 3 gt i In later parts we may need to generalize two indices such as a ac 2 6 4 j where a and a are a concrete and abstract versions of some assertion a The way we compute such abstractions over the state variables tloc and of system TOKEN RING is given by UR ert tloc a tloc m i j 3tloc m map 2 i 4 j 1 where rli Bl nj lloc i lt tloc 2 map 2
35. ene i v pres n j 7 Li Vi Aa Vj Aa Tali Vj d Tia Vj 72 i Ta i Ta i via 1 N Fig A 1 BFTS for Program BAKERY PRZ01 A Pnueli S Ruah and L Zuck Automatic de ductive verification with invisible invariants In Proc Intl Conference on Tools and Algo rithms for the Construction and Analysis of Sys tems TACAS 01 volume 2031 of Lect Notes in Comp Sci Springer Verlag pages 82 97 2001 A Pnueli J Xu and L Zuck Liveness with 0 1 oo counter abstraction 2002 Sha00 E Shahar The TLV Manual 2000 http www wisdom weizmann ac il verify tlv B K Szymanski A simple solution to Lam port s concurrent programming problem with lin ear wait In Proc 1988 International Conference on Supercomputing Systems pages 621 626 St Malo France 1988 M Y Vardi Verification of concurrent programs the automata theoretic framework Annals of Pure and Applied Logic 51 79 98 1991 L Zuck and A Pnueli Model checking and ab straction to the aid of parameterized systems Computer Languages Systems and Structures 2004 to appear PXZ02 Szy88 Var91 ZP04 A BFTS s and Auxiliary Constructs A 1 Program BAKERY BFTS See Fig A 1 Auxiliary Constructs The auxiliary constructs for Pro gram BAKERY with minid are o i i gt yli 0 guis paid 4 minid Zi v yj gt yli yl 0 v
36. eneration and illustrate it on the case of program TOKEN RING In TOKEN RING the progress property we wish to check is z 21 O2alz 2 2 For simplicity as all processes are symmetric we choose z thus we check ml 1 gt 2 This property claims that every state in which process is at location 1 is eventually followed by a state in which process 1 is at location 2 The construction uses the instantiation S No for the cutoff value No required in Theorem 2 1 For TOKEN RING as explained in Subsection 3 3 No 6 We de note by O and p the initial condition and transition relation for S No The construction begins by comput ing the concrete auxiliary constructs for S No denoted by Yo pend We then compute the concrete hf j s and j s Next we apply project amp generalize to derive the symbolic abstract versions of these constructs v pend hg J s and j s Since we focus on process 1 we would expect the constructs to have the symbolic forms q Vi y i and pend pend Viz pend i For each k 0 m we need to compute A 1 1 and the generic i 67 i that should be symbolic in 7 and apply for all i 1 i lt N All generic constructs are allowed to refer to the global variables and to the variables local to P 1 and Pli 3 2 1 Computing Concrete and Abstract y All concrete assertions are computed on S No We set Yo to be r
37. eorem to cover many intricate families of parameterized systems 1 Introduction Uniform verification of parameterized systems is one of the most challenging problems in verification Given a parameterized system S N PLN and a property p uniform verification attempts to verify that S N satisfies p for every N gt 1 One of the most pow erful approaches to verification that is not restricted to finite state systems is deductive verification This ap proach is based on a set of proof rules in which the user This research was supported in part by NSF grant CCR 0205571 ONR grant N000140310916 the John von Neumann Min erva Center for Verification of Reactive Systems the European Community IST project Advance and the Israel Science Foun dation grant 106 02 1 has to establish the validity of a list of premises in order to validate a given temporal property of the system The two tasks that the user has to perform are 1 Provide some auxiliary constructs that appear in the premises of the rule 2 Use the auxiliary constructs to establish the logical validity of the premises When performing manual deductive verification the first task is usually the more difficult requiring ingenuity expertise and a good understanding of the behavior of the program and the techniques for formalizing these insights The second task is often performed using the orem provers such as PVS OSR93 or step BBC 95 which
38. es r or pend Premise D2 guarantees that any suc cessor of a pend state also satisfies r or pend Premise D3 guarantees that any pend state has at least one transi tion which is helpful in this state Premise D4 guarantees that ranking never increases on transitions between two pend states Note that due to D2 every p successor of a pend state that has not reached the goal is also a pend state Premise D5 guarantees that taking a step from an h state leads into a state which either already sat isfies the goal r or causes the rank 6 to decrease or is again an h state Premise D6 guarantees that taking a T transition from an h state either reaches the goal r or decreases the rank Premise D7 guarantees that in all h states T is enabled Together premises D5 D6 and D7 imply that the computation cannot stay in h for ever otherwise justice w r t 7 is violated Therefore the computation must eventually decrease Since there are only finitely many 6 and until the goal is reached they monotonically decrease we can conclude that eventually an r state is reached 3 8 Automatic Generation of the Auxiliary Constructs We now proceed to show how the auxiliary constructs necessary for the application of rule DISTRANK can be automatically generated Recall that we have to con struct a symbolic version of each construct so that the rule can be applied to a generic N We consider each auxiliary construct provide a method for its g
39. et in g as not to violate J Since T is enabled infinitely often it is enabled after nvr is increased and c is not Err free We can therefore conclude that for every q and r SEq Or if S E q oEr gt rv Err Which allows us to assume that all BFTSs we consider here have an empty compassion set a parameterized system with transitions 7 N where p Vez T set of states X N just transitions 7 C T N invariant assertion assertions q r pend and h r J and ranking functions 6 0 1 re J Dl r V pend D2 pend p EN D3 pend gt D4 pend A p For every T J D5 hr p D6 he AT DT h Fig 3 1 The liveness rule DISTRANK 3 The Method of Invisible Ranking In this section we present a new proof rule that allows in some cases to obtain an automatic verification of live ness properties for a BFTS of any size We first describe the new proof rule and then present methods for the au tomatic generation of the auxiliary constructs required by the rule using TOKEN RING as an ongoing example 3 1 A Distributed Ranking Proof Rule In Fig 3 1 we present proof rule DISTRANK short for Distributed RANKing for verifying response properties for BFTSs whose only fair transitions are just The rule is configured to deal directly with parameterized sys tems As in other rules for verifying response proper ties MP91 e g progress is accomplished
40. generation of invariants in the form of boolean combinations of universal assertions This is demonstrated on a different version of the token ring protocol In Section 5 we study a version of the Bakery algorithm that seems beyond the scope of the invisi ble ranking method and show how enhancing a proto col with some auxiliary variables can make it a suitable candidate for the method The method studied in Sections 3 5 is adequate for cases where the set of reachable states can be satisfac torily over approximated by boolean combinations of V assertions and the helpful assertions as well as individ ual ranking functions 6 can be represented by quantifier free assertions Not all examples can be handled by as sertions which depend on a single parameter In Sec tion 6 we describe the modest model theorem which al lows handling of i 1 expressions within assertions and demonstrate these techniques on the Dining Philosopher problem In Section 7 we present the PRERANK proof rule that uses pre order among transitions discuss how to automatically obtain the pre order and demonstrate the technique on the Bakery algorithm Finally we dis cuss the advantages of combining several pre order re lations and demonstrate it on Szymanski s protocol for mutual exclusion 52 88 All our examples have been run on TLV Sha00 The interested reader may find the code proof files and out put of all our examples in cs nyu edu acsys Tlv
41. index gt bool variables Primed Occurrences When a variable appears both unprimed and primed in R both occurrences add to the count unless equal This is in general the case with the transition relation p that appears on the l h s of several implicants in our proof rules While it may seem that each additional variable that can be modified dou bles the count only a single step is to be considered at a time which is further restricted by reach reach ap pears explicitly in all the implicants moreover it can always be added since it is shown to be an invariant Yi Fang et al Liveness with Invisible Ranking 13 Hence in practice the bound can often be reduced as to be manageable Restricted Use of Assume that for each Vy variable under a operator all occurrences of the operator are of the same kind only amp or O for each variable Then when reducing a large model into a smaller one instead of finding two processes at the endpoint of a chain that agree on values of both their neighbors it suffices to find a pair that agrees on one neighbor which implies a chain of length L Consequently in this case the cut off value is No K 1 K Further analysis reveals that if only one operator or is applied to V3 variables then the bound can be further reduced to No K 1 L 1 K Restricting to Observable States Suppose that a process only has a partial view of its neighbor i e
42. ion The range of these ranking functions is usu ally 0 1 There are cases where a single transition must be helpful more than once before other helpful transi tions can be taken In such cases the restricted range of 0 1 i e the helpful transition was or was not taken is not sufficient We would have to consider ranking func tions with a larger range set In general we believe that it is best to use the smallest range possible for the rank ing functions The main burden in using our method is in devising the method in which we compute the explicit ranking functions and in deciding how to generalize these explicit assertions Thus having a larger range for the ranking functions would make the method harder to use and is inadvisable A key feature of our method is generalizing a concrete set of states into a universal assertion In the paper we explain briefly how to obtain existential auxiliary asser tions in the case that our approximation of the concrete set is too abstract This process can be iterated as fol lows When the assertion we have is too abstract we can add an existential conjunct that tightens the abstraction When the assertion does not capture the entire concrete set we can generalize the difference and add a univer sal disjunct Thus we can get assertions of the general form VA3 V V 3 Note that the quanti fiers are not nested hence using these assertions we can Yi Fang et al Livenes
43. ire the user to pro vide auxiliary constructs and thus do not provide for fully automatic verification of parameterized systems Most of the mentioned methods only deal with safety properties Among the methods dealing with liveness properties we mention CS02 which handles termina tion of sequential programs network invariants LHR97 and counter abstraction P X02 2 Preliminaries In this section we present our computational model the small model theorem and the procedure that allows to remove compassion strong fairness We assume that the reader is familiar with LTL CTL first order logic and fixpoint operators 2 1 Fair Transition Systems As our computational model we take a fair transition system FTS MP95 S V O 7 7 C with e V u1 Un A finite set of typed system variables A state s of the system provides a type consistent interpretation of the system variables V assigning to each variable v V a value s v in its domain Let X denote the set of all states over V An assertion over V is a first order formula over V A state s satisfies an assertion y denoted s H y if evaluates to T by assigning to every variable v appearing in y We say that s is a q state if s E v 4 Yi Fang et al Liveness with Invisible Ranking e O The initial condition An assertion characteriz ing the initial states A state is called initial if it is a O state e 7 A finite set of
44. j await Vj at a4 j await Vj j lt i at oa 2 j Critical Fig 8 1 Program Szymanski consider 1 lt 7 j for every 41 49 1 4 and i z zji jzszzi jzzfor 64G i z j The results for 1 lt Tz j for i Z z that are not trivially T are described in Appendix A 1 Using the above pre order we succeeded in validat ing Premises R1 R9 of PRERANK thus establishing the liveness property of program BAKERY 8 Multiple Pre Order Relations In the previous section we described how to compute the pre order relation Formula 7 1 is one alternative of computing the pre order We can view rule DISTRANK as a special case of rule PRERANK with a trivial pre order defined by s 7 if s H V r1 T2 where 8 1 ha V hn Obviously other definitions are also possible In fact by allowing different schemes of computing pre order on different states the rule PRERANK can be applied to a wider range of protocols In this section we demonstrate this idea on a version of Szymanski s mutual exclusion protocol described in Fig 8 1 The progress property we would ideally like to ver ify is 1 O a z 7 This property however is beyond the scope of the methods and rules described here since it requires some just transition to be helpful twice It is not difficult but rather tedious to extend our technique for generating ranking so to dea
45. l with cases where transitions may be helpful up to k times for any bounded k We bypass this difficulty here by restrict ing to a smaller progress property to which the proof applies namely to the progress property n z 21 Vi afi lt 4 gt O alz 7 8 2 An inspection of the protocol reveals that is the only transition whose enabling condition is of the form Vj p i j which is an obvious candidate for pre ordering of the type we used in Section 7 The other 16 Yi Fang et al Liveness with Invisible Ranking a parameterized system with a transition 7 7 N set of states X N just transitions J C T N invariant assertion assertions q r pend and h r J ranking functions 6 0 1 T E J and a pre order 4 X 27 7 R1 Q R2 pend p R3 pend p For every T J RA R5 R6 RT R8 For every 71 72 J R9 pend m R10 pend r V pend r V pend Neg r 207 hz r V r V n r AST hi V 6 gt 6 r gt TST MAT q gt Or Fig 7 1 The liveness rule PRERANK transitions all have enabling conditions of the form p i A Vj q 3 or simpler that can be easily handled by the trivial pre order which we implicitly use when apply ing DISTRANK Consequently we partition the concrete pending states into pend Ji Voge En re i and pend pend pend The concrete pre order is
46. les that appear existentially quantified in v Let F be the set of index constants including 1 and variables which appear free in v Note that state s provides an interpretation for all the variables in F and all the arrays which appear in s Similarly let Vy be the set of index variables that appear universally quantified in w i e the j variables The fact that y Jivj oR ij is satisfiable in s means that there exists an assignment a which inter prets all variables of by values in the domain 1 N1 such that s x where x Vj 2R i j and s a is the joint interpretation which interprets all system vari ables according to state s and all V3 variables according to the assignment o Let U lt u2 lt lt ux be a sorted list of values assigned to the V3 U F variables by a and s Obviously k No Let f U 1 k be the bijection such that f u i iff u ui Similarly let D 0 d lt d lt d2 lt lt dr be a sorted list of all the values assigned by s to the elements b u for the data array b and i 1 k We always include 0 in D even if it is not obtained as the value of some b u Obviously r k Let g D L r be the bijection such that g d j iff d dj We construct a state s of system S k and an assign ment Va 1 k such that s a x The state s is an interpretation defined as follows For each variable v F s interprets v as s
47. lier than 72 in some computations and 72 precedes 7 in oth ers we obtain both lt and 72 lt To abstract a formula A v h i W v h9 j we compute the asser tion A e h 2 W v h 3 over S No 2 and 3 being chosen arbitrarily to represent two generic indices and then generalize 2 to and 3 to j To abstract the nega tion of such a formula we first abstract the formula and then negate the result Therefore to abstract For mula 7 1 we abstract each A W formula separately and then take the disjunction of the first abstract asser tion with the negation of the second abstract assertion 7 1 7 2 Case Study Bakery Consider program BAKERY of Example 2 2 Fig 2 3 Suppose we want to verify z z 1 a z 3 We instantiate the system to No 3 and obtain the auxiliary assertions y pend the h s and s After ap plying project amp generalize we obtain for hefi two types of assertions One is for the case that i z and then as expected h2 z is the most interesting one having an V construct claiming that z s ticket is the minimal among ticket holders The other case is for j Z z and there we have a similar V construct for j s ticket min imality for 2 3 4 For the pre order one must in N natural where N gt 1 loop forever do NonCritical await Vj at 0 1 2 4 7 skip If 3j at 2 j then go to l4 else go to Is await Jj at s 6 7
48. n bound that does not satisfy it It follows that in order to check the validity of this formula it is enough to check all models up to the given bound The proof follows by contract ing a model that does not satisfy y to a smaller model that does not satisfy y In order to decrease the size of the model we consider the existentially quantified vari ables in the negation of o These variables refer to some processes in the model that does not satisfy y We keep the processes refered to by these variables and throw away the rest For simplicity we assume that the only data vari able constant that may appear in R is the data constant 0 Let No be the number of universally quantified vari ables free index variables and index constants appear ing in R The following theorem stated first in PRZOI and extended in APR 01 provides the basis for the automatic validation of the premises in the proof rules Theorem 2 1 Small model property Let p be an VA formula as above Then is valid over 6 Yi Fang et al Liveness with Invisible Ranking S N for every N gt 2 iff p is valid over S N for every N No For completeness of presentation we include the proof Proof We denote by the formula divj R i j which is the negation of y Assume v is satisfiable in state s of a system for N gt No We show that it is satisfiable in a state s of a system S N for some N No Let V3 be the set of index variab
49. nd to comply with the justice requirement associated with f2 r either 7 is taken infinitely often or nur eventually set to T Once nur is set to T T is not expected to be enabled and therefore taken ever again Let Err denote the assertion V co En r nuvr describing states where both 7 is enabled and nur holds which indicates that the prediction that r will never be 1 The proof in KPP03 is an adaptation of the proofs in Cho74 Var91 to the case of transition systems Yi Fang et al Liveness with Invisible Ranking 7 enabled is premature For a computation c of S de note by the sequence obtained from c by project ing away the nur variables The relation between S and its compassion free version is stated by the following claim Claim Let o be an infinite sequence of S states Then is an S computation iff there exists an Err free com putation co of S such that cjl y c Proof In one direction let o s s1 be a compu tation of S We will show how to define the values of nur at each position of the computation such the re sulting sequence of S states 50 51 15 an Err free computation of S The intention is to guarantee that transition 7 C is continuously disabled beyond some position j of c iff nur is set to T at some position beyond j For sim plicity assume that the compassionate transitions are T 71 Tk and that we may refer to nvr simply as nvri
50. nford Temporal Prover User s Manual Technical Report STAN CS TR 95 1562 Computer Science Department Stan ford University November 1995 E M Clarke O Grumberg and S Jha Verifying parametrized networks using abstraction and reg ular languages In 6th International Conference on Concurrency Theory CONCUR92 volume 962 of Lect Notes in Comp Sci pages 395 407 Philadelphia PA August 1995 Springer Verlag Y Choueka Theories of automata on w tapes A simplified approach J Comp Systems Sci 8 117 141 1974 M Colon and H Sipma Practical methods for proving program termination In E Brinksma and K G Larsen editors Proc 14 Intl Confer ence on Computer Aided Verification CAV 02 volume 2404 of Lect Notes in Comp Sci Springer Verlag pages 442 454 2002 E A Emerson and V Kahlon Reducing model checking of the many to the few In 17th In ternational Conference on Automated Deduction CADE 17 pages 236 255 2000 E A Emerson and K S Namjoshi Reasoning about rings In Proc 22nd ACM Conf on Prin ciples of Programming Languages POPL 95 San Francisco 1995 CGJ95 Cho74 CS02 EK00 EN95 FPPZ04a Y Fang N Piterman A Pnueli and L Zuck Liveness with incomprehensible ranking In Proc 10 Intl Conference on Tools and Algo rithms for the Construction and Analysis of Sys tems TACAS 04 volume 2988 of Lect Notes in Comp Sci Springer Verlag pages 452 496 A
51. ng this extended form of an invariant for both o and pend we can complete the proof of program CHANNEL RING using the methods of Section 3 Applying the method of invisible ranking with the new addition to program CHANNEL RING and the re sponse property at 1 at 2 1 we obtain for example pend 1 1 y and for i gt 1 h i at 11 at lmli chan j Thus Premise D3 be comes at amp 1 Vitk at_lo 1 V chan i 5 chan i A chan k 3j chan j at 1 3j chan j which is obviously valid and has the V3 form 5 The Bakery Algorithm As another example of the application of the invisible ranking method we consider the modified version of pro gram BAKERY presented in Fig 5 1 As previously explained in order to be able to use the rule in its current form we introduce the variable minid The variable minid is expected to hold the index of a process whose y value is minimal among all the posi tive y values The maintain construct implies that this variable is updated if necessary whenever some y vari ables change their values Already in PRZO1 we pointed out that in some cases it is necessary to add auxiliary variables in order to find inductive assertions with fewer indices This version of BAKERY illustrates the case that such auxiliary variables may also be needed in the case of the invisible ranking method The property we wish to verify for this
52. now defined for pend states by V rei re 2 0 6 Teli lt ve 16 T 6 F otherwise and for pend states by Te HW C C 6 Tet lt 1 T UA6 F otherwise where W is defined in Formula 8 1 and is defined Formula 7 1 These definitions allow us to use project amp generalize on the concrete pre order as described in Section 7 and successfully prove Formula 8 2 for program Szymanski 9 Discussion We have presented a method for automatically verify ing liveness properties of parameterized systems The method is based on automatic computation of the as sertions needed by a deductive rule according to the analysis of a small instance of the problem Then us ing a small model theorem the verification conditions of the deductive rule are discharged using BDD techniques on a sometimes not so small instance of the parame terized system Being able to discharge the verification conditions on a finite model has the additional advan tage that the user never gets to see the assertions which is why we termed the method invisible constructs Deductive proofs for liveness require the identifica tion of helpful transitions and in addition a ranking function that measures the progress towards the goal The deductive proof rule we are using is similar In order to facilitate the generation of the ranking function we partition it and include one ranking function per helpful transit
53. on for the general multi type case is straightforward Let N be the system s parameter We allow the following data types 1 bool the set of Boolean and finite range scalars 2 index a scalar data type that includes integers in the range 1 N 3 data a scalar data type that includes integers in the range 0 N and 4 Any number of arrays of the type index bool We refer to these arrays as Boolean arrays 5 At most one array of the type b index gt data We refer to this array as the data array Atomic formulas may compare two variables of the same type E g if y and y are index variables and z is an index data array then y y and z y lt 2 y are both atomic formulas For z index data and y index we also allow the special atomic formula z y gt 0 We refer to quantifier free formulas obtained by boolean combinations of such atomic formulas as re stricted assertions As the initial condition O we allow assertions of the form Vi u i where u i is a restricted assertion As the transitions 7 7 we allow assertions of the form 7 i Vj v 1 j for a restricted assertion wv i j This results in total transition p Ji Vj v 1 j For simplicity we assume that all quantified and free vari ables are of type index Example 2 1 The Token Ring Algorithm Consider program TOKEN RING in Fig 2 1 which is a mutual exclusion algorithm for any N processes In this versi
54. on of the algorithm the global variable tloc represents the index of the process currently holding the token Location 0 constitutes the non critical section which may non deterministically exit to the trying sec tion at location 1 While being in the non critical sec tion a process guarantees to move the token to its right neighbor whenever it receives it This is done by incre menting tloc by 1 modulo N At the trying section a Yi Fang et al Liveness with Invisible Ranking 5 V tloc 1 array 1 N of 0 2 O Vi r i 0 rali Vj i O tloc i tloc i y 1 Ar i 0 1 pres n j reli Vj Ai 0A tloc i m i 1 T pres n j tloc nG Vj Zi n i 1 tloc i Ar li 2 pres n j tloc Vj Ai m i 2 m i 0 A pres m j tloc Tia Vj pres n 5 tloc J 1 2 2 Tia ie 1 N Fig 2 2 BFTS for Program TOKEN RING process P i waits until it receives the token which is signaled by the condition tloc i Fig 2 2 describes the BFTS corresponding to program TOKEN RING where for a variable v V pres v de notes v and for a set U C V pres U denotes Avev Pres v When there is no danger of confusion we use pres a ay instead of pres ai a Note that tloc is an index variable while the program counter is an index bool array Actually m is of type index 0 2 but it can be enco
55. parameter ized system is i z gt 2 which implies accessibility for an arbitrary process 2 Having the auxiliary variable minid as part of the system variables we can proceed with the computation of the auxiliary constructs as explained in Section 3 Af ter some simplifications we can present the automat ically derived constructs as detailed in Appendix A 1 Using these derived auxiliary constructs we can verify the validity of the premises of rule DISTRANK over S 5 and conclude that for every value of N the property of accessibility holds 6 Protocols with p i i 1 Assertions In algorithms for ring architectures the auxiliary as sertions for a process often depend in addition to the process itself on its immediate neighbors Assume a ring of of size N For every j 1 N denote 761 j mod N 1 and j 6 1 j 2 mod N 1 As sertions of the type p i i 1 and p i i 1 can be replaced by equivalent less V3 assertions Unfortu nately this often results in formulae not covered by our small model theorem We bypass the problem by estab lishing a new small model theorem that allows proving validity of V3p i 1 assertions The size of the model in the new theorem is larger than the one indicated by the small model theorem which is why we refer to it as modest We state the modest model theorem and prove it in Subsection 6 1 describe how to fine tune the bounds in Subsection
56. plies that all pos sible counter examples to these premises satisfy p According to p all primed variables for every j i i 1 equal to their unprimed versions Thus if we treat 191 as another 2 element long chain of universally quantified variables we do not have to consider different values of the primed variables It follows that we can use L 40 for our search for duplicate entries As a result the value L above the maximal length of chain with no equivalent processes is 40 There are three free variables in the system 1 N and N 1 The reason we include N 1 is e g its explicit men tion in y Following the remarks on the modest model theorem since the three variables are consecutive and since with all universally quantified variables we use only i O 1 the size of the modest model we need to take is 40 u 1 u 4 where u is the number of universally quantified variables Since u lt 2 for each of D1 D7 it is 0 for D4 1 for D1 and 2 for D2 D3 and D5 it is sufficient to choose an instantiation of 128 4 In Table 6 1 we present the number of BDD nodes computed for each auxiliary construct and the time it By modifying project amp generalize to include only part of the variables of a process and not all variables this can be further reduced to 83 processes Construct nop nodes seconds D1 seconds D2 seconds D3 seconds D4 seconds D5 D6 seconds D7 seconds Table 6 1 Run time and
57. pril 2004 FPPZ04b Y Fang N Piterman A Pnueli and L Zuck Liveness with invisible ranking In Proc of the 5 conference on Verification Model Checking and Abstract Interpretation volume 2937 of Lect Notes in Comp Sci pages 223 238 Venice Italy January 2004 Springer Verlag V Gyuris and A P Sistla On the fly model checking under fairness that exploits symme try In O Grumberg editor Proc Proc 9f Intl Conference on Computer Aided Verification CAV 97 volume 1254 of Lect Notes in Comp Sci Springer Verlag 1997 E P Gribomont and G Zenner Automated ver ification of szymanski s algorithm In B Stef fen editor Proc 45 Intl Conference on Tools and Algorithms for the Construction and Analy sis of Systems TACAS 98 volume 1384 of Lect Notes in Comp Sci Springer Verlag pages 424 438 1998 B Jonsson and M Nilsson Transitive closures of regular relations for verifying infinite state sys tems In S Graf and M Schwartzbach editors Proc 6 Intl Conference on Tools and Algo rithms for the Construction and Analysis of Sys tems TACAS 00 volume 1785 of Lect Notes in Comp Sci Springer Verlag 2000 Y Kesten N Piterman and A Pnueli Bridg ing the gap between fair simulation and trace in clusion In W Hunt Jr and F Somenzi editors Proc 15 Intl Conference on Computer Aided Verification CAV 03 pages 381 392 Boulder CO USA August 2003 D Lesens N Halbwa
58. rd est step when applying the rule The new rule PRERANK Yi Fang et al Liveness with Invisible Ranking 3 introduced in Section 7 implements a new mechanism for selecting a helpful transition based on the establish ment of a pre order among transitions in each state The helpful transitions are identified as the transitions that are minimal according to this pre order We emphasize that the two extensions are part of the same method so that we can handle systems that both use 1 and require universal helpful assertions For simplicity of exposition we separate the extensions here Overview of Paper In Section 2 we present the gen eral computational model of FTS and the restrictions that enable the application of the invisible auxiliary con structs methods We also review the small model theo rem which enables automatic validation of the premises of the various proof rules In addition we outline a pro cedure that replaces compassion requirements by justice requirements which justifies our focus on proof rules that assume justice only Section 3 introduces the new DIsTRANK proof rule and explains how we automati cally generate ranking and helpful assertions for the pa rameterized case We refer to the new method as the method of invisible ranking We use a version of the to ken ring protocol for an ongoing example in this section Section 4 shows how to enhance the project amp generalize method to enable the
59. s We say that transition 7 7 is enabled at position k of o if 7 is enabled on sk We say that 7 is taken at position k if Sk 1 is a T successor of sg Note that several different transitions can be considered as taken at the same position We say that c is a computation of an FTS S if it satisfies the following requirements e Initiality 50 is initial i e 50 e Consecution For each 0 1 state is a p successor of se e Justice for every T J it is not the case that 7 is continuously enabled beyond some point j in c i e T is enabled at every position k gt j but not taken beyond j e Compassion for every C it is not the case that T is enabled at infinitely many positions in but taken at only finitely many positions Note that the idling transition being just implies that every computation contains infinitely many stuttering steps 2 2 Bounded Fair Transition Systems To allow the application of the invisible constructs meth ods we further restrict the systems we study leading in N natural where N gt 1 tloc 1 loop forever do if tloc i then tloc i 1 go to 0 1 await tloc Critical Fig 2 1 Program TOKEN RING to the model of bounded fair transition systems BFTS that is essentially the model of bounded discrete systems of APR 01 augmented with fairness For brevity we describe here a simplified two type model the extensi
60. s appearing in R Assume there are index bool arrays in S and let L 2 i e L is the number of different values that can be assigned to all variables indexed by a single process Define No K 1 7 1 K Theorem 6 1 Modest Model Theorem Let be an V3 formula as above Then q is valid over S N for every N gt 2 iff p is valid over S N for every N No Proof We denote by the formula divj R i j which is the negation of Assume wv is satisfiable in state s of system S N for Ni gt No We show that w is also satisfiable in a state s of a system S N for some N lt Np Let V3 be the set of index variables that appear exis tentially quantified in v Let F be the set of index con stants including 1 and N and variables which appear free in v Note that state s provides an interpretation for all the variables in F Observe that V3 U F K Sim ilarly let Vy be the set of index variables that appear universally quantified in v i e the j variables The fact that y SiVj R i j is satisfiable in s means that there exists an assignment a which inter prets all variables of by values in the domain 1 N1 such that s x where x Vj 2R i j and s a is the joint interpretation which interprets all system vari ables according to state s and all V3 variables according to the assignment a Let U 1 u1 lt lt uy be a sorted list of values assigned to the FUV3
61. s with Invisible Ranking 17 still employ the small model theorem We have studied examples where this iterative computation of the gener alization is necessary in order to get assertions that fulfill the requirements of the deductive rule This however is beyond the scope of this paper Finally we recall that the problem of uniform verifi cation of parameterized systems is undecidable thus we cannot hope that our method or other methods always succeed When the method does not work immediately it may help to obtain tighter abstractions It may help to increase the size of the small model on which we com pute the concrete assertions The corner stone of our method is a deductive rule so manual intervention of the user may help push a proof forward Sometimes un fortunately it would be best to try something completely different References AK86 K R Apt and D Kozen Limits for auto matic program verification of finite state concur rent systems Info Proc Lett 22 6 1986 APR O1 T Arons A Pnueli S Ruah J Xu and L Zuck Parameterized verification with auto matically computed inductive assertions In G Berry H Comon and A Finkel editors Proc 13 Intl Conference on Computer Aided Ver ification CAV 01 volume 2102 of Lect Notes in Comp Sci Springer Verlag pages 221 234 2001 BBC 95 N Bj rner LA Browne E Chang M Col n A Kapur Z Manna H B Sipma and T E Uribe STeP The Sta
62. v f s v That is w iff s v i For every boolean array a index bool we have s a s a u i e the value of in state s equals the value of a u in state s For the data ar ray b index gt data we take s b i g s b u for each i 1 k That is s b i j iff s b u dj Next we define the interpretation a as follows For each vari able v V3 a interprets v as a v f a v That is alu u iff ov 1 We proceed to show that s a H x To do so consider an arbitrary assignment j assigning to each variable v j a value 6 v 1 k We will show that s o 8 SR 1 j As we show this for an arbitrary assignment it follows that s o Vj R i 1 That is s o E x Consider the assignment interpreting each v j as u iff i It follows that 8 interprets each vari able v j by a value in 1 N1 Since s a E x it follows that s a 3 E R i j By induction on the structure of the formula R i j we can show that every sub formula y R i j evaluates to T under the joint interpretation s a 3 iff y evaluates to T under the in terpretation s a We conclude that s a H x which leads to the result that is satisfied in the state s of system S k The small model theorem allows to check validity of V assertions on small models

Download Pdf Manuals

Related Search

Related Contents

Purchase Order User Manual  LG 55WV70BS-B  カムクラッチ MLシリーズ  万 - About FedEx  ICES User Manual - University of Michigan  Targus 17” Groove Backpack  XPEED Outdoor Series Ver 1.0  

Copyright © All rights reserved. Failed to retrieve file