Killed notKilled
waitAbort
fail1 success1
voted1
handling1 locDone1
comp1 start1
2 2
sigAbort2 sigAbort1
doneAll abortAll commitAll
sync
voteAbort voteNotAbort start
synced noIntTasks Killed notKilled waitAbort
Fig.2.P/Tnetmodels:(a)Taskmodel(b)Controllermodel
whicharerepresentedgraphicallybyarcswithablackdotatthetransitionend,
andweightedarcs.Theformerareusedtoshowthefactthat transitionsinthe
tasknetcantestthestateofsharedvariable, suchas Killed, whichismodelled
bytwocomplementaryplacesnotKilledandKilledin thecontrollernet.
Ourbasicideaofmodelling theAda codefor theAtomicActionbehaviour
withP/Tnetsisasfollows.Werepresentstatesofeachtaskasunshadedplaces
andkeyactionslocaltothetaskasunshadedtransitions.ArrivingintheAtomic
Actionbythetaskisrepresentedbytransitionarr1.Thisalsogeneratesatoken
intheplacewaitAbort,whichbelongstothecontrollerandcountsthenumberof
tasks that haveactually entered the AtomicAction.The place labelled comp1
correspondsto thestateof thetask inwhichthetaskperformsnormal
compu-tation.Fromthisstatethetaskmayeither:(a)executetransitiondone1andgo
to the Local Done state of normalcompletion of the action (place locDone1),
or(b)itmayraiseanexceptionbyringtransitionsigAbort1(thiscorresponds
to executingtheSignalAbortprocedure,whichswitchesthestateof theKilled
ag from false to true { a token is toggled from place notKilled to Killed), or
(c) itmay beforcedtogo totheError-Handlingstate(placehandling1),either
from theNormalComputation stateorfrom thetheLocalDone statebecause
ofsometasks(includingitself)hasraisedanexception,inwhichcasetransition
except12willbered.
SubsequentactionofthetaskdependsonwhetherthetaskendsintheLocal
Done or in the Error-Handlingstate. If theformer, the task provides a
condi-tionfor thecontrollerto rea sharedtransitiondoneAll (correspondingto the
state, it handles the exception, and, depending on the result of the handling,
voteseither forActionCommitorActionAbort.
The voting mechanism used in Atomic Actions allows one task voting for
Abort toforce theentireoperationinto Failure.InourPetrinetmodel,this is
achieved by using three transitions sendAbort1, sendComm1 orsendAbComm1,
individual to thetask. These transitions are connected to twocomplementary
placesvoteNotAbortandvoteAbortinthecontrollernet.Initially,whenthe
vot-ingbegins,atokenisassumedtobeplacedintoplacevoteNotAbort.Whilenone
ofthetasksvoteforAbort,thetokenremainsinthisplace,andifthetaskvotes
for Commit, which corresponds to the handlingok ag being set in the task,
transition sendComm1resdueto thereading arcfrom placevoteNotAbort.As
soonasoneofthetasksvotesforAbort,transitionsendAbort1isred,which
tog-glesthetokenfromvoteNotAborttovoteAbortinthecontroller.Thiscorresponds
to assigning the stateof the global ag Finalresult to aborted in the Cleanup
entry. After that, in all tasks, regardlessof their individual voting, transition
sendAbComm1willreduetothereadingarcfrom placevoteAbort.
Votingiscompletewhenthetaskisinthestatewhereitisreadytocheckthe
value ofthe decision ag.This correspondsto a tokenin the voted1place. At
thispointalltaskssynchroniseonringsharedtransitionscommitAllorabortAll,
which are respectively preconditioned by the controller's places voteNotAbort
and voteAbort. If the former res it puts a token in the local success1place,
otherwisethe local fail1 ismarked.The task subsequentlyres one of the two
possiblerestart transitions which correspondsto bringing thetask to thestate
whereitisreadyto executetheAtomicActionagain.
UsingthePEDtoolweconstructedthemodelofthesystemfromthetaskand
controllerfragments.Oncetheappropriateplacesandtransitionsaremergedthe
actual behaviouralinteraction betweentask andcontrolleris achievedthrough
thefollowingtwomain mechanisms:
{ (i) synchronisation on shared transitions, which is similar to rendez-vous
(blocking)synchronisation,and
{ (ii)communicationviasharedplaces,whichissimilartoasynchronous
(non-blocking)communication.
3.4 Vericationof the P/T-net model
This P/T net model of the Ada code canbe exported from PED to analysis
tools,suchasINAorPEP.WeusedPEP,inwhichwecouldsimulatethetoken
game and perform reachabilty analysis to verify by Model Checking the key
propertiesofthealgorithm.First,if`Task1'isinplacesuccess1thenitmustnot
bepossibleforanyoftheothertasks(say2)tobein fail2.This ispresentedto
thereachabilityanalysistoolbythefollowinglogicstatement:
success1,fail2
aremarkedisnotreachable.
Similarly, to thetest forreachabilityofa markingin which bothtasks end
in successstate:
success1,success2
thetoolreactswith<YES>andproduces:
_SEQUENCE:
arr2,done2,arr1,done1,doneAll
whichisaringsequenceleadingtotheglobalsuccessstate.
Whensetting the option Calculate all paths to true, the tool produces
thefollowinglistofringsequences:
_SEQUENCE:
arr2,done2,arr1,done1,doneAll
arr2,arr1,done2,done1,doneAll
arr1,arr2,done2,done1,doneAll
arr1,done1,arr2,done2,doneAll
arr2,arr1,done1,done2,doneAll
arr1,arr2,done1,done2,doneAll
Thisset,however,includes onlythose paths which go throughthelocDone
states, but not those which are the result of succcesful handling and overall
Commit voting. This is caused by the fact the system searches for all paths
satisfyingtheshortestlengthcriterion.
Theeect ofacoherenterrorhandlingcanbetestedby:
fail1,fail2
Thisresultsin:
_SEQUENCE:
arr1,done1,arr2,sigAbort2,except21,sendAbort2,except12,sendAbComm1,sync,abortAll
arr2,arr1,done1,sigAbort2,except21,sendAbort2,except12,sendAbComm1,sync,abortAll
...
alltogetherover600paths.Theseassertionsimplyinconsistencyisnotpossible.
We have also used tool INA to verify the various behavioural (safety and
liveness)properties.Theresultsofthisanalysisare:
Safety Properties:
Safe - No
Bounded - Yes
Dead State Reachable - No
Covered by Transition-Invariants - Yes
ously,but that thetotal numberof tasksis bounded. All transitionsbelong to
a transition-invariant, which means that the net is structurally live, i.e. it is
suÆcientlyrich inconnectionsto makeitlive.
Resettable, reversable (to home state) - Yes
Dead transitions exist - No
Live - Yes
Live and Safe - No
Thecomputedreachabilitygraphhas76states.
The INA tool allows to state properties in the form of CTL
(Computa-tional Tree Logic) [12] formulas.We canformulate properties ofinterest, such
as whether there exists apath which leads to astate where one task ends in
successwhiletheotherinfail:
EF((P18&P21 )V(P19 &P20 ))
HereP18(P19)standsforsuccess1(success2)andP21(P20)forfail2 (fail1).
Theresultofthecheckis:
s1 sat EF((P18 &P21 )V(P19 &P20 )):FALSE
Anotherinterestingpropertywouldbe,whetherthereisapaththatleadsto
astatein which bothtasksend in successbut theagKilled (placeP7below)
hasbeensetto true:
s1 sat EF(P7&(P18 &P19 )): FALSE
Forcomparison,wehavetriedamodiednetmodelforatask{weomitteda
readarcleadingtotransitiondone1whichtestsagnotKilled.Thismodication
may correspond to allowingthe code for atask to benon-sequential {a task
maysignalabortandatthesametimepasstoLocalDone(theeectofinertia
or delay in reactingto the abort). Interestingly, such a modication doesnot
leadto the violationof deadlock-freenessorthe propertyof bothtasks ending
eitherin successorfail. Butforthelastpropertyaboveitreturns:
s1 sat EF(P7 &(P18 &P19 )): TRUE
4 CPN Modelling and Analysis
We modelled Atomic Actions using Coloured Petri nets (CPNs) and analysed
themodelusingtheDesign/CPNtool.ThethreemainCPNsforthemodelare
showninFigures3,4and5.
They capture the system hierarchically, asa composition of the controller
andtask nets.Dueto theabilityofCPNs todistinguishobjectsbytheirtoken
coloursand values,wecanusethesamenetstructure foralltasks andencode