Model Checking a Lazy Concurrent List-Based Set Algorithm ZHANG Shaojie, LIU Yang National University of Singapore
Agenda Introduction Background Ourapproach Overview Linearizabilitydefinition Modelinglanguage Linearizabilityasrefinementrelation Experiment Conclusion&FutureWork
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
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
Agenda Introduction Background OurApproach Overview Linearizabilitydefinition Modelinglanguage Linearizabilityasrefinementrelation Experiment Conclusion&FutureWork
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
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 }
Concurrent List-based Set Thesentinelnodescanonlybecompared,not modified. - 1 3 4 + Sorted by the key (min & max possible keys)
Concurrent List-based Set Optimisticlockingscheme TraversewithoutLocking 1 2 4 e Add(3) 3 TheFourthIEEEInternational ConferenceonSecureSoftware
Concurrent List-based Set Optimisticlockingscheme Lockthetargetnodeanditspredecessor 1 2 4 5 3 Add(3)
Concurrent List-based Set Optimisticlockingscheme Validation i Node2isnotmarkedtrue Node4stillsuccessortoNode2 t N d 1 2 4 e 3 Add(3)
Concurrent List-based Set Optimisticlockingscheme scheme Validation 1 2 4 e Add(3) 3 TheFourthIEEEInternational ConferenceonSecureSoftware
Concurrent List-based Set Remove 1 2 3
Concurrent List-based Set Remove 1 2 3 Remove(2) 1 not marked 1 still points to 2
Concurrent List-based Set Remove 1 2 3 What if directly free node 2? physical Logical delete
Agenda Introduction Background OurApproach Overview Linearizabilitydefinition Modelinglanguage Linearizabilityasrefinementrelation ExperimentalResult Conclusion& FutureWork
Overview of Our Approach Thedefinitionoflinearizabilityiscasttotrace refinementrelation. Fullyautomatically Withouttheknowledgeoflinearizationpoints Modelinglanguage:CSP#(Communicating sequentialprograms) Event-based;LTS-basedsemantics Tool:PAT(ProcessAnalysisToolkit) Atoolkitforautomaticallyanalyzingevent-based concurrentsystemsincludingrefinementchecking
Overview of Our Approach Dynamicmemoryallocation Pre-allocateaboundedarrayasaprivatememory space Garbagecollection Referencecountingalgorithm
Linearizability Manifesto Eachoperationcould takeeffect instantaneouslybetweeninvocationand response Correlateeveryconcurrentexecutionwitha consistent sequentialatomicexecutionofthe operations. Preservereal-timeorder Respectthesequentialspecificationoftheobject th ti ifi ti f th t
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
Modeling language CSP# CommunicatingSequentialProcesseswithshared variables,low-levelprogrammingconstructsand userdefineddatastructures. d d t t Grammar
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
Linearizability as refinement relations
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.
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
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
Agenda Introduction Background OurApproach Overview Linearizabilitydefinition Modelinglanguage Linearizabilityasrefinementrelation Experiment Conclusion&FutureWork
Experimental result Testbed isaserverwith2.813ghzintelxeon64-bit CPUand32GBmemory. Themaximum numberof insertedkeys Thenumber ofprocesses Thenumberof operationseach processperformsperforms meansinfeasible. meansunboundednumber. ThismodelisbuiltinsidePAT,http://pat.comp.nus.edu.sg TheFourthIEEEInternational ConferenceonSecureSoftware
Optimization Functiondetailsaboutdynamicmemory allocationandreference-countinggarbage collectionarehidedintheembeddedlibraryof PAT. Nointermediatestatesduringthefunctionexecution aregenerated. Manuallycombinesequencesoflocalactions intooneatomicblockone
Agenda Introduction Background OurApproach Overview Linearizabilitydefinition Modelinglanguage Linearizabilityasrefinementrelation Experiment Conclusion&FutureWork
Conclusion Verifylinearizabilityusingtracerefinement relation Showthatrefinementcheckingalgorithmbehind PATallowsverifyinglinearizabilityagainst linearizability against concurrentobjects Withouttheknowledgeoflinearizationpointsthe of linearization Fullyautomatically ShowthatPATprovidesafairlyconvenientand efficientwaytodefinenewdatatypesand complexfunctionsinaprogramminglanguage Leavesthemodelclean l Avoidaugmentingbecauseoftheruntime environment
On-going and future work Dealwithinfamousstateexplosionproblem Symmetryreduction(inprogress) Partialorderreduction Combinevariousstatespacereductiontechniques andparameterizedrefinementcheckingforinfinite numberofprocesses
The End Thankyou! Q&A