Modelling Real-time Database Systems in Duration Calculus

In this paper, we give a formal model for real-time database systems using Duration Calculus. Our model supports the formal reasoning about the operations in the systems. As a case study for our technique, we give a formal specification and verification of

ModellingReal-timeDatabaseSystemsinDurationCalculus

DangVanHungandHoVanHuong

UnitedNationsUniversity

InternationalInstituteforSoftwareTechnology

P.O.Box3058,Macao

ABSTRACT

Inthispaper,wegiveaformalmodelforreal-timedatabasesystemsusingDurationCalculus.Ourmodelsupportstheformalreasoningabouttheoperationsinthesystems.Asacasestudyforourtechnique,wegiveaformalspeci cationandveri cationoftheRead/WritePriorityCeilingProtocol(R/WPCP).

KEYWORDS

Real-timeDatabase,ConcurrencyControl,DurationCal-culus.

1Introduction

Real-timeDatabaseSystems(RTDBS)havebeenusedinawiderangeofapplicationssuchasairtraf ccontrol,roboticsandnuclearpowerplants.ResearchonRTDBShasreceivedagreatdealofattention[1,4],andbelongstotwodifferentimportantareasinComputerScience:ually,transactionsinRTDBSareassociatedwithtimeconstraints,e.g.dead-line.TheconcurrencycontrolinRealTimeDatabaseSys-temshastoensurenotonlytheconsistencyofthedatainthemulti-userenvironmentslikeintraditionaldatabases,butalsothetemporalconsistencyofthedata,andthatalltransactionsmeettheirdeadline.Therefore,theconcur-rencycontrolinRealTimeDatabaseSystems(RTDBS)ismuchmorecomplicatedthantheoneintraditionaldatabasesystems(DBS).Aformaltechniqueformodellingandrea-soningaboutthebehaviouroftheconcurrencycontrolwillsupporttheanalysisandveri cationofconcurrencycon-trolalgorithms.Inthispaper,wefocusonthedevelopmentofsuchamathematicalmodelofRTDBS.Inparticular,wefocusontheformalisationoftheintegrationoftheconcur-rencycontrolwithschedulinginRTDBS.WeuseDurationCalculus(DC)introducedbyZhou,HoareandRavnin[6]asalogicalfoundationforourapproach.ThereasonforthischoiceisthatDCisasimpleandpowerfullogicforreasoningaboutthetimedurations,whichisamaincon-ceptinscheduling.

Ourapproachissummarisedasfollows.We rstex-tendtheformalmodelofRTDBSproposedin[5]withthecapacityformodelling(iterated)periodictransactionsystems.Handlingtheperiodictransactionsystemswithdeadlineisnottrivial.Then,wegiveaformalspeci ca-tionofthecorrectnesscriteriaforconcurrencycontrolin

RTDBSwhichconsistsoftheserializability,thetemporalconsistencyandmeetingtimingconstraints.Toshowtheadvantagesofourmodel,wegiveaformalspeci cationandveri cationoftheRead/WritePriorityCeilingProto-col(R/WPCP).

2DurationCalculus

DurationCalculus(DC)isalogicalapproachtoformalde-signofrealtimesystems.DCadoptscontinuoustimeandusesboolean-valuedfunctionsovertimetomodelstatesandeventsoftherealtimesystems.Thedurationofastateoveratimeintervalistheaccumulatedpresencetimeofthestateovertheinterval.Wereferto[3]formorecomprehen-siveintroductiontoDC..

TimeinDCisthesetR+ofnon-negativerealnum-bers.Fort,t ∈R+,t≤t ,[t,t ]denotesthetimeintervalfromttot .LetIntvdenotethesetofallintervals.

DChasasetEofbooleanstatevariables.EincludestheBooleanconstants0and1denotingfalseandtruerespectively.Stateexpressions,denotedbyP,Q,P1,Q1,etc.,arebuiltfrombooleanstatevariablesusingbooleanconnectives.AstatevariablePisinterpretedasafunctionI(P):R+→{0,1}(astate).I(P)(t)=1meansthatstatePispresentattimeinstantt,andI(P)(t)=0meansthatstatePisnotpresentattimeinstantt.Weassumethatastatehasthe nitevariabilityina nitetimeinter-val.Astateexpressionisinterpretedasafunctionwhichisde nedintheobviouswayfromtheinterpretationsforthestatevariablesandBooleanoperators.

ForanarbitrarystateexpressionP,thedurationofPisdenotedby

P.GivenaninterpretationIofstatevari-ables

andaninterval[t,t],durationPisinterpretedast I(P)(t)dt. 1alwaysgivesthelengthoftheandt

intervalsisdenotedby .Anarithmeticexpressionbuiltfromstatedurationsandrealconstantsiscalledaterm.

WealsoassumeasetoftemporalpropositionalletterX,Y,...EachtemporalpropositionalletterisinterpretedbyIastruth-valuedfunctionsoftimeintervals.

AprimitivedurationformulaiseitheratemporalpropositionalletteroraBooleanexpressionformedfromtermsbyusingtheusualrelationaloperationsonthereals,suchasequality=andinequality<.Adurationformulaiseitheraprimitiveformulaoranexpressionformedfromotherformulasbyusingthelogicaloperators¬,∧,∨, , ,andthechop;.

In this paper, we give a formal model for real-time database systems using Duration Calculus. Our model supports the formal reasoning about the operations in the systems. As a case study for our technique, we give a formal specification and verification of

AdurationformulaDissatis edbyaninterpretationIinaninterval[t ,t ]justwhenitevaluatestotrueforthatinterpretationoverthattimeinterval.

GivenaninterpretationI,thechop-formulaD1;D2istruefor[t ,t ]iffthereexistsatsuchthatt ≤t≤t andD1andD2aretruefor[t ,t]and[t,t ]respectively.

Wegivenowshorthandsforsomedurationformulaswhichareoftenused.ForanarbitrarystatevariableP, P standsfor(

P= )∧( >0).Thismeansthatintervalisanon-pointintervalandPholdsalmostevery-whereinit.WhenPininterpretedasaone-sidecontin-uousfunction, P meansthattheintervalisanon-pointintervalandPholdseverywhereinit.Weuse todenotethepredicatewhichistrueonlyforpointintervals.Modali-ties3,2arede nedas:3D= true;D;true,2D= ¬3¬D.Thismeansthat3DistrueforanintervaliffDholdsforsomesubintervalofit,and2DistrueforanintervaliffDholdsforallsubintervalsofit.Wewillusetheabbreviation P = ∨ P

Wereferthereadersto[3]forapowerfulproofsystemforDCwhichiscompletefortheabstracttimedomain.

3FormalModelofRealTimeDatabaseSys-temsinDC3.1

Basicmodel

Letareal-timedatabasesystemconsistofasetOofdataobjects(rangedoverbyx,y,z,...),andasetTofntrans-actionsTi,1≤i≤n.

EachtransactionTiarrivesattheDBsystemperiodi-callywiththeperiodPi.Inaperiod,atransactionperformssomereadoperationsonsomedataobjects,doessomelo-calcomputationsandthenperformssomewriteoperationsonsomedataobjects.Weassumetheatomiccommitmentoftransactions:ifatransactionhasbeenabortedthenit’sexecutionhasnoeffectsonthedatabase.Wealsoassumethateachtransactioncanreadandwritetoadataobjectatmostonceduringitsexecutioninoneperiod.Theseas-sumptionsareforthesimplicityandwellacceptedintheliterature.EachtransactionTi,besidesitsperiodPi,alsohasitsowndeadlineDi,aprioritypi,anexecutiontimeCi,adatareadsetROiandadatawritesetWOi(ROiand/orWOimaybeempty).

Letxbeadataobject.Foreachi≤nletTi.wrtn(x)beaDCstatevariableexpressingthebehaviourofx.Ti.wrtn(x)holdsattimetiffthevalueofxattistheonewrittenbytransactionTi.TheviewofTionxcanbemodelledasastatevariableTi.read(x)de nedasfol-lows.Ti.read(x)holdsattimetwithinaperiodiffTihasperformedareadoperationonxsuccessfullybeforetinthatperiod.Therefore,thereadoperationonxinaperiodisperformedatthetimethatTi.read(x)changesitsvaluefrom0to1inthatperiod.Toexpressthatatimeinterval[a,b]isaperiodofTi,weintroducetemporalpropositionalletterTi.priod.Ti.period([a,b])=trueiff[a,b]isape-

riodofTi.Ofcourse,

Ti.period =Pi.

(1)

Foreachi≤nstatevariableTi.arrdisintroducedtoexpressthatTiisstandinginthesystemattimet:Ti.arrd(t)=1iffattimettransactionTiisinthesystemandhasnotbeencommittedorabortedsincethen.BecauseweassumethatTiarrivesatthebeginningofanyperiodofits,itholds:

Ti.period Ti.arrd true

(2)

WeintroducevariablesTi.req(x)andTi.req(x)toexpressthatTiisrequestinglockforadataobjectxattimet:Ti.req(x)(t)=1ifftransactionTiisrequest-ingaread-lockonxattimet,andTi.reqwlk(x)(t)=1ifftransactionTiisrequestingawrite-lockonxattimet.

WhenatransactionTirequestsalockondataobjectx,itmaybegrantedorhastowait.Therefore,foreachi≤nandforeachx,weintroducethestatevariablesTi.wt(x)andTi.wt(x)as:Ti.wt(x)(t)=1ifftransactionTiiswaitingforaread-lockondataob-jectxattimet,Ti.wtwlk(x)(t)=1ifftransactionTiiswaitingforawrite-lockondataobjectxattimet,Ti.hldrlk(x)(t)=1iffattimettransactionTiholdsaread-lockondataobjectx,andTi.hldwlk(x)(t)=1iffattimettransactionTiholdsawrite-lockondataobjectx.

Inaperiod,atransactioncancommitorabort.There-fore,foreachi≤tdandTi.abdareintroducedtoexpressthatTihasalreadycommittedorabortedattimet:td(t)=1iffTihascommit-tedsuccessfullybeforetinaperiodofcontainingt,andTi.abd(t)=1iffTihasabortedbeforetinaperiodofcontainingt.

Atthebeginningofaperiod,alltransactionshavenotreadanythingfromthedatabase.

2(T

i.period ( ¬Ti.read(x) ;true))(3)

x∈ROi

ForanytransactionTi,atanytime,tdorTi.abd(hereweassumethatatthebeginning,ifatransactionhasnotarrived,itiscommitted)

2 Ti.arrd∨td∨Ti.abd (4)

Thesethreestatesaremutuallyexclusive:

2 Ti.arrd ¬(td∨Ti.abd) (5)2 td

¬(Ti.arrd∨Ti.abd)

(6)2 Ti.abd ¬(Ti.arrd∨td) (7)

Atanytimethevalueofadataobjectisgivenbyoneandonlyonetransaction(hereweassumethatthereisavirtualtransactiontowritetheinitialvalueforalldata):

2 Ti.wrtn(x) (8)

Ti∈T

2

¬(Tj.wrtn(x)∧Ti.wrtn(x) (9)

Ti=Tj∈T

In this paper, we give a formal model for real-time database systems using Duration Calculus. Our model supports the formal reasoning about the operations in the systems. As a case study for our technique, we give a formal specification and verification of

AtransactionTirequestsalockforadataobjectxiffitisinstate“arrived”anditiseitherholdingitorwaitingforit:

2 Ti.req(x) (Ti.arrd∧

(Ti.hldrlk(x)∨Ti.wtrlk(x)))

(10)

2

Ti.req(x) (Ti.arrd∧

(Ti.hldwlk(x)∨Ti.wtwlk(x)))

(11)

Atransactioncannotholdalockandatthesametimewaitforit:

2 ¬(Ti.hld(x)∧Ti.wt(x)) (12)2 ¬(Ti.hld(x)∧Ti.wt(x))

(13)

Thecon ictinglockscannotbesharedbytransactions.Therefore,forTi=Tj

2 ¬(Ti.hld(x)∧Tj.hld(x)) (14)2 ¬(Ti.hld(x)∧Tj.hld(x))

(15)

Atransactioncanreadorwriteonadataobjectxonlyifitholdsthecorrespondinglockonthedataobjectxatthetime:

2 ¬Ti.read(x) ; Ti.read(x)

3 Ti.hld(x) (16)

2 ¬Ti.wrtn(x) ; Ti.wrtn(x)

3 Ti.hld(x)

(17)

Inanyperiod,atransactionTicannotholdalockforadataobjectsxafterithasreleasedthislock:

Ti.period ¬3( Ti.hld(x) ;

¬Ti.hldrlk(x) ; Ti.hldrlk(x) )(18)

Ti.period ¬3( Ti.hld(x) ;

¬Ti.hldwlk(x) ; Ti.hldwlk(x) )

(19)

Asmentionedearlier,foreachperiod,foralliandxthestateTi.read(x),tdandTi.abdcanchangeatmostonce.

Ti.period

(20)

2( Ti.read(x) ;true Ti.read(x) )Ti.period

2( td ;true td )(21)

Ti.period

2( Ti.abd ;true Ti.abd )

(22)

Fromtheassumptionofatomiccommitmentitfol-lowsthatifatransactionhaswrittensomethingintothedatabasethenitshouldcommitattheend.

Ti.period (23)

((3 Ti.wrtn(x) ) true; td )LetENVbethesetoftheformulas(1),(2),(4),...,(24)withx∈O,i=jandi,j≤n.

LetstatevariableTi.runbede nedasTi.run(t)=1ifftransactionTiisrunningonaprocessorattimet.WhenatransactionTihasarrivedandgotalldataobjectlocksitneeds,itisreadytorunontheproces-sor.Ti.ready(t)=1ifftransactionTiisreadytoex-ecuteonaprocessorattimet.WhenatransactionTiisready,itmustnotwaitforaread-lockorawrite-lock: Ti.ready ¬Ti.wtrlk(x) and Ti.ready ¬Ti.wt(x) .Atransactionrunsonlyifitisready.ThereforeforeverytransactionTi(A1):

2( Ti.run Ti.ready )

Inaperiodifatransactionisstanding,themaximalrequiredexecutiontimehasnotbeenreached.Hence,(A2):

Ti.period

(true; ¬td ;true (

Ti.Run<Ci); ¬td ;true)InaperiodifexecutiontimeofTiisequaltoCi,Ti

willcommitfromthattime(A3):

Ti.period

(

Ti.run=Ci; >0 true; td ))AssumethatthetransactionsT1,...,Tnshareasin-gleprocessor,andtransactionprioritiesareassignedbytheRateMonotonicAlgorithm,whichassignsahigherprioritytoatransactionwithshorterperiod.Withoutthelossofthegenerality,weassumeP1≤P2≤···≤Pn,andprioritiesareindecreasingorderfromp1topn,wherepidenotethepriorityofTi.

Atanytimeifonetransactionisrunning,anyothertransactioncannotberunning:Fori=j

(A4)

2 ¬(Ti.run∧Tj.run)

Theprocessorcannotstayidlewhenatransactionisready:

(A5)2( T

i.ready 1≤j≤nTj.run )Atransactionwithlowerprioritycannotberunningwhenatransactionwithhigherpriorityisready:

(A6)2( T

i.ready i<j≤n ¬Tj.run )Theconjunctionoftheprecedingformulas(A1)–(A6)cap-turesouruniprocessormodelforthetransactions.

3.2CorrectnessCriteriaofConcurrentExe-cutionofTransactionSystems3.2.1

Serializability

Theserializabilityofanexecutionofthetransactionsystemsaysthattherelation‘before’betweentheexecutionsoftransactionsde nedbytheorderofthecon ictoperationsintheexecutionisapartialorderingonthe(in nite)setof

In this paper, we give a formal model for real-time database systems using Duration Calculus. Our model supports the formal reasoning about the operations in the systems. As a case study for our technique, we give a formal specification and verification of

transactionexecutions.Givenanexecutionofthetransac-tionsystem,anytransactionhasitsownperiod,andineachperiod,thereisoneexecutionofthetransaction.Hence,thesetofalltheexecutionsoftransactionsisin nite.Wehavetotodescribeacriterionforthein niterelation‘before’tobeacyclicbyjustaformula.

Thereisanicecharacterisationfortherelation‘be-fore’ofthetransactionsystemtobeacyclicwhichisaboutthebehaviouroftransactionsysteminanintervalwiththelength(n+1) ly,weprovethattherelation‘before’ofasystemexecutionisacyclicifandonlyifforanyintervalwhichconsistsofexactly(n+1)consecutiveperiodsofTn,itsrestrictiononthetransactionexecutionsinthisintervalisacyclic.The‘onlyif’partofthestatementistrivial.Theproofofthe‘if’partisbycontradiction.Forcontradiction,assumethatthereisacycleC1,C2,...,Ckintherelation‘before’overthesetoftransactionexecu-tions,Cjis‘before’Cj+1forj<k,andCkis‘before’C1,whereCjisanexecutionofatransactionTijinape-riodP.LetIjbeintervaloftimeforthatperiodP.LetthecycleC1,C2,...,Ckbe‘smallest’(meaningthatitdoesnotincludeanothercycle).Bythede nitionoftherelation‘before’,foreachj<k,thereisadataobjectxjsuchthatCjperformsanoperationcjonxjbeforeCj+1performsanoperationonxjthatisincon icttocj.ThatmeansthereisatimepointinIjthatisearlierthanatimepointinIj+1.Similarly,thereisatimepointinIkthatisearlierthanatimepointinI1.SinceC1,C2,...,Ckisasmallest,thereisnotmorethanoneexecutionofthesametransactioninthecycle(thisisbecausethatallexecutionsofthesametransactionaccessthesamesetofdataobjectsandperformsthesamesetofoperations).Hence,k≤n.Consequently,theunionofthetimeintervalsoftheexecutionsofthiscy-cle,∪kj=1Ijshouldbeincludedinthetimeintervalwiththelengthn Pn.Hence,thisintervalshouldbeincludedinn+1consecutiveperiodsoftransactionTn.Thisisacon-tradictiontothefactthatforanyintervalwhichconsistsofexactly(n+1)consecutiveperiodsofTn,therestrictionontherelation‘before’onthetransactionexecutionsinthisintervalisacyclic.

Therelation‘before’betweentheexecutionsofdif-ferenttransactionsaremodelledasfollows.Leta=(n+1)Pn).Theorderbetweencon ictoperationsondataobjectxinanintervalwiththelengthlessthanaiscap-turedbyWRij(x)=( 3( Ti.wrtn(x) ∧ ¬Tj.read(x) ); <a; Tj.read(x) ),RWij(x)=( 3( Ti.read(x) ∧ ¬Tj.wrtn(x) ); <a; Tj.wrtn(x) ),WWij(x)=( 3 Ti.wrtn(x) ; <a; Tj.wrtn(x) ).

Toexpressthattherelation‘before’de nedasabovedoesnothaveacyclelongerthann,we rst ndanex-pressionforitstransitiveclosure.Thisisexpressesbythe

followingDCformulaCn

ijde nedas:

C1

ij= (RWij∨WRij∨WWij)

Cnij

= (Cn 1n 1n 1ij∨(Cir∧Crj))

SerializabilityCriterion

AconcurrentexecutionofthesetoftransactionsTis serializableiffitsatis es(Tn.period; =n Pn) i,j≤n,i=j¬(Cnij∧Cn

ji)inanyinterval.

3.2.2TemporalConsistencyCriteria

InaRTDB,therearetwokindsofdataobjects:continuousdataobjectsanddiscretedataobjects.LetOdenotethesetofalldataobjectsinaRTDBS.

Continuousdataobjectsarerelatedtoexternalobjectscontinuouslychangingwithtime.Thevalueofacontinu-ousdataobjectisobtaineddirectlyfromasensororiscom-putedfromthevaluesofasetofotherdataobjects.

Discretedataobjectsarestaticinthesensethattheirvaluesdonotbecomeobsoleteastimepasses.LetthesetofdiscretedataobjectsbeZ.

Ateachmomentoftimeacontinuousdataobjecthasavaluerepresentedbyitscurrentversionwhichisvalidforsometimeinterval.Notethatatthesamemomentoftimetheremaybeseveralversionsofthesamecontinuousobjectindatabasethatarevalid.

Letαbeacontinuousdataobject.Foreachq∈Nthereisastatevariablevalidityq(α)tore ectthevalidityofq’thversionforthevalueofαandarealstatevariablevalueq(α)tore ectthevalueofαattimetistheq’thver-sion.validityq(α)holdsattimetiffq’thversionofacon-tinuousdataobjectαhasbeencreated(beforetimet)andisstillvalidattimet.Forthesimplicityofrepresentation,weassumethatdiscretedataonlyhave0thversion(q=0)withthevalidityinterval[0,+∞).

validityq(α)(t)=1ifftisinthevalidintervaloftheq’thversionofα,valueq(α)(t)=1iffthevalueofαattistheq’thversionofα.

Thereisapositivelowerboundδ forthevalidin-terval(dependingonthesamplingperiods),andeachver-sionmayhaveonlyasingleintervalofvalidity.Foraver-sionqofthedataobjectα,thereisaprede nednumberaviq(α)ly,versionqofαisvalidforaviq(α)(≥δ )timeunitssincethetimeitwascreated.Therefore,

¬validityq(α) ; validityq(α) ;

¬validityq(α) ≥aviq(α)(24) validityq(α) ≤aviq(α))(25)

validityq(α) ;true validityq(α) ∨

validityq(α) ; ¬validityq(α)

(26)

Theabsolutetemporalconsistencyatatimetofadataobjectαmeansthatthereisaversionqofαwhichwasbornattimet(α,q)thatisstillvalid,i.e.t t(α,q)≤aviq(α).TheabsolutetemporalconsistencyofthedatainaRT-DBSmeansthatalldataobjectssatisfytheabsolutetem-poralconsistencyatanytime.Sincewehaveassumedthatatanytime,thereshouldbeaversionqforadataobject(normally,theversionthatwascreatedmostrecently)for

In this paper, we give a formal model for real-time database systems using Duration Calculus. Our model supports the formal reasoning about the operations in the systems. As a case study for our technique, we give a formal specification and verification of

whichvalueqholds,theabsolutetemporalconsistencyisformalisedsimplyasfollows.

AbsoluteTemporalConsistencyCriterionACONS(α,q)isde nedas

2( valueq(α) validityq(α) )

Relativeconsistencysaysthatdataobjectsfromsomedatasetshouldbetemporallycorrelated.AnysetRofver-sionsofcontinuousdataobjects,i.e.Risasetofpairs(α,q),isassociatedwithanumbercalledlengthofrelativevalidityintervaldenotedbyrvi(R).

TherelativeconsistencyofasetRofversionsisex-pressedbythefollowingDCformulaRCONS(R),meaningthatRisrelativelyconsistentiffDCformulaRCONS(R)istrueforallintervals,whereRCONS(R)isde nedas:Forany(α1 ,q),(α2,r)∈R validity)∧¬validity

q(α1r(α2) ;

2 ¬validityr(α2) ; validityr(α2)

( ≤rvi(R)); validityr(α2)

Aswehavesaidearlier,foranydataobjectα,atanytimet,thereisaversionqforwhichvalueq(α)istrue.Normally,whenatransactionreadsαattimet,itwillgettheversionqforwhichvalueq(α).However,insomescheduler,theymaygiveadifferentvalidversion.Inordertobemoregeneral,weintroducethestepfunc-tionTi.readvtoreturntheversionnumberreadbyTiforavalueofdataobject.Ti.readv(α)(t)=qiffattimettransactionTihasperformedareadoperationonq’thver-sionmostrecentlyofdataobject(α).

AtransactionTicanreadasetofversionsofdataob-jectsinaninterval.Therefore,foreachi≤nweintroduceatemporalvariablesRαitoexpressthesetofversionsofdataobjectsreadbyTiinaninterval.

Anexecutionofthetransactionsystemistemporallycorrectiffeachtransaction,ineachperiodofits,meetsthedeadline,readsthesetoftemporallyvalid(i.e.,re-centenough)dataobjectsandiscommittedbeforeanyofthembecomesinvalid,andthatallthedatareadbyatransactioninaperiodarerelativelytemporallyconsis-tent.Theseconditionsarespeci edbytheDCformulasDLi,AT Ci,RTCiasfollows. T

i.period

DLi= ((

2( Ti.arrd ≤Di))∧ .Ti.run=Ci)

Let RDVLD= (α)∈ROi,q=0

Ti.read(α) ∧

Ti.readv(α)=q validity.

Then,q(α)

ATCi=( Ti.period

2( Ti.arrd RDVLD)).RTC T

i.period ∧

((α,q)∈Rαi= 3 i q=0

∧3( T i.read(α) ∧

Ti.readv(α)=q )) RCONS(Rαi)LetCM=

.

i≤nDLi∧ATCi∧RTCi.

CorrectnesscriterionfortheexecutionoftransactionsinRTDBS:anexecutionofsetToftransactionsiscorrect

iffforanyintervalitsatis estheformulaSERIAL∧CM.

4

FormalisationofRead/WritePriorityCeil-ingProtocolinRTDB

Serializabilityof2PLWeadapttheformalisationin[5]fortheiteratedtransactionsystems.In2PL,atransactionexecutionconsistsoftwophases.Inthe rstphasedataobjectlocksareacquired,whileinthesecondphasethedataobjectlocksarereleasedandnewlockscannotbeacquired.ForeachtransactionTiweintroduceastatevari-ableTi.obphasetoexpresswhichphasethetransactionTiisinatatime.Ti.obphase(t)=1ifftransactionTiisintheobtainingphaseattimet.

Then,2PLisformalisedbythefollowingDCformu-las.

Ti.period

( Ti.obphase ; ¬Ti.obphase )(27)Ti.period (28)

2( Ti.obphase ¬td )Ti.period

(29)

2

¬T T i.hldrlk(x) ;i.hldrlk(x)

¬Ti.hldrlk(x) ; Ti.obphase ;true

Ti.period (30)

¬T.hldwlk(x) ; T ii.hldwlk(x)

2 ¬Ti.hldwlk(x) ;

Ti.obphase ;true

Ti.period (31)

2

T.hldrlk(x) ; ¬T(x) ii.hldrlk Ti.hldrlk(x) ; ¬Ti.obphase Ti.period 2

T(x) ; ¬T (32)

i.hldwlki.hldwlk(x) Ti.hldwlk(x) ; ¬Ti.obphase Let2PLC= bethesetoftheDCformulas(27),...,(32)and2PL ∈2PLC2 Theorem1SERIALisprovablefromENVand2PLC.

FormalisationofR/WPCPLetWPL(x)andAPL(x)beconstantsdenotingthewritepriorityceilingandtheabsolutepriorityceilingforadataobjectx,letPN={p1,...,pn}denotethesetofintegersforexpressingthepriorityoftransactions,andletTi.lockedandTi.sysceilbeobject-setandrealstatevariables(de nedbe-low).ThewritepriorityceilingWPL(x)ofdataobjectxisde nedasthehighestpriorityoftransactionswhichmaywritex.WPL(x)= max{pj|x∈WOjandj≤n}.TheabsolutepriorityceilingAPL(x)ofdataobjectxisde nedasthehighestpriorityoftransactionswhichmay

In this paper, we give a formal model for real-time database systems using Duration Calculus. Our model supports the formal reasoning about the operations in the systems. As a case study for our technique, we give a formal specification and verification of

readorwritex,APL(x)= max{pj|x∈ROj∪WOjandj≤n}

ToexpressthebehaviouroftheR/WPCP,weintro-ducearealstatevariableRWPL(x),calledreadwritepri-orityceiling.

Whendataobjectxisread-locked(write-locked),thereadwritepriorityceilingRWPL(x)isequaltoWPL(x)(APL(x)):RWPL(x)(t)=0ifattimetobjectxisneitherread-lockednorwrite-lockedbyanytransaction,RWPL(x)(t)=WPL(x)ifattimetobjectxisread-locked(bysometransaction)andisnotwrite-locked,andRWPL(x)(t)=APL(x)ifattimetobjectxiswrite-locked(bysometransaction).

Ti.lockedisafunctiondenotingthesetofdataobjectslockedbytransactionsotherthanTiatatime:Ti.locked∈[Time→2O],Ti.locked(t)={x|thereisjsuchthatTj.hldlk(x)(t)andi=j}.

Ti.sysceildenotesthehighestr/wpriorityceilingofdataobjectslockedbytransactionsotherthanTiatatime.Ti.sysceil(t)=max{RWPL(x)(t)|x∈Ti.locked(t)}.

WhenatransactionTiattemptstolockadataobjectxattimet,Tiwillbeblockedandthelockonanobjectxwillbedenied,ifthepriorityoftransactionTiisnothigherthanTi.sysceil(t).Inthiscase,wesayTiisblockedbyatransactionTjwhichholdsalockonx.WeintroduceastateexpressionTi.blockedby(Tj)forTi=Tjtoexpressthisfact:

x∈O(Tj.hldrlk(x)∧Ti.wt(x)∧Ti.sysceil≥pi)∨

x∈O(Tj.hld(x)∧Ti.wtwlk(x)∧Ti.sysceil≥p∨

i)x∈O(Tj.hld(x)∧Ti.wtrlk(x)∧Ti.sysceil≥pi)∨

x∈O(Tj.hld(x)∧Ti.wtwlk(x)∧Ti.sysceil≥pi)LetHiPri(Ti,Tj)beaboolean-valuedfunctionoftime(astatevariable)toexpresswhichtransactionbetweenTiandTjhashigherpriority.

(a)

Asapriory,HiPriisapartialorder:Ti=Tj∈T(HiPri (Ti,Tj) ¬HiPri(Tj,Ti))

(HiPri(T

T=T i,Tk)∧j=Tk∈T

HiPri(Tk,Tj))

iHiPri(Ti,Tj)

(b)HiPri(Ti,Tj)hastocapturetheinheritanceofpri-oritiesbytheR/WPCP:

T Tk.blockedby(Ti) i=Tj=Tk∈T

(HiPri(Tk,Tj)

HiPri(Ti ,Tj))(¬T

k.blockedby(T)) T=TTk∈Tiij∈T(HiPri(Ti,Tj) pi>pj)

R/WPCPalwaysallowsthetransactionwith‘thehighestpriority’amongthereadytransactionstorun(PPS):ForTi=Tj:

2( Ti.run ∧ Tj.ready HiPri(Ti,Tj) )

InR/WPCP,whenatransactionrequestsalock,itisgrantediffitspriorityishigherthanthesystemceilingforit.Thisisformalisedby(GrR):

2( ¬Ti.hldrlk(x) ; Ti.hldrlk(x)

3 pi>Ti.sysceil )and(GrW)

2( ¬Ti.hldwlk(x) ; Ti.hldwlk(x)

3 pi>Ti.sysceil )Whenalockisavailableforwhichsometransactionsarewaiting,itwillbegrantedtosomeofthem.Theonewhogetsshouldhavethehighestpriority.Theseunblock-ingrules canbespeci edas(UnBl1):

2(( Ti∈T ¬Ti.hld(x) ) (Ti∈T ¬Ti.wtlk(x) ))and(UnBl2):

2

Ti.wt(x)∧Tj.wtlk(x) ;

¬Ti.wt(x) HiPriR/WPCP(Ti,Tj)

(x∈O,i=j).

R/WPCPisnowobtainedastheconjunction2PL∧PPS∧GrR∧GrW∧UnBl1∧UnBl2.

AnumberofpropertiesofR/WPCPincludingthecorrectnesshasbeenveri edformallyinDC.Wereferthereadersto[7]fordetails.

References

[1]AzerBestavros,Kwei-JayLinandSangHyukSon.Real-TimeDatabaseSystems:IssuesandApplications.KluwerAcademicPublishers,1997.[2]PhilipChanandDangVanHung.DurationCalculusSpeci cationofSchedulingforTaskswithSharedRe-sources.LNCS1023,Springer-Verlag1995,pp.365-380[3]M.R.HansenandZhouChaochen.DurationCalcu-lus:LogicalFoundations.FormalAspectsofComput-ing,1997,9:283-330.[4]Kam-YiuLamandTei-WeiKuo.Real-TimeDatabaseSystems:ArchitectureandTechniques.KluwerAca-demicPublishers,2001.[5]EkaterinaPavlovaandDangVanHung.AFormalSpeci cationoftheConcurrencyControlinRealTimeDatabase.TheproceedinsofAPSEC’99,IEEECom-puterSocietyPress1999,pp.94-101.[6]ChaochenZhou,C.A.R.Hoare,rmationProcessingLetters,1991,40(5):269–276.[7]HoVanHuongandDangVanHung.ModellingReal-timeDatabaseSystemsinDurationCalculus.TechnicalReport260,UNU-IIST,P.O.Box3058,Macau,Septem-ber2002.

本文来源：https://www.bwwdw.com/article/i2d4.html