Microsoft PowerPoint - Model Checking a Lazy Concurrent List-Based Set Algorithm.ppt [Compatibility Mode]

Size: px

Start display at page:

Download "Microsoft PowerPoint - Model Checking a Lazy Concurrent List-Based Set Algorithm.ppt [Compatibility Mode]"

倏浦司
5 years ago
Views:

1 Model Checking a Lazy Concurrent List-Based Set Algorithm ZHANG Shaojie, LIU Yang National University of Singapore

2 Agenda Introduction Background Ourapproach Overview Linearizabilitydefinition Modelinglanguage Linearizabilityasrefinementrelation Experiment Conclusion&FutureWork

3 Introduction Concurrentobjectsarenotoriouslyhardtodesign correctly. Esp.Lock-free&wait-freeones. Linearizabilityisanacceptedcorrectnesscriterionis an accepted correctness criterion forsharedobjects. Asharedobjectislinearizableifeachoperationon Asharedobjectislinearizable if each operation on theobjectcanbeunderstoodasoccurring instantaneouslyatsomepoint,(a.k.a.linearization point) Formalverificationorproofoflinearizabilityrely ontheknowledgeoflinearizationpoints Expertknowledge Linearizationpointsarehardtobestaticallydetermined

4 Introduction Verifylinearizaibilityagainstlazyconcurrentlistbasedsetalgorithm ProposedbySteveHeller,MauriceHerlihy,VictorLuchangco, MarkMoir,WilliamN,SchererIII,andNirShavitin2005. Moir and Nir Shavit in MartinVechev,EranYahav,andGretaYorshdescribeda variationwithweakervalidationconditionin2009. Whychoosethisalgorithm? Highlyconcurrent,non-fixedlinearizationpoints. Complexity:non-deterministictargetlocation Manipulatesdynamicallocatedmemoryheavily& Needagarbagecollector

5 Agenda Introduction Background OurApproach Overview Linearizabilitydefinition Modelinglanguage Linearizabilityasrefinementrelation Experiment Conclusion&FutureWork

6 Concurrent List-based Set Setinterface Unorderedcollectionofitems Noduplicates Methods bool add(int x):putxinset;ifsucceeds,returntrue boolremove(int x)takexoutofset )t t t bool contains(intx)testsifxinset

7 Concurrent List-based Set Setasasingle-linkedsortedlist Listnode public class Node { public int key; // item of interest public Node next; // Reference to next node public bool marked; //Indicate this node is about to be removed }

8 Concurrent List-based Set Thesentinelnodescanonlybecompared,not modified Sorted by the key (min & max possible keys)

9 Concurrent List-based Set Optimisticlockingscheme TraversewithoutLocking e Add(3) 3 TheFourthIEEEInternational ConferenceonSecureSoftware

10 Concurrent List-based Set Optimisticlockingscheme Lockthetargetnodeanditspredecessor Add(3)

11 Concurrent List-based Set Optimisticlockingscheme Validation i Node2isnotmarkedtrue Node4stillsuccessortoNode2 t N d e 3 Add(3)

12 Concurrent List-based Set Optimisticlockingscheme scheme Validation e Add(3) 3 TheFourthIEEEInternational ConferenceonSecureSoftware

13 Concurrent List-based Set Remove 1 2 3

14 Concurrent List-based Set Remove Remove(2) 1 not marked 1 still points to 2

15 Concurrent List-based Set Remove What if directly free node 2? physical Logical delete

16 Agenda Introduction Background OurApproach Overview Linearizabilitydefinition Modelinglanguage Linearizabilityasrefinementrelation ExperimentalResult Conclusion& FutureWork

17 Overview of Our Approach Thedefinitionoflinearizabilityiscasttotrace refinementrelation. Fullyautomatically Withouttheknowledgeoflinearizationpoints Modelinglanguage:CSP#(Communicating sequentialprograms) Event-based;LTS-basedsemantics Tool:PAT(ProcessAnalysisToolkit) Atoolkitforautomaticallyanalyzingevent-based concurrentsystemsincludingrefinementchecking

18 Overview of Our Approach Dynamicmemoryallocation Pre-allocateaboundedarrayasaprivatememory space Garbagecollection Referencecountingalgorithm

19 Linearizability Manifesto Eachoperationcould takeeffect instantaneouslybetweeninvocationand response Correlateeveryconcurrentexecutionwitha consistent sequentialatomicexecutionofthe operations. Preservereal-timeorder Respectthesequentialspecificationoftheobject th ti ifi ti f th t

20 Linearizability Example Observation Sequentialpermutation enqueue(1).inv enqueue(1).res dequeue().inv dequeue().res.2 enqueue(2).inv enqueue(2).res dequeue().inv dequeue().res.1 enqueue(1) enqueue(2) dequeue() -> 1 dequeue() -> 2 Timeline

21 Modeling language CSP# CommunicatingSequentialProcesseswithshared variables,low-levelprogrammingconstructsand userdefineddatastructures. d d t t Grammar

22 Linearizability as Refinement Relations Theorem SupposeLsp isalinearizablespecificationlts modelforasharedobjectο,considerlim that implementsobjectο,thentracesoflim ο then of are linearizableifflim refineslsp. 1 st -Step: Definethelinearizablespecificationmodel Specifyeachoperationopofasharedobjectoeach of a object o onaprocessp i usingthreeatomicsteps: theinvocationactioninv(op), i thelinearizationactionlin(op),(invisibleevent) i theresponseactionres(op,resp) i. TheFourthIEEEInternationalConferenceonSecureSoftwareIntegrationandReliability Improvement

23 Linearizability as refinement relations

24 Linearizability as Refinement Relations 2 nd -Step: Considertheimplementationofobjecto. implementation of object o Thevisibleeventsofimplarealsothoseinv(op) i 'sandres(op,resp) andres(op, resp) i 's. Memorymanagementoperationsare encapsulatedasmethodsintheinnerlibraryof PAT.

25 Linearizability as Refinement Relations Memoryallocation var<entrylist>l=newentrylist(m,min,max); ReferenceCountingGarbageCollector Alwayskeepthenumberofreferencestoeachlistnode Collectorrunswhenthereferenceofsomelistnodebecomes zero public class Node { public int key; public Node next; public bool marked; public int reference; //the number of variables pointing to this node } TheFourthIEEEInternationalConferenceonSecure SoftwareIntegrationandReliabilityImprovement

26 Linearizability as Refinement Relations ReferenceCountingGarbageCollector Wheneverapointervariabletoalistnodeismodified, updatethereference Predecessor = Current Assign(Predecessor, Current) {... IncreaseReference(Current) DecreaseReference(Predecessor) } Don tconsiderthenodesofwhichreferenceiszeroduring th d hi h f i d i thechecking

27 Agenda Introduction Background OurApproach Overview Linearizabilitydefinition Modelinglanguage Linearizabilityasrefinementrelation Experiment Conclusion&FutureWork

28 Experimental result Testbed isaserverwith2.813ghzintelxeon64-bit CPUand32GBmemory. Themaximum numberof insertedkeys Thenumber ofprocesses Thenumberof operationseach processperformsperforms meansinfeasible. meansunboundednumber. ThismodelisbuiltinsidePAT, TheFourthIEEEInternational ConferenceonSecureSoftware

29 Optimization Functiondetailsaboutdynamicmemory allocationandreference-countinggarbage collectionarehidedintheembeddedlibraryof PAT. Nointermediatestatesduringthefunctionexecution aregenerated. Manuallycombinesequencesoflocalactions intooneatomicblockone

30 Agenda Introduction Background OurApproach Overview Linearizabilitydefinition Modelinglanguage Linearizabilityasrefinementrelation Experiment Conclusion&FutureWork

31 Conclusion Verifylinearizabilityusingtracerefinement relation Showthatrefinementcheckingalgorithmbehind PATallowsverifyinglinearizabilityagainst linearizability against concurrentobjects Withouttheknowledgeoflinearizationpointsthe of linearization Fullyautomatically ShowthatPATprovidesafairlyconvenientand efficientwaytodefinenewdatatypesand complexfunctionsinaprogramminglanguage Leavesthemodelclean l Avoidaugmentingbecauseoftheruntime environment

32 On-going and future work Dealwithinfamousstateexplosionproblem Symmetryreduction(inprogress) Partialorderreduction Combinevariousstatespacereductiontechniques andparameterizedrefinementcheckingforinfinite numberofprocesses

33 The End Thankyou! Q&A

2/80 2

2/80 2 2/80 2 3/80 3 DSP2400 is a high performance Digital Signal Processor (DSP) designed and developed by author s laboratory. It is designed for multimedia and wireless application. To develop application