Verifying a Quantitative Relaxation of Linearizability via Refinement
Contents
1. 2 2 Quasi Linearizability For two histories and o such that one is the permutation of the other we define their distance as follows Let o 1 2 3 n and o el 3 h Let ofe and a e be the indices of the event e in histories and g respectively The distance between the two histories denoted A o 0 is defined as follows A o 0 mazeco 0 le ofe In other words the distance between o and o is the maximum distance that an event in g has to move to arrive at its position in o While measuring the distance between two histories we often care about only a subset of method calls For example in a concurrent queue we may care about the ordering of enqueue and dequeue operations while ignoring calls to size operation In the remaining of this work we use words eng and deg for the interests of space Furthermore we may allow deq operations to be executed out of order but keep eng operations in order In such case we need a way to add ordering constraints on a subset of the methods of the shared object Let Domain o be the set of all operations of a shared object o Let d C Domain o be a subset of operations Let Powerset Domain o be the set of all subsets of Domain o Let D C Powerset Domain o be a subset of the powerset 28 K Adhikari et al Eng X gt Deqg X gt Deq Y gt lt End Y gt 4 Enq X gt 4 Deq Y gt 42. When the implementation model is indeed correct our method can also generate the formal proof quickly Paper Organization We establish notations and review the existing refinement check ing algorithm in Section 2 We present the overall flow of our method in Section 8 In Section 4 we present a manual approach for verifying quasi linearizability based on the existing refinement checking algorithm which is labor intensive and error prone We present our fully automated method in Section 5 based on our new algorithm for check ing the relaxed refinement relation We present our experimental results in Sections 6 We review related work in Section Jand conclude in Section 8 26 K Adhikari et al 2 Preliminaries We define standard and quasi linearizability in this section and review an existing al gorithm for checking the refinement relation between two labeled transition systems 2 1 Linearizability Linearizability is a safety property of concurrent systems over sequences of ac tions corresponding to the invocations and responses of the operations on shared ob jects We begin by formally defining the shared memory model Definition 1 System Models A shared memory model M is a 3 tuple structure O inito P where O is a finite set of shared objects inito is the initial valuation of O and P is a finite set of processes accessing the objects o Every shared object has a set of states Each object supports a set of opera
3. line 6 If there is any mismatch the check fails and we can return a counterexample showing how the violation happens Other wise we continue until pending is empty Lines 10 14 explore the new successor state pairs by invoking next_relaxed and add to pending if they have not been checked Subroutine enabled_relaxed spec QF It takes the current state spec of model M nec along with the quasi factor QF and generates all events that are enabled at state spec Consider the graph in Fig 5 as Mspec Without relaxation enabled s e1 This is equivalent to enabled_relaxed s 0 However when QF 1 according to the dotted edges in Fig 6 the set enabled_relaxed s 1 e1 e2 e3 The reason why ez and e3 become enabled is as follows before relaxation starting at state s there are two length 3 2QF 1 event sequences 0 e1 2 5 and 36 K Adhikari et al 02 1 3 4 When QF 1 it means an event can be out of order by at most 1 step Therefore the possilbe valid permutations of c1 is 71 e2 1 5 and T2 1 5 2 and the possible valid permutations of o2 is 73 3 1 4 and 74 1 4 3 for QF 1 In other words at state s1 events e2 e3 can also be executed We will discuss the generation of valid permutation sequences in Section 5 2 Subroutine next_relaxed impl spec QF It takes the current state impl of Mimpi and the current state spec of Mspec as input and retu
4. order execution or out of order by at most 1 step then the history is not quasi linearizable However if the quasi factor is 2 out of order by at most 2 steps then the third history in Fig is considered as quasi linearizable 2 3 Linearizability as Refinement Linearizability is defined in terms of the invocations and responses of high level oper ations In a real concurrent program the high level operations are implemented by al gorithms on concrete shared data structures e g a linked list that implements a shared stack object 21 Therefore the execution of high level operations may have compli cated interleaving of low level actions Linearizability of a concrete concurrent algo rithm requires that despite low level interleaving the history of high level invocation and response actions still has a sequential permutation that respects both the run time ordering among operations and the sequential specification of the objects For verifying standard but not quasi linearizability an existing method can be used to check whether a real concurrent algorithm we refer as implementation in this work refines the high level linearizable requirement we refer as specification in this work In this case the behaviors of the implementation and the specification are mod eled as labeled transition systems LTSs and the refinement checking is accomplished by using explicit state model checking Definition 5 Labeled Transition Syst
5. states and edges Note that this process is conducted on the fly AlgorithmBJexplains the high level pseudo code for expanding the state space for the current specification state under the check Let SEQ sequ seqo Seqx be the sequences which are reachable from the state so in Mspec such that each sequence has less than or equal to 2QF 1 events Each sequence seq E SEQ calls a genValidPer mut seq QF line 4 to generate all the possible valid permutation paths for that trace A new State is formed with a new transition for each event in the permuted sequences hence allowing the relaxed refinement checking of the implementation trace The valid permutations for a given sequence is generated using an Algorithm 4 which is based on the cost associated with the event Initially for each events e where 1 lt i lt n associated with the seq the cost is initialized to QF line 2 We generate all possible permutations and update cost with respect to the relative ordering of the events for each reshuffled sequences This cost attribute of an event stores the information on 38 K Adhikari et al Algorithm 3 Pseudo code for Expanding Specification Under Check 1 Let so be a specification state and QF be the quasi factor 2 Let SEQ seqr seq2 seq3 eqn be the set of all possible event sequences reach able from so in Mspec such that for 1 lt i lt k each seq has less than or equal to 20F 1 relaxed events 3 for all se
6. linearizability For example Liu et al use a process algebra based tool to verify that an implementation model refines a specification model the refinement relation Verifying a Quantitative Relaxation of Linearizability via Refinement 41 implies linearizability Vechev et al use SPIN to verify linearizability Cerny et al use automated abstractions together with model checking to verify linearizabil ity properties There also exists some work on proving linearizability by constructing mechanical proofs often with significant manual intervention e g 22 There are also runtime verification algorithms such as Line Up 4 which can di rectly check the actual source code implementation but for violations on bounded exe cutions and deterministic linearizability However quasi linearizable data structures are inherently nondeterministic For example the deq operation in a quasi queue imple mentation may choose to return any of the first k items in a queue To the best of our knowledge no existing method can directly verify quasi linearizability for execution traces of unbounded length Besides quasi linearizability there also exist many other consistency conditions for concurrent computations including sequential consistency 13 quiescent consis tency 2 and eventual consistency 24 Some of these consistency conditions in prin ciple may be used for checking the correctness of data structure implementations al though so fa
7. 2 2011 Sadowski C Freund S N Flanagan C Singletrack A dynamic determinism checker for multithreaded programs In Castagna G ed ESOP 2009 LNCS vol 5502 pp 394 409 Springer Heidelberg 2009 Sun J Liu Y Dong J S Chen C Integrating specification and programs for system modeling and verification In TASE pp 127 135 2009 Sun J Liu Y Dong J S Pang J PAT Towards Flexible Verification under Fairness In Bouajjani A Maler O eds CAV 2009 LNCS vol 5643 pp 709 714 Springer Heidelberg 2009 Treiber R K Systems Programming Coping with Parallelism Technical Report RJ 5118 IBM Almaden Research Center 1986 Vafeiadis V Shape value abstraction for verifying linearizability In Jones N D Miiller Olm M eds VMCAI 2009 LNCS vol 5403 pp 335 348 Springer Heidelberg 2009 Vechev M Yahav E Yorsh G Experience with model checking linearizability In Pasareanu C S ed SPIN 2009 LNCS vol 5578 pp 261 278 Springer Heidelberg 2009 Vogels W Eventually consistent Commun ACM 52 1 40 44 2009 Wang C Limaye R Ganai M Gupta A Trace based symbolic analysis for atomic ity violations In Esparza J Majumdar R eds TACAS 2010 LNCS vol 6015 pp 328 342 Springer Heidelberg 2010 Wang L Stoller S D Runtime analysis of atomicity for multithreaded programs IEEE Trans Software Eng 32 2 93 110 2006
8. 9 2 i O O I sok Y lt a l e E Bt A e2 1 e3 7 v 7 ot ot 5 O E s2 Sa Fig 5 Specification model before the addi Fig 6 Specification model after adding re tion of relaxed transitions for state s1 laxed edges for state s and quasi factor 1 Table 2 Specification Sequence Generation at State s1 BES Steps Frontier s2 s1 4 52 s3 s4 s1 4 52 3 s3 81 2 3 s4 s5 s2 s t S2 3 83 5 85 81 2 S2 S4 4 s2 In this case the valid permutation sequences are e2 1 s 1 5 e2 and e3 1 6 e1 e3 eg For each newly generated permutation sequence we add new edges and states to the specification model From an initial state s1 if we follow the new permuta tion e2 1 s as shown in Fig 6 the transition e2 will lead to newly formed pseudo state sg the transition e1 will lead to s7 from state sg and from this state it is reconnected back to the original state s5 via transition e5 Similarly if we follow the new permutation e3 1 e4 the transition e3 will lead to newly formed pseudo state sg the transition e Will lead to s19 from state sg and from this state it is reconnected back to state s via transition e4 We continue this process of state expansion for all the valid permutation sequences This relaxation process needs to be conducted by using every existing state of Mspec as the starting point for BFS up to 2QF 1 steps and then adding the new
9. Deq X gt End Y gt Eng X gt Deg Z gt SEn gt e Enq gt Fig 1 Execution traces of a queue Only the first trace at the top is linearizable The second trace is not linearizable but is 1 quasi linearizable The third trace is only 2 quasi linearizable Definition 3 Quasi Linearization Factor A quasi linearization factor is a function Qo D gt N where D is a subset of the powerset and N is the set of natural numbers Example 1 For a bounded queue that stores a set X of non zero data items we have Domain queue enq x deq x deq 0 X where enq x denotes the enqueue operation for data x deq x denotes the dequeue operation for data x and deq 0 indi cates that the queue is empty We may define two subsets of Domain queue d enq y y Y d2 deq y y E Y Let D d1 d2 where d is the subset of deq events and d is the subset of enq events The distance between o and o after being projected to subsets d and do is defined as A o a 0 a If we require that the eng calls follow the FIFO order and the deq calls be out of order by at most K steps the quasi linearization factor Q queue D N is defined as Q queue d1 0 Q fenieuey d2 K Definition 4 Quasi Linearizability Given a model M O 01 0 inito P p1 Pn Let H be the behavior of M M is quasi linearizable under the quasi factor Qo D gt N if for any his
10. Verifying a Quantitative Relaxation of Linearizability via Refinement Kiran Adhikari James Street Chao Wang Yang Liu and ShaoJie Zhang 1 Virginia Tech Blacksburg Virginia USA 2 Nanyang Technological University Singapore 3 Singapore University of Technology and Design Singapore Abstract Concurrent data structures have found increasingly widespread use in both multi core and distributed computing environments thereby escalating the priority for verifying their correctness Quasi linearizability is a relaxation of linearizability to allow more implementation freedom for performance optimiza tion However ensuring the quantitative aspects of this correctness condition is an arduous task We propose a new method for formally verifying quasi lineariz ability of the implementation model of a concurrent data structure The method is based on checking the refinement relation between the implementation and a specification model via explicit state model checking It can directly handle con current programs where each thread can make infinitely many method calls and it does not require the user to write annotations for the linearization points We have implemented and evaluated our method in the PAT verification framework Our experiments show that the method is effective in verifying quasi linearizability or detecting its violations 1 Introduction Linearizability is a widely used correctness condition for concurrent data struc tu
11. axed impl spec QF do 11 if impl spec checked then 12 pending enqueue impl spec 13 end if 14 end for 15 end while 16 return true 2 We replace enabled spec with enabled_relaxed spec QF It will return not only the events enabled at current spec state in Mspec but also the additional events allowed under the relaxed consistency condition 3 We replace next impl spec with next_relaxed impl spec QF It will return not only the successor state pairs in the original models but also the additional pairs allowed under the relaxed consistency condition Conceptually it is equivalent to first constructing a relaxed specification model M ae from Mspec QF and then computing the enabled spec and next impl spec on this new model However in this case we are constructing M ec automatically without the user s intervention Furthermore the additional states and edges that need to be added to Mj ec are processed incrementally on a need to basis At the high level the new procedure performs a BFS exploration for the state pair impl spec where impl is the state of implementation and spec is a state of specifi cation The initial implementation and specification events are enqueued into pending and each time we go through the while loop we dequeue from pending a state pair and check if all events enabled at state impl match with some events enabled at state spec under the relaxed consistency condition
12. can directly check a relaxed ver sion of the refinement relation This new algorithm subsumes the standard refinement checking procedure that has already been implemented in PAT In particular when QF 0 our new procedure degenerates to the standard refinement checking proce dure When QF gt 0 our new procedure has the added capability of checking for the quantitatively relaxed refinement relation Our algorithm can directly handle the imple mentation model Mj 1 the standard not quasi specification model Mspec and the quasi factor QF thereby completely avoiding the user s intervention We have evaluated our new algorithm on a set of models of standard and quasi lin earizable concurrent data structures 1 12 17 including queues stacks quasi queues quasi stacks and quasi priority queues For each data structure there can be several variants each of which has a slightly different implementation In addition to the im plementations that are known to be linearizable and quasi linearizable we also have versions which initially were thought to be correct but were subsequently proved to be buggy by our verification tool The characteristics of all benchmark examples are shown in Table 3 The first two columns list the name of the concurrent data structures and a short description of the implementation The next two columns show whether the implementation is linearizable and quasi linearizable Table 4 shows the results of the experime
13. ed as follows Given an implementation model Mimpi a specification model Mspec and a quasi factor Qo decide whether Mimpi is quasi linearizable with respect to Mspec under the quasi factor Qo Sequential Concurrent Sequential Concurrent Specification Implementation Specification Implementation F F tA Q 1 Q Create Manually Relaxing the Transitions 1 On Demand Quasi Lin Spec Model New Checking Algorithm t t Standard Refinement Checking Quasi Refinement Checking Impl vs Q Lin Spec Impl vs Spec Yes No Yes No Fig 2 Verifying quasi linearizability manual approach left and automated approach right The straightforward approach for solving the problem is to leverage the procedure in Algorithm I However since the procedure checks for standard refinement relation not quasi refinement relation the user has to manually construct a relaxed specification model denoted M a based on the given specification model Mspec and the quasi factor Qo This so called manual approach is illustrated by Fig P left The relaxed specification model M pec must be able to produce all histories that can be produced by Mspec as well as the new histories that are allowed under the relaxed consistency condition in Definition Unfortunately there is no systematic method or general guideline on constructing such relaxed specifica
14. em A Labeled Transition System LTS is a tuple L S init Act where S is a finite set of states init S is an initial state Act is a finite set of actions and C S x Act x S is a labeled transition relation For simplicity we write s 5 s to denote s a s The set of enabled actions at s is enabled s a Act ds S s Ss s A path 7 of L is a sequence of alternating states and actions starting and ending with states 7 s0 a1 1 2 such that so init and s ae Si 1 for all i If 7 is finite then r denotes the number of transitions in 7 A path can also be infinite i e containing infinite number of actions Since the number of states are finite infinite paths are paths containing loops The set of all possible paths for L is written as paths L A transition label can be either a visible action or an invisible one Given an LTS L the set of visible actions in L is denoted by vis and the set of invisible actions is denoted by invisz A 7T transition is a transition labeled with an invisible action A state s is reachable from state s if there exists a path that starts from s and ends with s denoted by s s The set of r successors is T s s E S s Ss ae inviszr The set of states reachable from s by performing zero or more 7 transitions denoted as r s can be obtained by repeatedly computing the 7 successors starting from s until a fixed point is reached We wri
15. emsegmeno os o A linearizable hence quasi implementation s s s Queue buggy1 Segmented queue with a bug Dequeue on the empty No o Coo queue may erroneously change current segment a a o s Table 4 Results for Checking Quasi Linearizability with 2 threads Queue 2 oa o a S o 3 318 530 Lin Stack 4 2 690 6 896 is completed in 21 2 seconds and 114 5 seconds respectively As the quasi factor is increased to 3 the verification time for quasi queue with size 4 and 8 is increased to 131 6 seconds 1517 1 seconds respectively which is much higher in comparison to the time for quasi factor 2 This is basically because of the significant increment in state expansion for the higher quasi factor For the priority queues where enqueue and dequeue operations are performed based on the priority the verification time is higher than the regular quasi queue Also it is important to note that the counterexample is produced with exploration of only part of the state space for the buggy models The verification time is much faster for the buggy queue which shows that our approach is effective if the quasi linearizability is not satisfied In all test cases our method was able to correctly verify quasi linearizability or detect the violations 7 Related Work In the literature although there exists a large body of work on formally verifying lin earizability in models of data structure implementations none of them can verify quasi
16. es The specifi cation model Msne has the following set of states 81 2 83 4 85 Suppose that the current state is s in step 0 then the current frontier state set is s1 and the current event sequence is s1 The results of each BFS step are shown in Table P In step 1 the frontier state set is s2 and the event sequence becomes s1 s2 In step 2 the frontier state set is s3 s4 and the event sequence is split into two sequences One is s Y s 3 s3 and the other is s1 Y s 3 s4 The traversal continues until the BFS depth reaches 2QF 1 After completing the 2Q F 1 steps of BFS starting at state spec as above we have to generate possible valid permutations first and then we will be able to evaluate the two subroutines enabled_relaxed spec QF and next_relaxed impl spec QF We transform the original specification model in Fig 5 to the relaxed specification model in Fig 6 for QF 1 The dotted states and edges are newly added to reflect the relaxation More specifically for QF 1 we will reach 2QF 1 3 steps dur ing the BFS At step 3 there are two existing sequences e1 e2 e5 and e1 es e4 For each existing sequence we compute all possible valid permutation sequences Verifying a Quantitative Relaxation of Linearizability via Refinement 37 r e Fd Isgh gt 510 4s11 sp ega A e3 e4 Le 2 amp 4 I y 7 a r BL EL e3 C4 a l a e2 4 U No ogee e O29 3
17. f the user constructed Mj incorrectly the verification result becomes invalid Therefore we need to design a fully automated method to directly verify quasi lin earizability of Mimpi against Mspec under the given quasi factor QF N N N N es 5 New Algorithm for Checking the Quasi Refinement Relation We shall start with the standard refinement checking procedure in Algorithm I and ex tend it to directly check a relaxed version of the refinement relation between M and M spec under the given quasi factor The idea is to establish the simulation relationship from specification to implementation while allowing relaxation of the specification 5 1 Linearizability Checking via Quasi Refinement The new procedure shown in Algorithm 2 is different from Algorithm as follows 1 We customize pending to make the state exploration follow a breadth first search BFS In Algorithm it can be either BFS or DFS based on whether pending is a queue or stack Verifying a Quantitative Relaxation of Linearizability via Refinement 35 Algorithm 2 Quasi Refinement Checking 1 Procedure Check Quasi Refinement impl spec QF 2 checked 3 pending enqueue initimpi initspec 4 while pending 4 0 do 5 impl spec pending dequeue 6 if enabled impl Z enabled_relaxed spec QF then T return false 8 endif 9 checked checked U impl spec 10 forall impl spec next_rel
18. g in SEQ do 4 PERMUT VALID genV alidPermut seq QF 5 for all perm in PERMUT_VALID do 6 Let perm e1 2 gt gt n T Let sn be the specification state reached from so via seq 8 if perm is not equal to seq then 9 for all e where 1 lt i lt n do 10 Create a new state s and a new transition from s 1 to s via event e 11 end for 12 Create a new transition from Sn 1 tO Sn Via en 13 end if 14 end for 15 end for Algorithm 4 genV alidPermut seq QF 1 PERMUT VALID 6 2 Initialize cost associated with each event in seq to QF 3 Generate possible permutations PERMUT_SEQ and update cost 4 for all p in PERMUT_SEQ do 5 isValid true 6 Let p e1 2 En T for all e where 1 lt i lt n do 8 if e cost gt 2QF V ei cost lt 0 then 9 isValid false 10 break 11 end if 12 end for 13 if isValid then 14 PERMUT_VALID PERMUT VALID p 15 endif 16 end for 17 return PERMUT_VALID how many more steps an event may be postponed Each time an event is postponed the cost associated with this event is decremented by 1 On the contrary the event can also be chosen upto QF steps ahead and for each step the cost is increased by 1 So the cost attribute of the event that is allowed for relaxation is 2QF lt cost lt 0 We check the validity of each of these sequences using this cost attribute line 8 Finally only the valid permutations are appended in PERMUT_VALID after each check a
19. i linearizable we construct a new model M spe which includes not only all histories of Mspec but also the histories that are allowed only under the relaxed consistency condition In this example we choose to construct the new model by slightly modifying the standard FIFO queue This is illustrated in Fig B upper half where the first K data items are grouped into a cluster Within the cluster the deq operation may remove any of the k data items based on randomization Only after the first k data items in the cluster are retrieved will the deq move to the next k data items a new cluster The external behavior of this model is expected to match that of the segmented queue in Mimp both are quasi linearizable Checking Refinement Relation Once Mj is available checking whether Mimpi re fines M aan is straightforward by using Algorithm For the segmented queue imple mentation 1 we have manually constructed M spec and checked the refinement relation in PAT Our experimental results are summarized in Table I Column 1 shows the differ ent quasi factors Column 2 shows the number of segments the capacity of the queue is QF 1 x Seg Column 3 shows the refinement checking time in seconds Col umn 4 shows the total number of visited states during refinement checking Column 5 shows the total number of state transitions activated during refinement checking The experiments are conducted on a computer with an Intel Core i7 2 5 GH
20. ification framework the specification model Mspec is written in a process algebra language named CSP 19 Implementation Model Mimpi The bounded quasi linearizable queue can be imple mented using a segmented linked list This is the original algorithm proposed by Afek et al i A segmented linked list is a linked list where each list node can hold K data items as opposed to a single data item in the standard linked list As shown in Fig 3 ower half these K data items form a segment in which the data slots are numbered as 1 2 K In general the segment size needs to be set to QF 1 where QF is the maximum number of out of order execution steps The example in Fig B has the quasi factor set to 3 meaning that a deq operation can be executed out of order by at most 3 steps Consequently the size of each segment is set to 3 1 4 Since Q queue Deng 0 meaning that the eng operations cannot be reordered the data items are enqueued regularly in the empty slots of one segment before the head points to the next segment But for deq operations we randomly remove one existing data item from the current segment Relaxed Specification Model M apee Not all execution traces of Mimpi are traces of Mspec In Fig 4 histories other than H1 a are not linearizable However they are all quasi linearizable under the quasi factor 1 They may be produced by a segmented queue where the segment size is 1 1 2 To verify that Mjm pj is quas
21. is the initial valuation of o and for all 7 1 2 according to the sequential specification the function the j th invocation in o together with state s _1 will generate the j th response in o and state s For example a sequence of read and write operations of an object is legal if each read returns the value of the preceding write if there is one and otherwise it returns the initial value Given a history a sequential permutation 7 of o is a sequential history in which the set of operations as well as the initial states of the objects are the same as in Definition 2 Linearizability Given a model M O 01 ok inito P pi Pn Let H be the behavior of M M is linearizable if for any history o in H there exists a sequential permutation 7 of o such that 1 for each object o 1 lt i lt k mo is a legal sequential history i e 7 respects the sequential specification of the objects and 2 for every op and ops in o if op lt o Ope then op lt r Opg i e m respects the run time ordering of operations o Linearizability can be equivalently defined as follows In every history if we assign increasing time values to all invocations and responses then every operation can be shrunk to a single time point between its invocation time and response time such that the operation appears to be completed instantaneously at this time point 163 This time point is called its linearization point
22. ishnan Eds SPIN 2013 LNCS 7976 pp 24 42 2013 Springer Verlag Berlin Heidelberg 2013 Verifying a Quantitative Relaxation of Linearizability via Refinement 25 Despite the advantages of quasi linearizability and its rising popularity e g 207 such relaxed consistency property is difficult for testing and validation Although there is a large body of work on formally verifying linearizability for example the meth ods based on model checking 15 14 23 5 runtime verification 4 and mechanical proofs 22 they cannot directly verify quasi linearizability Quasi linearizability is harder to verify because in addition to the requirement of covering all possible inter leavings of concurrent events one needs to accurately analyze the quantitative aspects of these interleavings In this paper we propose the first automated method for formally verifying quasi linearizability in the implementation models of concurrent data structures There are several technical challenges First since the number of concurrent operations in each thread is unbounded the execution trace may be infinitely long This precludes the use of existing methods such as LineUp 4 because they are based on checking permuta tions of finite histories Second since the method needs to be fully automated we do not assume that the user will find and annotate the linearization points of each method This precludes the use of existing methods that are based on either u
23. nd once the check is completed for all permuted sequences the function returns the valid traces Consider the event sequence e1 e2 e5 from state s be seq as shown in Fig 5 If QF 1 the cost for each of these events is initialized to 1 We generate all possible Verifying a Quantitative Relaxation of Linearizability via Refinement 39 permutations by reshuffling the events and updating the cost based on the relative posi tioning of the event with respect to the initial sequence There are as many as 6 possible permutations including the original sequence in this case If we consider reordering be the sequence e2 1 s then the cost associated with event e is 2 as it is chosen one step earlier For the event e1 it is postponed for one step meaning its cost is decreased by 1 which makes the cost associated with it be 0 Event e3 is not reordered and hence its cost is unchanged and is 1 This sequence is valid because cost associated with each of the events in this sequence lies within the allowable range Similarly if we consider another permuted sequence e3 1 2 then the cost associated with each of these events is 3 0 0 which exceeds the allowable range So this permutation sequence is not valid We do this for all the permuted sequences to generate the valid traces 6 Experiments We have implemented and evaluated the quasi linearizability checking method in the PAT verification framework 20 Our new algorithm
24. ng that deq can be out of order by 1 The first deq randomly 4 Quasi Factor 4 8 12 returns a value from the set 1 2 and IEG LSE the second deq returns the remaining one Quasi Implementation Then the third deq randomly returns a value from the set 3 4 and the forth deq Fig 3 Implementations of a 4 quasi queue returns the remaining one Our automated approach is shown in Fig 2 right It is based on designing a new refinement checking algorithm that in contrast to Algorithm can directly check a re laxed version of the standard refinement relation between Mimp and M spec Therefore the user does not need to manually construct the relaxed specification model Mf In stead inside the new refinement checking procedure we systematically extend states and transitions of the specification model Mspec so that the new states and transitions as required by Mj are added on the fly This would lead to the inclusion of a bounded degree of out of order execution on the relevant subset of operations as defined by the quasi factor Qo A main advantage of our new method is that the procedure is fully automated thereby avoiding the user intervention as well as the potential errors that may be introduced during the user s manual modeling process Furthermore by ex ploring the relaxed transitions on a need to basis rather than upfront as in the manual approach we can reduce the number of states that need
25. nses of operations that are performed on object o Every history of a shared memory model M O inito P must satisfy the following basic properties Correct interaction For each process p P o consists of alternating invoca tions and matching responses starting with an invocation This property prevents pipeline gperation Closedness Every invocation has a matching response This property prevents pending operations More rigorously the sequential specification is for a type of shared objects For simplicity however we refer to both actual shared objects and their types interchangeably in this paper Pipelining operations mean that after invoking an operation a process invokes another same or different operation before the response of the first operation 3 This property is not required in the original definition of linearizability in However adding it will not affect the correctness of our result because by Theorem 2 in for a pending invo cation in a linearizable history we can always extend the history to a complete one and preserve linearizability We include this property to obviate the discussion for pending invocations Verifying a Quantitative Relaxation of Linearizability via Refinement 27 A sequential history o is legal if it respects the sequential specifications of the objects More specifically for each object 0 there exists a sequence of states so 51 S2 of object o such that so
26. nts The experiments are conducted on a computer with an Intel Core i7 2 5 GHz processor and 8 GB RAM running Windows 7 The first column shows the statistics of the test program including the name and the size of benchmark The second column is the quasi factor showing the relaxation bound allowed for the model The next three columns show the runtime performance consisting of the verification time in seconds the total number of visited states and the total number of transitions made The number of states and the running time for each of the models increase with the data size For 3 segmented quasi queue with quasi factor 2 the verification completes in 7 2 seconds It is much faster than the first approach presented in Section 4 where the same setting requires 130 7 seconds for the verification Subsequently as the size increases the time to verify the quasi queue increases For queue with size 6 and 9 verification 40 K Adhikari et al Table 3 Statistics of Benchmark Examples Quasi Queue 3 Segmented linked list implementation size 3 Quasi Queue 6 Segmented linked list implementation size 6 Quasi Queue 9 Segmented linked list implementation size 9 N N Ye Queue buggy2 Segmented queue with a bug Dequeue may get No Saena ie tom awone seemed oao S o Lm Queus A Tinearizable hence quasi implementation Yes Ye Priority Queue buggy Segmented priority queue Dequeue on the empty No No pony queue may Shange cur
27. r none of them is as widely used as quasi linearizability These consis tency conditions do not involve quantitative aspects of the properties We believe that it is possible to extend our refinement algorithm to verify some of these properties work Outside the domain of concurrent data structures serializability and atomicity are two popular correctness properties for concurrent programs especially at the applica tion level There exists a large body of work on both static and dynamic analysis for detecting violations of such properties e g and 26 7 18 25 These existing methods are different from ours because they are checking different properties Al though atomicity and serializability are fairly general correctness conditions they have been applied mostly to the correctness of shared memory accesses at the load store in struction level Linearizability in contrast defines correctness condition at the method call level Furthermore existing methods for checking atomicity and serializability do not deal with the quantitative aspects of the properties 8 Conclusions We have presented a new method for formally verifying quasi linearizability of the im plementation models of concurrent data structures We have explored two approaches one of which is based on manual construction of the relaxed specification model whereas the other is fully automated and is based on checking a relaxed version of the refine ment relation between
28. res A concurrent data structure is linearizable if each of its operations method calls appears to take effect instantaneously at some point in time between its invocation and response Although being linearizable does not necessarily ensure the full fledged cor rectness linearizability violations are clear indicators that the implementation is buggy In this sense linearizability serves as a useful correctness condition for implementing concurrent data structures However ensuring linearizability of highly concurrent data structures is a difficult task due to the subtle interactions of concurrent operations and the often astronomically many interleavings Quasi linearizability 1 is a quantitative relaxation of linearizability to allow for more flexibility in how the data structures are implemented While preserving the basic intuition of linearizability quasi linearizability relaxes the semantics of the data structures to achieve increased runtime performance For example when implementing a queue for task schedulers in a thread pool it is often the case that we do not need the strict first in first out semantics instead we may allow the dequeue operations to be overtaken occasionally to improve the runtime performance The only requirement is that such out of order execution should be bounded by a fixed number of steps This work is supported in part by the National Science Foundation under Grant CCF 1149454 E Bartocci and C R Ramakr
29. rns a set of state pairs of the form impl spec Similar to the definition of next impl spec in Section 2 we define each pair mpl spec as follows 1 if impl impl where r is an internal event then let spec spec 2 if impl amp impl where e is a method call event then spec amp spec where event e enabled_relaxed spec QF is enabled at spec after relaxation For example when spec s in Fig 5 and the quasi factor is set to 1 meaning that the event at state s can be out of order by at most one step the procedure next_relaxed impl s1 1 would return not only mpl s2 but also mpl se and impl s9 as indicated by the dotted edges in Fig 6 The detailed algorithm for gen eration of the relaxed next states in specification is described in Section 2 5 2 Generation of Relaxed Specification In this subsection we show how to relax the specification Mspec by adding new states and transitions those that are allowed under the condition of quasi linearizability to form a new specification model Notice that we accomplish this automatically and incrementally on a need to basis For each state spec in Mspec we compute all the event sequences starting at spec with the length 2QF 1 These event sequences can be computed by using a simple graph traversal algorithm e g a breadth first search Fig 5 shows an example for the computation of these event sequenc
30. s CAV 2008 LNCS vol 5123 pp 52 65 Springer Heidelberg 2008 Flanagan C Qadeer S A type and effect system for atomicity In PLDI pp 338 349 2003 Herlihy M Shavit N The art of multiprocessor programming Morgan Kaufmann 2008 Herlihy M Wing J M Linearizability A correctness condition for concurrent objects ACM Trans Program Lang Syst 12 3 463 492 1990 Hoare C A R Communicating Sequential Processes Prentice Hall Englewood Cliffs 1985 Kirsch C M Payer H R ck H Sokolova A Performance scalability and semantics of concurrent FIFO queues In Xiang Y Stojmenovic I Apduhan B O Wang G Nakano K Zomaya A eds ICA3PP 2012 Part I LNCS vol 7439 pp 273 287 Springer Heidelberg 2012 Lamport L How to make a multiprocessor computer that correctly executes multiprocess programs IEEE Trans Computers 28 9 690 691 1979 Liu Y Chen W Liu Y Zhang S Sun J Dong J S Verifying linearizability via opti mized refinement checking IEEE Transactions on Software Engineering 2013 Liu Y Chen W Liu Y A Sun J Model checking linearizability via refinement In Cav alcanti A Dams D R eds FM 2009 LNCS vol 5850 pp 321 337 Springer Heidelberg 2009 Lynch N Distributed Algorithms Morgan Kaufmann 1997 Payer H R ck H Kirsch C M Sokolova A Scalability versus semantics of concurrent fifo queues In PODC pp 331 33
31. ser guidance e g 22 or annotated linearization points e g 23 To overcome these challenges we rely on explicit state model checking That is given an implementation model Mimpi and a specification model Mspec we check whether the set of execution traces of Mj is a subset of the execution traces of M spec Toward this end we extend a classic refinement checking algorithm so that it can check for the newly defined quantitative relaxation of standard refinement relation Consider a quasi linearizable queue as an example Starting from the pair of initial states of a FIFO queue specification model and its quasi linearizable implementation model we check whether all subsequent state transitions of the implementation model can match some subsequent state transitions of the specification model To make sure that the verification problem remains decidable we bound the capacity of the data structure in the model to ensure that the number of states of the program is finite We have implemented the new method in the PAT verification framework 20 PAT provides the infrastructure for parsing and analyzing the specification and implemen tation models written in a process algebra that resembles CSP 11 Our new method is implemented as a module in PAT and is compared against the existing module for checking standard refinement relation Our experiments show that the new method is ef fective in detecting subtle violations of quasi linearizability
32. spec denoted as spec spec Therefore the procedure starts with the pair of initial states of the two models and repeatedly checks whether their have matching successor states If the answer is no the check at lines 6 8 would fail meaning that Limpi is not linearizable Otherwise for each pair of immediate successor states impl spec we add the pair to the pending list The entire procedure continues until either 1 a non matching transition in Limpi is found at lines 6 8 or 2 all pairs of reachable states are checked in which case Limpi is proved to be linearizable In Algorithm I the subroutine next impl spec is crucially important It takes the current states of Limpi and Lspec as input and returns a set of state pairs of the form impl spec Here each pair mpl spec is one of the immediate successor state pairs of impl spec They are defined as follows 1 if impl impl where 7 is an internal event then let spec spec 2 if impl amp impl where e is a method call event then spec amp spec We have assumed without loss of generality that the specification model Lspec is de terministic If the original specification model is nondeterministic we can always apply standard subset construction of DFAs to make it deterministic Verifying a Quantitative Relaxation of Linearizability via Refinement 31 3 Verifying Quasi Linearizability The Overview Our verification problem is defin
33. te s 73 s iff s is reachable from s via only 7 transitions i e there exists a path s0 1 1 Q2 Sn such that so s Sn 8 and si ye Si 1 A A441 E tinvisy for all i Given a path 7 we can obtain a sequence of visible actions by omitting states and invisible actions The sequence 30 K Adhikari et al Algorithm 1 Standard Refinement Checking Procedure Check Refinement impl spec checked 0 pending push inttimp1 initspec while pending 4 do impl spec pending pop if enabled impl Z enabled spec then return false end if 9 checked checked U impl spec 10 forall impl spec next impl spec do OO SON Ne Ot 11 if impl spec checked then 12 pending push impl spec 13 end if 14 end for 15 end while 16 return true denoted as trace m is a trace of L The set of all traces of L is written as traces L trace m m paths L Definition 6 Refinement Let L and Lz be two LTSs L refines L written as Ly Ir L iff traces L C traces L2 o In 15 we have shown that if Limpi is an implementation LTS and Lspec is the LTS of the linearizable specification then Limp is linearizable iff Limpi Sr Lspec Algorithm I shows the pseudo code of the refinement checking procedure in 15 14 Assume that Limp refines Mspec then for each reachable transition in Mimpi denoted as impl impl there must exist a reachable transition in Li
34. the implementation model and the specification model For future work we plan to incorporate advanced state space reduction techniques such as sym metry reduction and partial order reduction References 1 Afek Y Korland G Yanovsky E Quasi Linearizability Relaxed consistency for im proved concurrency In Lu C Masuzawa T Mosbah M eds OPODIS 2010 LNCS vol 6490 pp 395 410 Springer Heidelberg 2010 2 Aspnes J Herlihy M Shavit N Counting networks J ACM 41 5 1020 1048 1994 42 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 K Adhikari et al Attiya H Welch J Distributed Computing Fundamentals Simulations and Advanced Topics 2nd edn John Wiley amp Sons Inc Publication 2004 Burckhardt S Dern C Musuvathi M Tan R Line up a complete and automatic lin earizability checker In PLDI pp 330 340 2010 3 ern P Radhakrishna A Zufferey D Chaudhuri S Alur R Model checking of lin earizability of concurrent list implementations In Touili T Cook B Jackson P eds CAV 2010 LNCS vol 6174 pp 465 479 Springer Heidelberg 2010 Farzan A Madhusudan P Causal atomicity In Ball T Jones R B eds CAV 2006 LNCS vol 4144 pp 315 328 Springer Heidelberg 2006 Farzan A Madhusudan P Monitoring atomicity in concurrent programs In Gupta A Malik S ed
35. tion models Each M spec may be different depending on the type of data structures to be checked And there is significant amount of creativity required during the process to make sure that the new specification model is both simple enough and permissive enough For example to verify that a K segmented queue 1 is quasi linearizable we can create a relaxed specification model whose dequeue method ran domly removes one of the first A data items from the otherwise standard FIFO queue This new model Mj will be more complex than Mspec but can still be significantly simpler than the full fledged implementation model Mimpi which requires the use of a complex segmented linked list Since the focus of this paper is on designing a fully automated verification method we shall briefly illustrate the manual approach in Section 4 and then focus on develop ing an automated approach in the subsequent sections 32 K Adhikari et al Quasi Factor gt Y Hl a H1 b Hl a H1 b n E eS A E E EE a EE A 695 10s Heer enq 1 enq 1 eng 1 eng 1 enq 2 enq 2 enq 2 eng 2 Quasi Abstract Specification eng 3 eng 3 eng 3 eng 3 eng 4 eng 4 enq 4 eng 4 deq 1 deq 1 deq 2 deq 2 deq 2 deq 2 deq 1 deq 1 SEGO SEG1 SEG2 deq 3 deq 4 deg 3 deq 4 it a deq 4 deq 3 deq 4 deq 3 2 6 10 Fig 4 Valid histories of a J quasi lin g y a earizable queue meani
36. tions which are pairs of invocations and matching responses These operations are the only means of accessing the state of the object A shared object is deterministic if given the cur rent state and an invocation of an operation the next state of the object and the return value of the operation are unique Otherwise the shared object is non deterministic A sequential specification of a deterministic resp non deterministic shared object is a function that maps every pair of invocation and object state to a pair resp a set of pairs of response and a new object state response and a new object state An execution of the shared memory model M O inito P is modeled by a history which is a sequence of operation invocations and response actions that can be performed on O by processes in P The behavior of M is defined as the set H of all possible histories together A history H induces an irreflexive partial order lt s on operations such that op lt o Opg if the response of operation op occurs in g before the invocation of operation op2 Operations in that are not related by lt are concurrent A history is sequential iff lt is a strict total order Let c be the projection of o on process p i which is the subsequence of consisting of all invocations and responses that are performed by p in P Let o o be the projection of on object o in O which is the subsequence of o consisting of all invocations and respo
37. to be checked 4 Verifying Quasi Linearizability via Refinement Checking In this section we will briefly describe the manual approach and then focus on present ing the automated approach in the subsequent sections Although we do not intend to promote the manual approach since it is labor intensive and error prone this section will illustrate the intuitions behind our fully automated verification method Given the specification model Mspec and the quasi factor Qo we show how to manu ally construct the relaxed specification model Mj in this section We use the standard FIFO queue and two versions of quasi linearizable queues as examples The construc tion needs to be tailored case by case for the different types of data structures Specification Model Msnec The standard FIFO queue with a bounded capacity can be implemented by using a linked list where deg operation removes a data item at one Verifying a Quantitative Relaxation of Linearizability via Refinement 33 end of the list called the head node and eng operation adds a data item at the other end of the list called the tail node When the queue is full eng does not have any impact When the queue is empty deq returns NULL As an example consider a sequence of four enqueue events eng 1 eng 2 enq 3 enq 4 the subsequent dequeue events would be deq 1 deq 2 deq 3 deq 4 which obey the FIFO semantics This is illustrated by the first history H1 a in Fig 4 In PAT ver
38. tory o in H there exists a sequential permuta tion 7 of o such that for every op and opo in o if op lt o Opa then op lt r op i e 7 respects the run time ordering of operations and for each object o 1 lt i lt k there exists another sequential permutation n of n such that 1 T o is a legal sequential history i e n respects the sequential specification of the objects and 2 A r o i d x o1 This definition subsumes the definition for linearizability because if the quasi factor is Qo d 0 for all d D then the objects behave as a standard linearizable data structure e g a FIFO queue a lt Qold foralld D Example 2 Consider the concurrent execution of a queue as shown in Fig 1 In the first part it is clear that the execution is linearizable because it is a valid permutation of the sequential history where Enq Y takes effect before Deq X The second part is not linearizable because the first dequeue operation is Deq Y but the first enqueue operation is Enq X However it is interesting to note that the second history is not Verifying a Quantitative Relaxation of Linearizability via Refinement 29 far from a linearizable history since swapping the order of the two dequeue events would make it linearizable Therefore flexibility is provided in dequeue events to allow them to be reordered Similarly for the third part if the quasi factor is 0 no out of
39. z processor and 8GB RAM running Ubuntu 10 04 34 K Adhikari et al Table 1 Experimental results for standard refinement checking MOut means memory out Verification Time s Visited State 2 0 1 2310 4458 1 D E a A 15213 0a 2680 a on Pas 08 sis 620s 230259 A a 2 1 06 26605 38281 286397 970980 a 34 130 7 74484213 8742485 Mow id C38ORE 3432702 7906856 The experimental results in Table I show an exponential increment in the verification time when we increase the size of the queue or the quasi factor This is inevitable since the size of the state space grows exponentially However this method requires the user to manually construct M apee which is a severe limitation For example consider the seemingly simple random dequeued model in Fig 3 A subtle error would be introduced if we do not use the cluster to restrict the set of data items that can be removed by deg operation Assume that deg always returns one of the first k data items in the current queue Although it appears to be correct such im plementation will not be k quasi linearizable because it is possible for some data item to be over taken indefinitely For example if every time deq chooses the second data item in the list we will have the following deg sequence deq 2 deq 3 deq 4 deq 1 where the dequeue of value can be delayed by an arbitrarily long time This is no longer a 1 quasi linearizable queue In other words i
Download Pdf Manuals
Related Search