Automated test case generation for the Paxos single-decree protocol using a Coloured Petri Net model

(1)

Journal of Logical and Algebraic Methods in Programming 104 (2019) 254–273

Contents lists available atScienceDirect

Journal of Logical and Algebraic Methods in Programming

www.elsevier.com/locate/jlamp

Automated test case generation for the Paxos single-decree protocol using a Coloured Petri Net model

Rui Wang

^a^,∗

, Lars Michael Kristensen

^a

, Hein Meling

^b

, Volker Stolz

^a

aDepartmentofComputing,Mathematics,andPhysics,WesternNorwayUniversityofAppliedSciences,Norway bDepartmentofElectricalEngineeringandComputerScience,UniversityofStavanger,Norway

a rt i c l e i n f o a b s t ra c t

Articlehistory:

Received27March2018

Receivedinrevisedform10December2018 Accepted13February2019

Availableonline14February2019 Keywords:

ColouredPetriNets Distributedsystems Model-basedtesting

Implementing test suites for distributed software systems is a complex and time- consumingtask dueto the number of test cases that need to be considered in order toobtainhighcoverage.WeshowhowaformalColouredPetriNetmodelcanbeusedto automaticallygenerateasuiteoftest casesforthePaxosdistributedconsensusprotocol.

Thetest cases coverboth normaloperation ofthe protocolas well as failure injection.

Toevaluateourmodel-basedtestingapproach,wehaveimplementedthePaxosprotocol intheGoprogramminglanguageusingthequorumabstractionsprovidedbytheGorums framework.Ourexperimentalevaluationshowsthatweobtainhighcodecoverageforour Paxosimplementationusingtheautomaticallygeneratedtestcases.

©²⁰¹⁹^TheÂuthors.^Published^byÊlsevierÎnc.^Thisîsânôpenâccessârticleûnder^the^CC BYlicense(http://creativecommons.org/licenses/by/4.0/).

1. Introduction

Systematictestingisan importantactivityinsoftware development.Thisis especiallyimportantforfault-tolerantdis- tributedsystems,becausetheyarenotoriouslydiﬃculttoimplementcorrectly [1].Thereasonforthisdiﬃcultyisthatsuch systems must cope withboth concurrency and failures,e.g. due to crashes andnetwork partitions. Distributed systems therefore employ protocols withcomplex logic to tolerate individual componentfailures without causingservice disrup- tion forusers.Testing approachesandprogrammingabstractions thatcan be usedtosystematically test andsimplifythe implementationofprotocolsfordistributedsystemsarethereforeimportant.

Model-based testing(MBT) [2] has emerged asa powerful approach fortesting software,andas partof ourongoing researcheffort,weareinvestigatingtheapplicationofMBTonprotocolsforstatemachinereplication (SMR).SMRisacore technique fordevelopingfault-tolerantdistributedsystemsthatcan tolerateaboundednumberofserverfailures.InMBT, weconstructamodelofthesystemundertest(SUT)anditsenvironment,inordertogeneratetestcases.ThegoalofMBT is validation and error-detectionby ﬁnding observable differencesbetween the behavior ofthe implementation and the intended behavioroftheSUT,asdeﬁnedbythemodel.AtestcaseconsistsofinputstotheSUTandtheexpectedoutput, whichdetermineswhethertheexecutionofthetestwassuccessfulorfailed.Finally,itinvolvesimplementingatestadaptor that can be used to embedthe SUT,enabling the test casesto be executed against the SUT,andtheir output compared againsttheexpectedoutput.

ColouredPetriNets(CPNs) [3] areaformalmodelinglanguagethatcanmodeldistributedsystemscombiningPetriNets andtheStandardMLprogramminglanguage.PetriNetsprovidethefoundationformodelingconcurrency,synchronization,

*

Correspondingauthor.

E-mailaddresses:[email protected](R. Wang),[email protected](L.M. Kristensen),[email protected](H. Meling),[email protected](V. Stolz).

https://doi.org/10.1016/j.jlamp.2019.02.004

2352-2208/©²⁰¹⁹^TheÂuthors.^Published^byÊlsevierÎnc.^Thisîsânôpenâccessârticleûnder^the^CC^BY^license (http://creativecommons.org/licenses/by/4.0/).

(2)

R. Wang et al. / Journal of Logical and Algebraic Methods in Programming 104 (2019) 254–273 255

communication,andresourcesharing,whileStandardMLprovidestheprimitivesforcompactdatamodelingandsequential computations.Construction,simulation,validation,andveriﬁcationofCPNmodelsaresupportedbyCPNTools [4].CPNsand CPNTools havebeenwidely usedformodeling,validation, andveriﬁcationofdistributed systemsprotocols [5],buttheir applicationinsoftwaretestinghasonlybeenexplored toalimitedextent [6–8].Recently,CPNshavebeenexplored inthe contextofautomated codegenerationto obtainan implementationofamodeled system [9].Eventhough theautomated codegenerationisappliedtoobtainsuchanimplementationofthemodeledsystem,itisseldomthatthecorrectnessofthe model-to-texttransformations andtheirimplementation canbeformally proved.Thus, itisalso animportanttaskinthe engineeringofdistributedsystemstocomprehensivelytesttheimplementation.Therefore,wehavedevelopedtheMBT/CPN library [10] thatextendsCPNToolswiththesupportformodel-basedtestcasegeneration.ThereasonwechoseCPNsasthe foundationforourtestingapproachisthatCPNshaveastrongtrackrecordformodelingdistributedsystemsandareableto createparametricmodelsandperformmodelvalidation.Moreover,CPNsalsohavematuretoolstosupportbothsimulation andstatespaceexploration,whichisimportantforimplementingourapproachandforourpracticalexperiments.

The contributionofthispaperis theapplicationofCPNs andtheMBT/CPNlibrary [10] for model-basedtestingofan implementationofPaxos [11].Paxos isafault-tolerantconsensusprotocolthatmakes itpossibletoconstructareplicated service,orSMR,usingagroupofserverreplicas. Paxosisanimportantfoundationalbuildingblock, andawholefamilyof Paxos-basedprotocolshavebeendeveloped [12–15],focusingondifferentattributessuchaslatencyandthroughput.More- over,PaxosisalsothebasisformanyproductionsystemssuchasGoogle’sChubby [16] andSpanner [17],andAmazonWeb Services [18].However,Paxosisalsoknownforbeingdifficulttounderstandandimplementcorrectly [19].Themainaimof ourworkhasbeentodevelopapractically-orientedapproachthatnarrowsthegapbetweentheprovablycorrectintheory, andacorrectimplementation inpractice.Weusefinite-state modelcheckingto automaticallyvalidate thecorrectnessof smallconfigurations ofthe CPNmodel usedfortest casegeneration. Thisincreasesconfidence inthe testcases that are thensubsequentlyextractedfromrunningasetofsimulationsoftheCPNmodel.Theuseofsimulationtoextracttestcases (whicharethenexecutedagainsttheSUT)ensuresscalabilityofourapproach.Italsomeansthatourapproach(ingeneral) onlyteststheSUTagainsta subsetofthebehaviorsspecifiedby theCPNmodel.Assuch ourapproachshouldbeseenas aimedatvalidatinganimplementationanddetectingimplementationerrors.

Asecondarycontributionisanimplementationofthesingle-decreePaxosprotocolthatisespeciallyamenabletotesting.

Single-decreePaxosallows acollectionofserverstooperateasacoherentgroup andtoagree onacommonvalue,while toleratingthefailureofsomeofitsmembers.Theimplementation,writteninGo,takesadvantage ofquorumabstractions provided by the Gorums middlewarelibrary [20]. These abstractionsinclude the abilityto perform invocations on a set ofserver replicas, andcollect,analyze,andcombinea quorumof repliesinto asingle representative reply tobe usedin thenextprotocolstep.Theseabstractionsalsohelptoshieldtheprogrammerfromhavingtoexplicitlydealwithlow-level communicationanderrorhandling.

Thepaperisorganizedasfollows.§2introducesthePaxosconsensusprotocolandgivesanoverviewoftheconstructed CPNmodel, while§3provides detailedmodels ofthe various Paxos agents.§4 givesan overview ofGorumsandits abstractions,andoutlinesourGorums-basedimplementationofPaxos.§5presentsourtestingapproach,andourtestadapter developedtoexecutethetestcasesgeneratedfromtheCPNmodel.§6discussestestcasegenerationandourexperimental resultsobtainedusingCPNToolsandtheMBT/CPNtestinglibrary.§7discussesrelatedwork.Finally,§8concludesthepa- peranddiscussesfuturework.Thereaderisassumedtobefamiliarwiththebasicsyntacticalandsemanticalconceptsof PetriNets(places,transitions,tokens, andtransitionenabling andoccurrence).TheCPNmodelandPaxosimplementation presentedhereinareonlypartial.ThefulldetailsoftheCPNmodelareavailablevia [21].

2. ThePaxosconsensusprotocolandCPNmodeloverview

TheobjectiveofadistributedconsensusalgorithmsuchasPaxosistohaveasinglevaluechosenamongthoseproposed, whilethesafety(S)andliveness(L)properties [22,23] belowareupheldwithacorrectreplicabeingareplicathatdoesnot fail:

S1 Onlyaproposedvaluemaybechosen.

S2 Onlyasinglevalueischosen.

S3 Onlyachosenvaluemaybelearnedbyacorrectreplica.

L1 Someproposedvalueiseventuallychosen.

L2 Onceavalueischosen,correctreplicaseventuallylearnit.

Note that the deﬁnitionpermits multiple valuesto be proposed forconsensus. An algorithm satisfying the above safety propertiesisconsideredsafeinthatallreplicasthatlearnthechosenvalueremainconsistentwitheachother.However,we notethat distributedconsensusisimpossibleinan asynchronoussystemmodel [24].Therefore,tosatisfyliveness,periods ofsynchronyarerequired.

Thesingle-decreePaxos consensusprotocolcanbe usedbyadistributedapplication, inwhichthePaxosreplicasneed toagreeonasinglecommonvalueamongpotentiallymanyinputvalues.Weassumethattheinputvaluesaresenttothe Paxosreplicasfromoneormoreclients,andthenthedecidedoutputvalueisreturnedtotheseclients.

(3)

256 R. Wang et al. / Journal of Logical and Algebraic Methods in Programming 104 (2019) 254–273

Fig. 1.Top-level CPN module for Paxos.

Fig. 2.TheClientsCPN module.

The constructedCPN model ofthe single-decree Paxos protocol iscomprised of 23 hierarchicallyorganized modules.

Fig. 1showsthetop-level moduleof theCPNmodelconsistingof twosubstitution transitions(drawnasrectangles with a double border)connected bythe two places Request andResponse.The nameofthe submodule associatedwitheach substitution transitioniswritteninthename-tagpositionednexttothesubstitutiontransition. Thesubstitutiontransition ClientsanditsassociatedsubmoduleClientsaremodelingthebehavioroftheclientsthatmayproposevaluestobechosen.

The substitution transitionReplicas and its associated submodule are modeling the behavior of the distributed replicas executing thePaxosprotocolinordertoreachconsensusonavalueproposedbytheclients.Theclientsendsarequestto thePaxosreplicasbyputtingatokenontheplaceRequestandthenwaitsforthedecidedresponsevaluetobereturnedas atokenonplaceResponse.

Fig. 2showsthe submoduleofthe Clientsubstitution transition.The portplaces Request andResponseare associated with the identically namedsocket places in Fig. 1. Thismeans that anytokens addedto or removed fromthese places by transitions intheProposeValue modulewill bereﬂected inthe top-levelmodule.The submodule ofthe ProposeValue substitutiontransitionmodelsthebehaviorofsendingaclientrequestvalueforconsensustothePaxosreplicas.

Paxos [11,22] isoftendescribedintermsofthreeseparateagentroles:proposersthatcanproposevalues,acceptorsthat acceptavalueamongthoseproposed,andlearnersthatlearnthechosenvalue.APaxosreplicamaytakeonmultipleroles:

in a typical conﬁguration (and alsoin the CPNmodel), all replicas play all roles.Paxos is safe foranynumber of crash failures,andcanmakeprogresswithupto f crashfailures,givenn=²^f+1 acceptors.

Fig.3showstheReplicasmodulewhichisthesubmodule ofthesubstitutiontransitionReplicasinFig.1.Themodule has a substitution transitionforeach Paxos agent connected by socketplaces to modelthe communicationbetweenthe different agents.Thedetailedbehaviorsofthe agentsarethen modeled inthe submoduleof thesubstitution transitions.

TheReplicasmodulehasbeenconstructedsuchthatwecanconﬁgureanynumberofreplicas,eachencapsulatingthethree Paxos agents,without modifyingthe net-structure.Thisallows ustoeasily generatetest casesfordifferently sizedPaxos conﬁgurations.

The Paxos protocol operates in rounds, which refer to a set of semantically related messages that may or may not concludetheconsensusprotocol.Wesaythattheprotocolsolvesconsensusinsomeround.Duetoasynchronyandfailures,

(4)

Fig. 3.The single-decreeReplicasmodule.

Fig. 4.The single-decree Paxos consensus protocol with three phases.

aconsensusprotocolmayneedtorunseveralroundstosolveconsensus.Whendescribingtheprotocol,weusethevariables rnd,crnd, andvrnd to denoteroundnumber, currentround,andvotedinround.Everyround isassociatedwitha single proposer, which is the leader forthat round. Other proposers can start new (higher)rounds concurrently by sending a ^Prepare ^message^to âcceptors, ^to ^collect ^Promise^s ^from^the âcceptors ^to ^followâ ^new^proposer. ^This îs êssential ^for Paxostomakeprogressincasethecurrentleadergoesmute.Everyroundrunsinthreephases:

1. Aproposersendsa^Prepare^message^to^theâcceptorsând^collectsât^least ^f+¹^Promise^messages;

2. theproposerthensends^Accept^messages^for^some^value ^v ^to^the^acceptors,^who^respond^by^sending ^Learn^mes- sagesbacktotheproposeracknowledgingthevalue v;

3. theproposersendsthedecidedvaluein^Commit^messages^to^learners.

The commoncaseexecutionofthethree phasesisshowninFig. 4.Thefirst numberineach messageis thernd=^1, and v isthe valuethat theproposer wantstheacceptors tochoose.The grayboxes labeled v representthe executionof astate machinecommandderivedfromthedecidedvalue v.Whilenot showninthefigure,eachreplicahasinstancesof eachofthePaxosagents.ThecommunicationbetweenthedifferentPaxosagentshasbeenmodeledbasedonthequorum abstractionsprovided by the Gorumsframework [20], which we discussin§4.Specifically, the communicationtakesthe formofquorumcalls,oneforeachofthePaxosphases:Prepare,Accept,andCommit.

Thevalue v tochooseisthe valuewiththe highestround amongthoseprovidedin the^Promise^messages, ôrîf^no votesare providedin the^Promise ^messages,âny^value ^can^be ^chosen ^by ^the^proposer; ^this^would^typically ^beâ ^value that theproposer receivedfroma client.InPaxos,acceptors are saidto havechosenavalue v,ifa majorityofacceptors havevotedforv inthesameround.Onceavaluehasbeenchosen byacceptorsinaround,noothervalue canbechosen inanyother round.However, ifthere isno majorityofacceptors thathavevoted forv,then theacceptors mayvotefor differentvaluesinother rounds.Sinceroundsexecute concurrently,thereisnoguaranteeofprogressevenifthereareno failuresormessageloss.Therefore,Paxostypicallyreliesonaneventualleaderdetectionprotocol,oftenimplementedfrom

(5)

Fig. 5.TheProposermodule.

thefailuredetector [25].Whilemaybeinaccurateforsometime,eventuallyitmakescorrectproposersagreeonwhich proposeristheleader.Using,andundertheassumptionthatn≥²^f+1 acceptors,PaxossatisﬁesProperties L1and L2.

3. ModelingthePaxosagents

Thissection presentsthebehavioralmodelingofthe Paxosagents.Oneofthe Proposersisdesignatedasa leaderand proposestheclientrequestvalueforconsensus.TheAcceptorschoosetheconsensusvalueamongthoseproposed,andthe Learner ofeach replicalearnsthedecidedvalue. Onceavalue hasbeenlearnedbya Learner,aresponse maybesentby thisLearnertotheclient.ThisresponseispresentedasatokenontheportplaceResponse.

3.1. Proposers

The submodule of the Proposer substitution transition is shown in Fig. 5. It contains three substitution transitions:

LeaderDetector,FailureDetector,andProposerCore.The Proposer ofeachreplica receives theclientrequest(presented asa tokenontheportplaceRequest)forconsensus,sentfromthesubmoduleoftheClientssubstitutiontransition.

InPaxos,oneoftheProposersisresponsiblefordrivingtheconsensusprocess,namelytheleader.However,duetothe asynchronous nature ofthe environmentin whichwe are operating,we mayhavethat manyProposers believe they are theleader,thusthePaxosprotocolcanonlyguaranteeprogressifoneofthemiseventuallychosen.Therefore,theobjective ofthe ﬁrstphaseofPaxos istoobtain permissionsfromtheAcceptors thata particularProposer canserveastheleader.

However, to be able to detect ifa newproposer should initiate the ﬁrst phase, we use the LeaderDetector substitution transitionwhich hasasubmodule topicka leaderamongthe Proposers.Thissubmodule isinformedaboutfailuresfrom the failure detector. The FailureDetectorsubstitution transition hasa submodule that can detect thefailure of anyof the Proposers.Then,anotherleadercanbe selectedbythesubmodule ofthe LeaderDetectorsubstitutiontransitionandit can takeovertheleadershipbystartingtheﬁrstphaseofPaxoswithahigherroundnumberthanpreviousleaders.

Paxosusesroundnumberstorankreplicas,andeachreplicahasauniquesetofroundnumbers.Morespecifically,each round isassignedto asingle proposer. Thechoice oftheproposer forround i isdetermined by adeterministic mapping p:^B→^P^,^where ^B îs^the ^set ôf ^round ^numbersând ^P îs ^the ^setôf ^proposers. În ^this^paper, ^we âssume ^that ^B îs ^the set ofnaturalnumbers,andthatproposers haveassignedidentities0,1,. . . ,|^P|−^1, ^where|^P|=^n.^Then, ^we^can ^choose mapping psuchthatp(i)=ⁱ (mod|^P|)^.

A clientrequestpresentedasatokenvalue onthe portplaceRequest willbe sentto theProposerCore,waiting tobe handledbytheleaderascanbeseenfromFig.5.

The submodule oftheProposerCore substitutiontransitionisshownin Fig.6andmodelsthe internalbehavior ofthe Proposer. In this module, the InitProposer substitution transition has a submodule to initialize Proposers, obtain a new

(6)

Fig. 6.TheProposerCoremodule.

leader,andreceiveaclientrequestforconsensus.Then,thevalueofthecurrentroundnumberoftheleaderandthevalue ofthereceivedclientrequestwillbepresentedontheportplacesastokens,respectively.Thesetokenswillbehandledby thesubmoduleofthePhasessubstitutiontransition.

Asuccessfulroundofthesingle-decreePaxosprotocolhasthreephases,modeledbysubmodulesofthethreesubstitution transitionsshowninFig.7.Theﬁrstphaseinvolvestwotypesofmessagesknownasthe^Prepare^and^Promise^messages.

Theleadercandidatecreatesa^Prepare^message^withîts^current^round^numberândînvokesâ ^Prepare^quorum^call.^This ismodeledbythesubmoduleofthePreparesubstitutiontransition,showninFig.6,whichsendsthe^Prepare^message^to Acceptorsinordertoproposeitselftobealeader.AftertheAcceptorsreceivethe^Prepare^message,ândîf^theyâcceptedît, theneachAcceptorreturnsbacka^Promise^message^to^the^leader^candidate^by^the^Prepare^quorum^call.^Thisîs^modeled^by thesubmoduleoftheAcceptorsubstitutiontransitionshowninFig.3.Whentheleadercandidatereceivesenough^Promise messages fromAcceptors(obtaina quorum),then thefirst phaseis finished,which meanstheleader candidatenow can becomealeader,andproposetheclientrequesttoAcceptorsforconsensus.

In the second phase, the leader creates an Âccept ^message ^with îts ^current ^round ^number, ^crnd, ând ^the ^value ^v obtainedfromtheclientrequest,andinvokestheAcceptquorumcall,modeledbythesubmoduleoftheAcceptsubstitution transition, shown in Fig. 6.This quorum call sends the Âccept ^message ^to ^the Âcceptors, ^requesting ^them ^to ^vote ^for consensus value v.Upon receiving anÂccept^message^whose^round ^numberîs^greaterôrêqual^to ^theÂcceptor’s^round number, the Acceptor will returna ^Learn ^message ^to ^the ^leader. Ônce ^the ^leader ^has ^received â ^quorum ôf Âccept messagesfromAcceptors,thesecondphaseisdone.Forthethirdphase,theleaderinvokestheCommitquorumcallonthe Learners,asmodeledbythesubmoduleoftheCommitsubstitutiontransition,showninFig.6.ThisenablestheLearnersto learnthechosenconsensusvalueandcansendittotheclient.

Fig.8showsthesubmoduleofthePhaseOnesubstitutiontransition.Theleaderusesitscurrentroundnumbertocreatea ^Prepare,0,crnd^message^by^triggering^the^transitionSendPrepareMessagesothatthismessagecanbeplacedontheport

(7)

Fig. 7.ThePhasesmodule.

place Prepareasatoken toinvoke thePreparequorumcall.Thisquorumcall returnsa^Promise,cid,rnd,(vrnd,v value) messageaswealreadydiscussed,wherecidisthecallID(initializedas0in^Prepare^message);^rndîs^the^round^number confirmedbytheAcceptor; vrndisthemostrecentroundinwhichtheAcceptorvoted,andv value istheconsensusvalue itvotedfor.TheplaceFDControl providesanupperboundonthenumberoftimeouts/failuresinourtest cases.Thisplace isnotpartoftheCPNmodelforsingle-decreePaxos,butisusedtocontrolthetestenvironment.Ifnotimeoutoccurs,and theleaderobtainedaquorumof^Promise^messages,^the^second^phase^can^start.^The^placeFailedReplicaisusedtocollect theidentityoffailedreplicas,whichweusein§6forvalidationofthemodel.Thesecondandthirdphasesaremodeledin asimilarmannerasthefirstphase,andwedonotincludethemhere.

Afterthe^Promise^message^returns,â^timeout^could^happen^to^trigger^the^failure^detector^when^theProcessPromiseMes- sagetransitionoccurs.Thisisusedtocapturescenarioswhereafailureofanyreplicaoccurs.Suchfailureismodeledasan eventthatmayoccurafteraquorumhasbeenobtainedforthequorumcall,which,inthiscase,isrepresentedasatoken ofthe^Promise^messageâppearingôn^the^port^place^Prepare.Ât^this^stage,ânôccurrenceôf^theProcessPromiseMessage transition(Fig.8)mayresultinatimeoutmodeledbythecreationofatokenontheportplaceTimeoutFDsignalingthata failure hasoccurred. Wemaythen haveafinitesequenceoftransitionoccurrencesfortheaccomplishmentofthePrepare quorumcall (inthiscase)andforfinishingthe remainingtransitionsinthesubmodule oftheLeaderDetectorsubstitution transition.Afterthis,thetransitionsforleaderdetectioninthesubmoduleoftheFailureDetectorsubstitutiontransitionwill occur asthey aregivenhigherprioritycomparedtoother transitionsinthemodel.Thisensuresthattheexecutionofthe failure detectorcannot be forever postponedandthe currentleader ID(round number) forthisfailedround isobtained, whichthencausestheexecutionoftheleaderdetectortoelectanewleader.Thefactthatthefailuredetectorwillbeexe- cutedinafinitenumberofstepsfromwhenafailurehasoccurred,restrictsthebehaviorofthemodelandinturnimplies thatthemodelsatisfiespropertiesL1(aproposedvalueiseventuallychosen)andL2(thatcorrectreplicaseventuallylearns thechosenvalue).

3.2. Acceptors

This section details the model for the acceptors. Fig. 9 showsthe Acceptor module. The submodule consists of Han- dlePrepareandHandleAcceptsubstitutiontransitions.Theformerhandles^Prepare^messages^sent^by^the^submodule^of^the Proposer substitution transitionshowninFig.3through theportplacePtoAPrepare.Thelattersimilarlyhandles^Accept messagesalsosentbytheProposerthroughportplacePtoAAccept.

(8)

Fig. 8.ThePhaseOnemodule.

Fig. 9.TheAcceptormodule.

The AcceptorState place represents the state of each Acceptor. It is initialized with each replica’s ID, round number rnd=^0,^last^voted^round^vrnd=^0,^and^voted^value ^{v value}=

ε

(emptystring).

The submoduleof theHandlePrepare substitution transitionisshowninFig. 10.The HandlePreparetransitionhandles ^Prepare^messages^sent^by^the^Proposer.Îf^the^crndôf^the^Prepare^messageîs^higher^than^theÂcceptor’s^rnd,^then^the token placedonthe AcceptorStateport placeisupdated accordingly,anda newtokenforthe ^Promise^message^can ^be placedon theAtoPPrepare portplace accordingtotheexpression ofthearcconnectingtheHandlePrepare transitionand AtoPPrepareplace.WedonotshowthesubmoduleoftheHandleAcceptsubstitutiontransitionasitissimilartoHandlePre- pare. The main difference is that it updatesthe triplet (rnd,vrnd,v value) inthe AcceptorState port place,and places a ^Learn^messageôn^theÂtoPAccept^place.

3.3. Learners

Finally,wediscusstheLearnersubstitutiontransitionshowninFig.3,whichhasasubmodulewithasingleHandleCom- mitsubstitutiontransition,asshowninFig.11.Thissubmodulehandlesthe^Learn^message^sent^by^the^Proposer,^checking thataquorumoflearnmessageshavebeenreceivedbeforereturningthedecidedconsensusvaluetotheclientbyplacinga tokenontheResponseportplace.ThisbehaviorismodeledbythesubmoduleoftheHandleCommitsubstitutiontransition, showninFig.12.

(9)

Fig. 10.TheHandlePreparemodule.

Fig. 11.TheLearnermodule.

Fig. 12.TheHandleCommitmodule.

(10)

Fig. 13.Gorums abstractions.

4. Gorumsandsingle-decreePaxosimplementation

Gorums [20] is a framework forimplementing quorum-baseddistributed systems.This section describesGorumsand howweuseittoimplementsingle-decreePaxos [11].OurgoalhereistoprovideaPaxosimplementationthatisamenable totestingbasedontheCPNmodelin§3,andin§5wedescribeourtestingapproach.

4.1. Gorumsabstractions

Gorumsisalibrarywhosegoalistoalleviatethedevelopmenteffortforbuildingadvanceddistributedalgorithms,such asPaxos [11] and distributedstorage [26,27].Thesealgorithms arecommonlyusedtoimplementreplicated services,and theyrelyonaquorumsystem [28] toachievefaulttolerance.Inaquorumsystem,suchasPaxos,protocolreplicasneedto exchangeandupdateinformationabouteachother’sstate.However,toensureconsistency,areplicamustcontactaquorum, e.g. amajorityofthereplicas.Inthisway,asystemcanprovideservicedespitethefailureofindividual replicas.However, communicatingwithandhandlingrepliesfromsetsofreplicasoftencomplicatetheprotocolimplementations.

Toreduce thiscomplexity,Gorums provides threecore abstractions:(a) configurations that group a setof replicasto hidetheexistence ofindividualreplicas, (b) aflexibleandsimplequorumcallabstraction, whichisusedtocommunicate witha configuration,i.e. a setofreplicas, andto collecttheir responses, and(c) a quorumfunction abstraction whichis usedto process responses.Theseabstractions canhelp tosimplifythe maincontrol flowofprotocolimplementations, as weillustratelaterinthissection.

Fig.13illustratestheinterplaybetweenthemainabstractionsprovidedbyGorums.Gorumsconsistsofaruntimelibrary andcodegeneratorthatextendsthegRPC [29] remoteprocedurecalllibraryfromGoogle.Speciﬁcally,Gorumsallowsclients toinvokeaquorumcall,i.e.asetofRPCs,onagroupofservers,andtocollecttheirreplies.Therepliesareprocessedbya quorumfunctiontodetermineifaquorumhasbeenreceived.Notethatthequorumfunctionisinvokedevery timeanew replyisreceivedattheclient,toevaluatewhetherornotthereceivedsetofrepliesconstitutesaquorum.

Protocoldevelopers usingGorumscan specifyRPCservicemethodsusingprotobuf[30], andfromthisspecification, Gorums’scode generatorwill producecode tofacilitatequorum callsandcollection ofreplies.Eachquorum callmethod mustprovideauser-definedquorumfunctionthatGorumswillinvoketodetermineifaquorumhasbeenreceivedforthat specificquorumcall.Inaddition,the quorumfunction willalsoprovideasingle replyvalue, basedonacoalescingofthe receivedreplyvaluesfromthedifferentserverreplicas.Thiscoalescedreplyvalueisthenreturnedtotheclientastheresult ofitsquorumcall.Thatis,theinvokingclientdoesnotseetheindividualreplies.

Thequorumfunctionsforaspeciﬁcprotocolimplementationmustfollowawell-deﬁnedinterfacegeneratedbyGorums.

These only require a set of reply values asinput and a return of a single reply value together witha booleanquorum decision.Hence,quorumfunctionscaneasilybetestedusingmanuallywrittenunittests.However,somequorumfunctions involvecomplexlogic,andtheirinputandoutputdomainsmaybelarge,andsogeneratingtestcasesfromamodel,provide signiﬁcantbeneﬁtforverifyingtheircorrectness.

AquorumcallisimplementedbyasetofRPCs,invokedatdifferentservers,andsomustconsiderdifferentinterleavings duetoinvocationsbydifferentclients.Hence,usingmodel-basedtestingwecanproducesequencesofinterleavingsaimed atﬁndingbugsintheserver-sideimplementationsoftheRPCmethodsandalsointheGorumsruntimesystem.

Fig.14gives thePrepare quorumcallmodule ofthePrepare substitution transitionin Fig.6.This modulemodelsthe behaviorofthequorumcallandquorumfunctionabstractionsprovidedbyGorumsforsendingthe^Prepare^messages^from aProposer(leader)toAcceptorswhenthetransitionSendPrepareMessagesoccurs.Then,aftersuch^Prepare^messages^are handledbyAcceptors,thereplied^Promise^messages^from^Acceptors^can^be^processed^when^the^transitionApplyPrepareQF occurs,whichmodelsthebehaviorofthePreparequorumfunction.Thelogictoimplementsuchquorumfunctionwillbe discussedin§4.2.

(11)

Fig. 14.ThePreparequorum call module.

type SinglePaxosServer interface {

Prepare(context.Context, *PrepareMsg) (*PromiseMsg, error) Accept(context.Context, *AcceptMsg) (*LearnMsg, error) Commit(context.Context, *LearnMsg) (*Empty, error) ClientHandle(context.Context, *Value) (*Response, error) Ping(context.Context, *Heartbeat) (*Heartbeat, error) }

Listing 1: TheSinglePaxosServerinterface that Paxos replicas must implement.

Our goalin thispaper isto provide a framework forgenerating test casesto validate the correctness ofthe Gorums implementation itself, in addition todifferent quorum function andquorum call implementations forour Gorums-based Paxosimplementation.

4.2. Implementingsingle-decreePaxosusingGorums

Wehaveimplementedthesingle-decreePaxosprotocolasoursystemundertest,usingGorumsandtheGoprogramming language. Thesystemconsistsofn=²^f+^{1 replicas}^that ^run^the^Paxos^protocol, ^taking^client^requestsâsînput,âimedât reachingconsensusonasingleoutputresponse.TheimplementationcorrespondstotheCPNmodeldiscussedin§2and§3.

In our implementation, we first define a set of RPC service methods for Paxos using the interface description language (IDL) ofprotocol buffers [30]. ThisIDL isthen supplied to the Gorumscode generator, which generates the code necessarytoinvokequorumcallsforthemethodsdefinedintheIDL.EachofthePaxosreplicasmustimplementtheSin- glePaxosServer interface shown inListing 1,which is generated fromthe IDL. The methods Prepare(), Accept()and Commit()inthisinterfacerepresentPaxosquorumcallsthatcanbeinvokedbythedifferentreplicasinordertoaccessand updateeachother’sPaxosstate.

In additionto thePaxos methodsmentioned above,the SinglePaxosServerinterface alsocontains ClientHandle() and Ping().The former isa quorum call usedby clients to communicate their proposed value to the Paxos replicasand receive the decided value. Recallthat multipleclients can propose a value, possibly simultaneously, butonly one of the proposed valueswill be decided, and returned to all clients. The Ping() issimply a regular RPC call usedby thefailure detectortodetermineifareplicahasfailed.

Inthefollowing,we explainthemaincontrol ﬂowofthesingle-decreePaxosprotocol, asshowninListing2; ignoring errorhandlingandctxinitialization.OnLine3oftheProposer,thePrepare()quorumcallsendsa^Prepare^message^to theAcceptors,whomreturn^Promise^messages^back^to^theProposer.Onceaquorumofpromiseshasbeenreceived,

(12)

1 func (p *Proposer) runPaxosPhases() error {

2 preMsg := &PrepareMsg{Rnd: crnd}

3 prmMsg, err := p.config.Prepare(ctx, preMsg)

4 if prmMsg.GetVrnd() != Ignore {

5 p.cval = prmMsg.GetVval()

6 }

7 accMsg := &AcceptMsg{Rnd: crnd, Val: p.cval}

8 lrnMsg, err := p.config.Accept(ctx, accMsg)

9 ackMsg, err := p.config.Commit(ctx, lrnMsg)

10 return nil

11 }

Listing 2:Proposer’s code for Paxos phases, slightly simpliﬁed, and without error handling.

type QuorumSpec interface {

PrepareQF(replies []*PromiseMsg) (*PromiseMsg, bool) AcceptQF(replies []*LearnMsg) (*LearnMsg, bool) CommitQF(replies []*Empty) (*Empty, bool)

ClientHandleQF(replies []*Response) (*Response, bool) }

Listing 3: The^QuorumSpecinterface must be implemented to process replies.

1 type PaxosQSpec struct {

2 quorum int

3 }

4

5 func (q PaxosQSpec) PrepareQF(replies []*PromiseMsg) (*PromiseMsg,bool) {

6 if len(replies) < q.quorum {

7 return nil, false

8 }

9 reply := &PromiseMsg{Rnd: replies[0].GetRnd()}

10 for _, r := range replies {

11 if r.GetVrnd() >= reply.GetVrnd() {

12 reply.Vrnd = r.GetVrnd()

13 reply.Vval = r.GetVval()

14 }

15 }

16 return reply, true

17 }

Listing 4: ThePrepareQFprocesses^Promisereplies from replicas.

the Prepare() quorumcall returns witha single combined^Promise ^message. ^We ^explain ^later ⁱⁿ ^this^section, ^how ^we leverage Gorums’s quorum function abstraction to determine whetheror not a quorum has been received, and how to combinetherepliesintoasingle^Promise^message.

Next,theProposerdeterminesfromthe^Promiseîfânyôf^theAcceptorshavevotedinapreviousround,vrnd.If so,thecorresponding valuefromthe^Promise^message^(Line⁵⁾^that ^was^voted^for,^mustâlso^beûsed^by^theProposer whenconstructingits Âccept ^messageôn^Line^7.Ôtherwise,^theProposerusesthevalue cvalthat itreceivedfroma client.

AtthisstagetheProposerinvokestheAccept()quorumcall,askingtheAcceptorstochoosethevalue includedin the ^Accept ^message.^The Acceptors respondback witha ^Learn ^message,^followed ^by ^the Proposerinvokingthe Commit()quorumcalltopropagatethedecisiontotheLearners,whichconcludestheprotocol.

We have implemented the SinglePaxosServer interface methods on an object of type PaxosReplica, encap- sulating thestate andbehavior ofthe Paxos agents: Proposer, Acceptor, andLearner.The behavior ofeach agent correspondstodifferentCPNmodelsin§3.Further,thePaxosReplicatakescareofdispatchingthemethodcallstotheir respectivePaxosagents.

We now turn our attention to the handling of replies from quorum calls. For each quorum call deﬁned in the IDL, Gorumsaddsa quorumfunction signaturetoan interfacecalledQuorumSpec,asshowninListing3.Thisinterfacemust beimplementedbytheprotocoldeveloper;Listing4showstheimplementationofthePrepareQFquorumfunction.These methodsareimplementedonthePaxosQSpectype,whichholdsinformationaboutthequorumsize(Line2).

(13)

Fig. 15.Overview of the test framework.

PrepareQFis calledbythe Gorumsruntimewiththeset ofrepliesthat havebeenreceived sofar; itis calledonce foreachreply.Intheﬁrstpart(Lines6–8),wecheckifthereareenoughrepliestoreturnfromthequorumcall,orreturn falsetosignaltoGorumsthatwemustwaitformorereplies.

If enough replies havebeen received, we continue toconstruct a combined ^Promise ^message^by êxamining âll ^the replies, andpickingthevalue, v val, fromthe ^Promise^message^with^the ^highest^voted^round, ^vrnd. Îf^suchâ ^locked-in value isfound in thereplies, thismeans that the Proposeris constrainedand mustcontinue to use thisvalue in the remainderoftheprotocol.Otherwise,theProposerisunconstrained,andcanpickitsownclientvalue.

Similarconstructsareusedforallthemethodsinthe^QuorumSpecinterface,butwedonotshowthemhere.However,we notethatoneofthebeneﬁtsofusingGorums’squorumfunctionsisthattheyareamenabletounittesting.

5. Testcaseexecution

To performmodel-basedtesting ofourPaxos implementationdescribed in §4.2,we have implementeda clientappli- cation, which together withthe Paxos implementationand Gorumsconstitute the SUT.Fig. 15 givesan overviewof our test framework,whichconsistsofCPNTools andatestadapter.Ourtestapproach involvesthreesteps: (a) useCPNTools to constructatest modelofourSUT;(b) perform simulation-basedtestcasegeneration byusingtheMBT/CPN libraryto generatetestcaseswithoraclesrepresentedinanXMLformat;(c) implementatestadaptertoexecutethegeneratedtest casesontheSUT,andcomparethetestresultsagainstgeneratedoracles.

5.1. Thetestadapter

A central partofour test approachis the development ofa test adapterwhich can executethe systemandunit test cases generated fromCPN Tools using ourMBT/CPN library [10] (discussedin §6). The test adapter consists ofa reader and a tester, both implemented in Go. The reader of the adapter can read test cases with oracles in the XML format generated fromtheCPNtest model.The tester componenthasbeenimplementedusing thetesting package fromthe Go standard library.Go’s testinginfrastructurecomprisesthego testcommandwhichallows ustosimplyrunandexecute our generated testsandobtain pass/fail informationforeach test caseexecution. Moreover, the Go testinginfrastructure includesatoolwhichcanbeusedtoevaluateourapproachbymeasuringthestatementcoverageforbothunitandsystem tests.

5.2. Testcaseexecution

WedistinguishbetweenunitandsystemtestsforourSUT.Theunittestsareusedtotestthecentralprotocollogicused to implement the single-decreePaxos protocol, such asquorum functionsdiscussed in §4. The systemtests are used to test thecompletePaxosimplementationandGorumslibrarywithclients.Thisseparationprovidesa modularapproach to testing.Additionally,undersystemtests,weconsiderfailurescenariosforthePaxosreplicaswhenindifferentPaxosphases, cf. Fig.8.

5.2.1. Unittests

The test adapter implements a Go-based tester that can execute the unit testsobtained from the reader. The tester invokes themethods tobe testedwiththe supplied input values,anduponcompletion compares theresults againstthe

(14)

</PromiseMsg>

</PromiseMsg>

</TestValues>

</PromiseMsg>

</TestOracles>

</TestCase>

</Test>

Fig. 16.XML format for PrepareQF().

test oracle’s expectedoutput,also obtainedfromthereader. Theunit testscan be performedwithoutrunning thePaxos protocolandclients.Themethodsweconsiderforunit testsincludePrepareQF()andAcceptQF(),discussedin §3and §4.2.

Fig.16showsanexcerptfromtheXMLrepresentationofatestcaseforPrepareQF(),whichcorrespondstoatestcasewhere Paxosisconfiguredwiththreereplicasandthequorumsizeistwo.Thetest inputforthePrepareQF()methodinthetest caseis two ^Promise^messages ^with^values ^for^the^fields ^Rnd, ^{V rnd} ând ^{V val.} ^The êxpectedôutput ôf^the PrepareQF() is a ^Promise ^message^together ^with^the ^Quorum^boolean ^true,îndicating ^that â ^quorum^was ôbtained^for ^theseînput messages.

5.2.2. Systemtests

ExecutionofthesystemtestsrequiresthatthePaxosreplicasarerunningandreadytohandletherequestsfromclients sothatwecantestthecompletesystemincludingtheGorumslibrary.

Therefore,forsystemtests,thetesterﬁrststartsthePaxosreplicasandtheniteratesthroughthetestcasesobtainedfrom thereader.Foreachtestcase,thetesterstartsclientsinordertosendclientrequeststothePaxosreplicas.Eachclienthas asinglerequestvaluetosendforconsensus.Asanexample,thetest adaptercanexecutetwoclientsconcurrentlytosend theirrequeststothePaxosreplicas.AfterthePaxosreplicashavedecided,aresponsevalueissentbacktotheclients.The testercheckswhethertheresponseforeachclientbelongstotheexpectedresponses (oracles)andwhethertheresponses arethesameforallclients,i.e.,theconsensuswasreached.

In addition to testing success scenarios, we also test scenarios with differenttypes offailures. This includes forcing the failure detector to timeout, triggering a new leader to be promoted. In this way, we can test leader changes and faulttolerance ofthePaxosprotocol. Tomaketheimplementationamenableforsuchfailure scenariosduring systemtest execution, our test adapter must be able to observe the messages exchanged between thereplicas, andto interfere, for example,inatestcasewherewesimulatealostmessageortriggeratimeout.

Wehaveconsideredthreemajorharnessingapproachesbelowforhowwecaneffectivelytestaparticularscenario,and wemotivateourﬁnalchoice.Furtherdetailsontheﬁrsttwoapproachesandtheirprosandconscanbefoundin [31].

In the ﬁrst approach, one would isolate the involved (Unix)processes in individual, networked, containers or virtual machines, andifnecessaryinterferewiththeenvironmentby,e.g.,introducing networkpartitions.Thisisaheavy-weight approach, wherea lotof implementationeffort willhave to be spent on manipulatingthe environment basedon a test casedescription.Also, thetest caseadapter coordinatingtheenvironment needsan understanding ofthemessagesto be exchangedbetweenreplicas,sothatitcandecidethataparticularsetuphasnowbeenreachedanditshouldinterfere.

Thesecondapproachismorelight-weightinthatthePaxosreplicaswouldconnecttothetestadapterinsteadofdirectly to each other. The test adapter can then observe the protocol and either relay message, or introduce faults [32]. This approach can reusemarshaling logicin the test adapter,which makes analyzing themessage content easierthan inthe virtualmachineapproachabove.

Ourapproachisevenmorelight-weightinthatwe donotuseanexternal testadapter.Instead,totrackthestateofa replica, wecompile an instrumentedversion of theserver that contains severalpoints fortest caseinteraction.Byusing thisapproach,wecan usetestcasestodescribe notonlythe successfulscenarios, butalso differentfailure scenarios and guidethetest caseexecution. As anexample,considera Paxosconfigurationwiththreereplicas. Atestcasemaycontain eventsthatcausetheleadertofailduring eitherthefirstorthesecondphaseofthePaxosprotocol.Aftersuchafailure,a newleaderwilleventuallyemerge,restartingthePaxosphases.Inaconfigurationwithfivereplicas,atestcasecan,e.g.,be

(15)

</TestValues>

</TestOracles>

</TestCase>

</Test>

Fig. 17.XML format for testing a three-way replicated Paxos system.

configuredtoletthefirstleaderfailinthefirstphase,andafterthesecondleaderemergesandthePaxosphasesrestart,the second leadercanbemadetofailinthesecondphase.Finally,thethirdleadercanrestartandcompletethePaxosphases successfully.

Toenable the testadapterto knowwhenit ispossibletoinject afailure, wehaveinstrumented theProposerwith an AdapterConnectortocommunicatetheProposer’sstate,suchasthecurrentleaderandwhichPaxosphaseshave completed,tothetestadapter.Moreover,betweeneachstatechange,theProposerwillwaitforadecisionfromthetest adaptertodetermineifthecurrentPaxosphaseshouldfail,e.g.triggering aleaderfailure.Thedecisionsmadeby thetest adapterregardingfailuresofthePaxos phasesareconfiguredforeachtestcaseintheXMLfile.Fig.17showsanexample ofatestcaseforthePaxosprotocolwiththreereplicas,wherethereisafailureinthefirstPaxosphase.Thetestinputfor thisexampleconsistsoftwo clientssendingrequestsconcurrently tothePaxosreplicas. Thetestoraclesincludethelegal responsesfromPaxosreplicas,andtheexpectedleaders.Leader0isthefirstleader,andafteritfails,leader1becomesthe new leader.Thetest adapter checkswhetherthe correctleadersare chosen, andwhethertheresponse returned toeach client belongs to theset of legal responses. Furthermore,it also testswhetherthe responses obtainedby all clients are equal,sothatwecandetermineiftheyhavereachedconsensus.

6. Modelvalidationandtestcasegeneration

ForthetestcasegenerationwerelyontheMBT/CPNlibrary [10],whichwehavedevelopedasanextensiontoCPNTools.

The MBT/CPNlibraryisbasedon extractingtest casesfromexecutionsequences oftheCPNmodelbypartially observing occurring events. MBT/CPN supports both state space and simulation-based test case generation. State space-basedtest casegenerationworksforﬁnite-statemodelsandisbasedoncomputingallreachablestateandstate changesoftheCPN model.Simulation-based testcasegenerationis basedonrunning asetofsimulations andextractingtestcases fromthe correspondingsetofexecutions.

The CPN test modelfor thePaxos protocol hasan infinite state spaceandalso forrestricted andrepresentative configurations withafinite statespace, state-basedtest casegenerationisinfeasibledueto thestate explosionproblem. We thereforeonlyusestatespaceforvalidatingtheCPNmodelforsmallconfigurations(see§6.1)inordertogainconfidencein thecorrectnessofthetestgenerationCPNmodel.Forthetestcasegenerationitself,werelyonsimulation-basedtestcase generationduetothehighcomplexityofthePaxosprotocol.

6.1. Modelvalidation

AdistinctadvantageofrelyingonformalmodelssuchasCPNsfortestcasegenerationisthatrestrictedconfigurationsof thetestcasegenerationmodelwithafinitestatespacecanbeverifiedusingmodelcheckingpriortotestcasegeneration.

Thiscanbe usedtoincrease conﬁdenceinthecorrectnessofthetest casegenerationmodelandthegeneratedtestcases.

ToobtainconfigurationsofthePaxosCPNtestgenerationmodelwithafinitestatespace,wehaveboundedthebehaviorof thePaxosagentrolessuchthatonlyafinitenumberofmessagescanbegeneratedinthesystem.

Specifically, we considerconfigurations ofourCPN modelwithtwo clients,where eachclient cansend oneclient re- questmessage(modeledasastring) intothePaxossystem.Thesetworequestmessagescanbesentinanyorder,andthe Paxossystemthenmakesadecisiononwhichclientrequestmessageshouldbechosenandhandled.Themodelterminates when bothclientshavereceivedthedecisionresponsefromthePaxossystem. ForthePaxos agentroles, wehavelimited thenumberofmessageswhenexecutingthePaxosphasesbyconfiguringan upperbound ofoneonthenumberoftime- outs/failures. Thisisdoneby meansofplaceFDControldiscussed in§3.1andshowninFig.8.Themostcomplexscenario currentlycoverediswherethefirstPaxosphasefailsonce,thenthePaxossystemrestartsthefirstphase;butthistimethe second phase failsonce andthePaxossystemrestarts again,andthen Paxoscompletes successfullyforboth phases. This scenarioinvolvestheProposer(leader)sendingthe^Prepare^message^three^times,^theÂccept^message^two^times,ând the^Commit^messageônce.

(16)

In other words, we explicitlymodel failure scenarios wheremessages timeout orget lost in particularphases ofthe protocol,andcombinationsthereof.AftertheassociatedrestartsofthePaxosprotocolinthepresenceofthesefailures,the modelletstheruncompletesuccessfullywithoutfurthererrors.

We have used the model checker and ASK-CTL library available in CPN Tools to verify that the CPN model (in the restricted conﬁgurations) satisﬁes the correctness properties S1–S3 and L1–L2 asformulated in §2. The ASK-CTL library makesit possibletospecifytemporalpropertiesinastate andevent-orientedvariantofthecomputation treelogic (CTL).

Belowwe showhowthebehavioralpropertiescan bespeciﬁedinCTLrelative tothedevelopedtestcasegenerationCPN model. We use M(p) to denote the marking (multi-set of tokens) on a place p in the marking (state) M. For a token (value)t,weuset∈^M(p)todenotethatt isatokenonplacepinthemarkingM.

S1 Only a proposed value may be chosen: TocheckthispropertyweconsidertheplaceServerResponseinFig.2.Proposed valuesarerepresentedastokens onplaceClientRequestintheinitial marking(state),andthechosen consensus valuewillappearasatokenonplaceServerResponse.ThepropertycanthereforebeformulatedinCTLas:

AG

(

t

∈

^M

(

ServerResponse

) ⇒

^t

∈

^M0

(

ClientRequest

))

S2 Only a single value is chosen: As anychosenvalue willappear asa tokenonplace ServerResponsewecan verifythis property by checking that there is at mostone token on this place in anyreachable state. In CTL this can be formulatedas:

AG

(|

^M

(

ServerResponse

)| ≤

¹

)

S3 Only a chosen value may be learned by a correct replica: Weconsider thetokens onAcceptorState (Fig. 9) ofthe form (r,rnd,vrnd,v)wherethefirstcomponentspecifiesthereplicaandthelastcomponentspecifiesthechosenvalue.

The value learnedby eachreplica will appearastokens on placeResponse (Fig. 3), where thefirst component specifiesthe replicaandthesecond componentspecifiesthe learnedvalue.Toaccount onlyforcorrectreplicas, weconsiderthefusionplaceFailedReplica(Fig.8)andrestrictthepropertytoreplicasnot presentonthisplace.

ThepropertycanthereforebecheckedusingthefollowingCTLformulawhereRdenotesthesetofreplicas:

AG

(∀

^r

∈

^R

\

^M

(

FailedReplica

) :

(

r

,

v

) ∈

^M

(

Response

) ⇒ ∃(

^r

,

rnd

,

vrnd

,

v

) ∈

^M

(

AcceptorState

))

L1 Some proposed value is eventually chosen: Forthispropertywecancheckthateventuallyatokenwillbeputonplace ServerResponse.InCTLthiscanbeformulatedas:

AG AF

(

M

(

ServerResponse

) = ∅ )

L2 Once a value is chosen, correct replicas eventually learn it: We consider the place AcceptorState holding any chosen value,andcheckthatthisvalueiseventuallylearnedbynon-failingreplicasbyconsideringtheplaceResponsein Fig.3.InCTLthispropertycanbeformulatedas:

AG

( ∃ (

r

,

rnd

,

vrnd

,

v

) ∈

^M

(

AcceptorState

) ⇒

AF

( ∀

^r

∈

^R

\

^M

(

FailedReplica

) : (

r

,

v

) ∈

^M

(

Response

))

We haveexecuted the above queries against the test casegeneration CPNmodel configured withtwo replicaswhich yields a relatively smallstate spacewith lessthan 2000 states.In the process of checkingthese properties we found a number ofminor modeling errors that we were then able to correct.In particular, we use the support inCPN Tools to obtain errortraces (incase a propertywas violated) whichhelped inidentifying the source ofthe problem. Evenifthe Paxosmodelistoocomplextoconductmodelcheckingforlargerconfigurations(duetothestatespacesize),beingableto verifythemodelforsmallerconfigurationsincreasestheconfidenceinthecorrectnessofourtestcasegenerationforlarger configurationsofthePaxosprotocol.

6.2. Testcasespeciﬁcation

Test case generation from the CPN model requires identiﬁcation of observableevents originating fromoccurrences of transitions.Atestcaseiscomprisedofobservableevents,wheretheinputeventsrepresentstimulitothesystemandthe outputeventsrepresenttheexpectedoutputsused astest oraclesto determinethepass/failureofa testcase. Theformal foundation usedto checkwhetherthe executionof theSUTconformstothe speciﬁcationasprovided bythe testcaseis hencebasedontraceequivalence.

ThegenerationoftestcaseswithMBT/CPNrequiresanimplementationofatestcasespeciﬁcationdeﬁnedbytheStandard MLsignature(interface)showninListing5.

(17)

signature TCSPEC = sig

val detection : Bind.Elem -> bool;

val observation : Bind.Elem -> TCEvent list;

val format : TCEvent -> string end;

Listing 5: Signature for test case speciﬁcation.

fun detection (Bind.DecidedValue’Request _) = true

| detection (Bind.DecidedValue’Apply_RequestQF _) = true

| detection (Bind.PhaseOne’Process_PromiseMsg _) = true

| detection (Bind.PhaseTwo’Process_LearnMsg _) = true

| detection _ = false;

exception obsExn;

fun observation (Bind.DecidedValue’Request (_,b)) = [InEvent (SYS_Propose (#value b)]

| observation (Bind.DecidedValue’Apply_RequestQF (_,b) = [OutEvent (SYS_Decide (#value b))]

| observation (Bind.PhaseOne’Process_PromiseMsg (_,b) = [InEvent (SYS_P1Failure (#crnd b))]

| observation (Bind.PhaseTwo’Process_LearnMsg (_,b) = [InEvent (SYS_P2Failure (#rnd b)))]

| observation _ = raise obsExn;

Listing 6: Implementation of test case speciﬁcation for system level tests.

The typeBind.Elemisanexistingdatatype inCPNTools representingbindingelements,i.e.,a transitionandanas- signment of valuesto the variables of the transition. The type TCEvent is the type deﬁnedfor observable events. The detectionfunctionis a predicateon bindingelements that evaluates to true forbinding elements representingobservable events.The purposeoftheobservationfunctionisto mapan observable bindingelementinto anobservable inputorout- put eventbelonging to the TCEventtype. The observation function mayreturn a listof observable eventsin caseone mightwanttosplitabindingelementintoseveralobservableeventsinthetestcase.Finally,theformattingfunctionmaps observableeventsintoastringrepresentationwhichisusedinordertoexportthetestcasesintoﬁles.

ForthePaxosprotocolwegeneratedbothsystemtestandunittests.Thesystemleveltestisconcernedwiththeproposed values,chosenvalue,selectedleaders,andfailureofreplicas.Theunittestareconcernedwithtestingthequorumfunctions, which forms the coreof the Gorums-basedimplementation.Listing 6 showsa slightlysimpliﬁed implementation of the detectionandobservationfunctionforsystemleveltests.WeomittheformattingfunctionastheXMLformatfortestcases isalreadydescribedin§5.2.

The first two binding elements for which the detection function returns true correspond to events representing the proposalandchoiceofavalue.Thetwonextbindingelementscorrespondtoeventsrepresentingreplicafailures.Theobser- vation functionthengeneratestheobservableevents,whichcanbeeitheranInEventrepresentingstimulitothesystem oranOutEventrepresentingexpectedoutputs.Theimplementationofthetestcasespecificationforunittestscoversthe prepare,accept,andcommitquorumfunctionsandtheimplementationissimilartothesystemtestcasespecification.

6.3. Experimentalresultsonstatementcoverage

We have used statement coverage to evaluate the quality of our test casegeneration. Severalother metrics exist to assess test coverage, but currentlyonly statement coverage is supported by the Go tool chain.Table 1 summarizes the experimentalresultsobtainedusingsimulation-basedtestcasegenerationforthePaxosprotocol.WehaveconsideredPaxos conﬁgurationswith3and5replicasandgenerated1,2,5and10simulationrunsoftheCPNmodel.Aswedidnotseeany increaseinthenumberoftestcasesbygoingfrom5to10simulations,wedidnotincreasethenumberofsimulationruns further. The table shows thecoverage obtainedforthe differentsubsystems ofour Paxos implementation.Note that the Unittestsareforthequorumfunctionsandhencenotapplicablefortheothersubsystems.Thetwonumberswrittenbelow SystemtestsandUnittestsgivesthe totalnumberof testcases generatedfor3and5replica conﬁgurations, respectively.

The testcasegenerationforeach conﬁgurationconsideredtook lessthan 10seconds,andtheexecutionofeach testcase tooklessthanoneminute.

Theresultsshowthat,fortheconﬁgurationwithboth3and5replicas,thestatementcoverageofunittestsforPrepare andAcceptquorumfunctionsareupto90%and85.7%,respectively.Forthesystemtests,thestatementcoverageforPrepare, Accept and Commit quorum calls reaches 83.9%, respectively; the results of statement coverage for Prepare and Accept quorumfunctionsareupto100%;forthePaxosimplementation(Paxoscoreinthetable),theProposermodule’sstatement coverage reaches 97.4%; the statement coverage of the Acceptor module is up to 100%; the statement coverages of the Failure Detector and Leader Detector modules reach 75.0% and 91.4%, respectively; the statement coverage of the Paxos replicamodule(discussedin§4.2)reaches91.4%;fortheGorumslibraryasawhole,thehigheststatementcoveragereaches 51.8%. The results and test cases considered above validate that the implementation of the single-decree Paxos system andtheGorumsframeworkwork inbothcorrectscenariosandscenarios involvingfailuresofreplicas. Thereasonforthe lower coverage results ofthe Gorumslibrary is that Gorums contains code generated by Gorums’s code generator, and among them, various auxiliary functionsanderror handlingcode that are not used by our currentimplementation.The total number oflines of codefor the SUTis approximately3890 lines,which includegenerated code by Gorums’s code

(18)

Table 1

Experimentalresultsfortestcasegenerationandexecution.

Subsystem Component System tests Unit tests

Test cases for 3/5 replicas

15/38 74/424

Coverage

Gorums library 51.8% –

Paxos core Proposer 97.4% –

Acceptor 100.0% –

Failure Detector 75.0% –

Leader Detector 91.4% –

Replica 91.4% –

Quorum calls Prepare 83.9% –

Accept 83.9% –

Commit 83.9% –

Quorum functions Prepare 100.0% 90.0%

Accept 100.0% 85.7%

generator(around3150lines),thecodeforPaxosreplica(around110lines),theclientcode(around80lines),theProposer code(around170lines),theAcceptorcode(around40lines),thecodeforfailuredetector(around170lines),thecodefor leaderdetector(around100lines),andthecodeforquorumfunctions(around70lines).

Aspartofanalyzingthetestresultsandexecutinggeneratedtestcases,wehavediscoveredbugsintheimplementation of the Paxos protocol, which are not capturedby usingmanually written table-driventests inGo. We havefound bugs relatedto:theleader detectorelectsawrongleader;onlytheleader’sfailure detectorisexecuted;theelectednewleader obtainsawrongroundnumber;clientscannotreceiveresponsesfromthePaxosreplicas;thePaxossystemcanonlyhandle onerequestfromoneclient;andafterthecurrentleaderfails,thefailedleaderexecutesthePaxosphasesagain.Thisshows howourMBTapproachisabletodetectnon-trivialprogrammingerrorsincomplexdistributedsystemsprotocols.

7. Relatedwork

Chubby [33] wasoneoftheﬁrst implementationsofPaxosthatwere deployedina productionenvironment,andthus wereextensivelytested. Theauthorshighlightthat atthetime (2007),itwas unrealistictoprovecorrectarealsystemof thatsize.Thustoachieverobustness,theyadoptedmeticuloussoftwareengineeringpractices,andtestedtheirsystemthor- oughly.Oneoftheirtestingstrategieswas totesttheirimplementationwhensubjectedtoarandomsequenceofnetwork outages,messagedelays,timeouts,processcrashesandrecoveries,scheduleinterleavings,andsoon.UsingourCPNmodel andourgeneratedtests,weaimtotestmanyofthesameattributesinamoresystematicmanner.

ModbatisanMBTtoolimplementedinScalaandhencecompatiblewithJavabytecode-basedapplications [34].Models are specified asannotated, non-deterministic extended finite state machines. Modbatexplores the transitionsystemand executesthecallsspecifiedonthe transitions.It hasbeenusedsuccessfullyinasimilar settingasourson theZooKeeper distributedcoordinationservice.Itexploresdifferentpossibleinterleavingsandnon-deterministicoutcomesduetoschedul- ingdecisionsornetworkcommunicationintherealsystemwhicharejudgedbyanoracleessentiallyimplementingamodel checkingcomponent.UnlikeourCPNmodels,thespecificationsarenotforconsumptionbyothertoolssuchasmodelcheck- ers,noristhereaninteractivecomponentthatallowsexploringaparticularexecutionofthemodel.Asinourapproach,it requiressomemanualeffortconnectingtheenginetotheSUT.

AtestingapproachfortrueconcurrencyusingI/OPetrinetshasbeendiscussedbyPoncedeLeónet al. [35].Theauthors deﬁne a concurrent conformance relation for input–output labeled transitions systems, IOLTS. They present a test case selectionalgorithmusingcriteriasuchasallpathsoflengthn,ortraversingeachbasicbehavioracertainnumberoftimes.

Sincetestcaseselectionisalsoachallengeinoursetting,itremainsanopenquestionhowtheirunfoldingswouldworkin ourCPNsetting.

MBThasbeenusedwithsuccess(asmeasuredthroughproductivitygain)inMicrosoft’sProtocolDocumentationQuality AssuranceProcess.Grieskampet al. [31] usedSpec Exploreronprotocols,whereaso-calledmodelprogram describesthe testcase,includinghowtocheck anobservationagainstapossiblynon-deterministicoutcome.Themaindifferencetoour work isthat their modelprograms are rule-based,andassuch onlyget avisual representationasa graphthrough state spaceexploration.OurCPNmodels givedevelopersa betteroverviewasthey directlylinkclient- andserverinteractions.

Spec Explorerusesthecoordination languageCordforslicingmodelsintotractable subsetsoftest casesthatmayimpact coverage andcompleteness,butnot correctness.Wehave notyet tackledtheissueoftest caseselection,relying on user interactionthroughsimulationwhenstatespaceexplorationbecomesinfeasible.

A CPN-based test generation approach is proposed by Liu et al. [6]. This approach requires defining a conformance testing-orientedCPN(CT-CPN)modelandaPN-iocorelationwhichspecifieshowanimplementationconformstoitsspec- ifications. Furthermore,thisapproach usessimulation-based testcasegeneration algorithm fortheCT-CPN model.Inour