下载
加入VIP
  • 专属下载券
  • 上传内容扩展
  • 资料优先审核
  • 免费资料无限下载

上传资料

关闭

关闭

关闭

封号提示

内容

首页 The Theory and Practice of Concurrency_Roscow

The Theory and Practice of Concurrency_Roscow.pdf

The Theory and Practice of Conc…

费旻昱003
2011-07-26 0人阅读 举报 0 0 0 暂无简介

简介:本文档为《The Theory and Practice of Concurrency_Roscowpdf》,可适用于IT/计算机领域

ContentsiTheTheoryandPracticeofConcurrencyAWRoscoePublished,revisedtoandlightlyrevisedtoTheoriginalversionisinprintinAprilwithPrenticeHall(Pearson)ThisversionismadeavailableforpersonalreferenceonlyThisversioniscopyright(c©)PearsonandBillRoscoeContentsPrefaceixIntroductionBackgroundPerspectiveToolsWhatisacommunicationIAFOUNDATIONCOURSEINCSPFundamentalconceptsFundamentaloperatorsAlgebraThetracesmodelandtracesrefinementToolsParalleloperatorsSynchronousparallelAlphabetizedparallelInterleavingGeneralizedparallelivContentsParallelcompositionasconjunctionToolsPostscript:OnalphabetsHidingandrenamingHidingRenamingandalphabettransformationsAbasicguidetofailuresanddivergencesToolsPipingandenslavementPipingEnslavementToolsBuffersandcommunicationPipesandbuffersBuffertoleranceThealternatingbitprotocolToolsNotes()TerminationandsequentialcompositionWhatisterminationDistributedterminationLawsEffectsonthetracesmodelEffectsonthefailuresdivergencesmodelIITHEORYOperationalsemanticsAsurveyofsemanticapproachestoCSPTransitionsystemsandstatemachinesContentsvFiringrulesforCSPRelationshipswithabstractmodelsToolsNotesDenotationalsemanticsIntroductionThetracesmodelThefailuresdivergencesmodelThestablefailuresmodelNotesAnalyzingthedenotationalmodelsDeterministicprocessesAnalyzingfixedpointsFullabstractionRelationswithoperationalsemanticsNotesInfinitetracesCalculatinginfinitetracesAddingfailuresUsinginfinitetracesNotesAlgebraicsemanticsIntroductionOperationalsemanticsviaalgebraThelawsof⊥NNormalizingSequentialcompositionandSKIPOthermodelsNotesviContentsAbstractionModesofabstractionReducingspecificationsAbstractingerrors:specifyingfaulttoleranceIndependenceandsecurityToolsNotesIIIPRACTICEDeadlock!BasicprinciplesandtreenetworksSpecificwaystoavoiddeadlockVariantsNetworkdecompositionThelimitationsoflocalanalysisDeadlockandtoolsNotesModellingdiscretetimeIntroductionMeetingtimingconstraintsCasestudy:levelcrossinggateCheckinguntimedpropertiesoftimedprocessesCasestudy:thealternatingbitprotocolUrgencyandpriorityToolsNotesCasestudiesCombinatorialsystems:rulesandtacticsAnalysisofadistributedalgorithmDistributeddataanddataindependenceAnalyzingcryptoprotocolsNotesContentsviiAMathematicalbackgroundAPartialordersAMetricspacesBAguidetomachinereadableCSPBIntroductionBExpressionsBPatternmatchingBTypesBProcessesBSpecialdefinitionsBMechanicsBMissingfeaturesBAvailabilityCTheoperationofFDRCBasicoperationCHierarchicalcompressionNotationBibliographyMainindexIndexofnamedprocessesPrefaceSinceCARHoare’stextCommunicatingSequentialProcesseswaspublishedin,hisnotationhasbeenextensivelyusedforteachingandapplyingconcurrencytheoryThisbookisintendedtoprovideacomprehensivetextonCSPfromtheperspectivethatmoreyearsofresearchandexperiencehavebroughtByfarthemostsignificantdevelopmentinthistimehasbeentheemergenceoftoolstosupportboththeteachingandindustrialapplicationofCSPThishasturnedCSPfromanotationusedmainlyfordescribing‘toy’exampleswhichcouldbeunderstoodandanalyzedbyhand,intoonewhichcananddoessupportthedescriptionofindustrialsizedproblemsandwhichfacilitatestheirautomatedanalysisAswewillsee,theFDRmodelcheckingtoolcan,overawiderangeofapplicationareas,performanalysesandsolveproblemsthatarebeyondmost,ifnotall,humansInordertousethesetoolseffectivelyyouneedagoodgraspofthefundamentalconceptsofCSP:thetoolsaremostcertainlynotanalternativetogaininganunderstandingofthetheoryThereforethisbookisstill,inthefirstinstance,atextontheprinciplesofthelanguageratherthanbeingamanualonhowtoapplyitstoolsNeverthelesstheexistenceofthetoolshasheavilyinfluencedboththechoiceandpresentationofmaterialMostofthechaptershaveasectionspecificallyonthewaythematerialinthemrelatestotools,twooftheappendicesaretoolrelated,andthereisanassociatedwebsitehttp:wwwcomlaboxacukouclpublicationsbooksconcurrencyonwhichreaderscanfind•alistoftoolsavailableforCSPxPreface•demonstrationsanddetailsofsomeofthetools•directoriesofexamplefilescontainingmostoftheexamplesfromthetextandmanyotherrelatedones•practicalexerciseswhichcanbeusedbythoseteachingandlearningfromthisbook•alistofmaterialsavailabletosupportteaching(overheadfoils,solutionstoexercises,etc)andinstructionsforobtainingthemaswellassupportingtextualmaterialContactinformation,etc,relatingtothosetoolsspecificallymentionedinthetextcanbefoundintheBibliographyTheIntroduction(Chapter)givesanindicationofthehistory,purposeandrangeofapplicationsofCSP,aswellasabriefsurveyoftheclassesoftoolsthatareavailableThereisalsoadiscussionofhowtogoaboutoneofthemajorstepswhenusingCSPtomodelasystem:decidingwhatconstitutesaneventItprovidesbackgroundreadingwhichshouldbeofinteresttomoreexperiencedreadersbeforebeginningtherestofthebookthosewithnopreviousexposuretoconcurrencymightfindsomepartsoftheIntroductionofmorebenefitafterlookingatPartITherestofthebookisdividedintothreepartsandstructuredtomakeitusablebyaswideanaudienceaspossibleItshouldbeemphasized,however,thatthequantityofmaterialandthedifferinglevelsofsophisticationrequiredbyvarioustopicsmeanthatIexpectitwillberelativelyuncommonforpeopletoattemptthewholebookinashortspaceoftimePartI(Chapters–)isafoundationcourseonCSP,coveringessentiallythesamegroundasHoare’stextexceptthatmostofthemathematicaltheoryisomittedAtanintuitivelevel,itintroducestheideasbehindtheoperational(ie,transitionsystem),denotational(traces,failuresanddivergences)andalgebraicmodelsofCSP,buttheformaldevelopmentoftheseisdelayedtoPartIIPartIhasitsoriginsinasetofnotesthatIdevelopedforanintroductorylecturecourseforOxfordundergraduatesinEngineeringandComputingScienceIwouldexpectthatallintroductorycourseswouldcoveruptoSection(buffers),withthethreetopicsbeyondthat(buffertolerance,communicationsprotocolsandsequentialcomposition)beingmoreoptionalPartIIandPartIII(Chapters–and–,thoughChapterarguablybelongsequallytoboth)respectivelygointomoredetailonthetheoryandpracticeInstructorswhoareintendingtodealatanylengthwiththetheorypresentedinPartIIshouldconsidercarefullywhethertheywanttoincludethetreatmentofsequentialcomposition,sinceitcanreasonablybearguedthatthespecialcasesitcreatesaredisproportionatetotheusefulnessofthatoperatorinthelanguageCertainlyitiswellworthconsideringpresentingthetheorywithouttheseextracomplicationsbeforegoingbacktoseehowterminationandsequencingfitinPrefacexiofCSPEitherofthemwouldformthebasisofaonetermgraduatecourseasafollowontoPartI,thoughsomeinstructorswilldoubtlesswishtomixthematerialandtoincludeextractsfromPartsIIandIIIinafirstcourse(AtOxford,introductorycoursesformoremathematicallysophisticatedaudienceshaveusedpartsofChaptersand,onthedenotationalsemanticsanditsapplications,andsomecourseshaveusedpartofChapter,ondeadlock)ThechaptersofPartIIIarelargelyindependentofeachotherandofPartIIThisbookassumesnomathematicalknowledgeexceptforabasicunderstandingofsets,sequencesandfunctionsIhaveendeavouredtokeepthelevelofmathematicalsophisticationofPartsIandIIItotheminimumconsistentwithgivingaproperexplanationofthematerialWhilePartIIdoesnotrequireanyfurtherbasicknowledgeotherthanwhatiscontainedinAppendixA(whichgivesanintroductiontotheideasfromthetheoryofpartialordersandmetricrestrictionspacesrequiredtounderstandthedenotationalmodels),themathematicalconstructionsandargumentsusedaresometimessignificantlyharderthanintheothertwopartsPartIIdescribesvariousapproachestothesemanticanalysisofCSPDependingonyourpointofview,youcaneitherregarditschaptersasanintroductiontosemantictechniquesforconcurrencyviathemediumofCSP,orasacomprehensivetreatmentofthetheoryofthislanguageEachofthethreecomplementarysemanticapproachesused–operational,denotationalandalgebraic–isdirectlyrelevanttoanunderstandingofhowtheautomatedtoolsworkMyaiminthisparthasbeentogiveasufficientlydetailedpresentationoftheunderlyingmathematicsandoftheproofsofthemainresultstoenablethereadertogainathoroughunderstandingofthesemanticsNecessarily,though,themostcomplexandtechnicalproofsareomittedChapterdeservesaspecialmention,sinceitdoesnotsomuchintroducesemantictheoryasapplyitItdealswiththesubjectofabstraction:formingaviewofwhataprocesslooksliketoauserwhocanonlyseeasubsetofitsalphabetAfullunderstandingofthemethodsusedrequiressomeknowledgeofthedenotationalmodelsdescribedinChapters,and(whichaccountsfortheplacingofChapterinPartII)However,theirapplications(totheformulationofspecificationsingeneral,andtothespecificationoffaulttoleranceandsecurityinparticular),areimportantanddeserveattentionbythe‘practice’communityaswellastheoreticiansChapter,ondeadlockavoidance,isincludedbecausedeadlockisamuchTheonlydependencyisofSectiononChapterItfollowsfromthisidependencethatacoursebasedprimarilyonPartIIIneednotcoverthematerialinorderandthatinstructorscanexerciseconsiderablefreedominselectingwhattoteachForexample,theauthorhastaughtatoolbasedgraduatecoursebasedonSection,Chapter,Section,AppendixC,Chapter,Chapter(Sectionsandinparticular),thefirsthalfofChapterandSectionxiiPrefacefearedphenomenonandthereisanimpressiverangeoftechniques,bothanalyticandautomated,foravoidingitChapterdescribeshowtheuntimedversionofCSP(theonethisbookisabout)canbeusedtodescribeandreasonabouttimedsystemsbyintroducingaspecialeventtorepresentthepassageoftimeatregularintervalsThishasbecomeperhapsthemostuseddialectofCSPinindustrialapplicationsofFDREachofthesetwochapterscontainsextensiveillustrativeexamplesChapterisbasedentirelyaroundfivecasestudies(twoofwhicharerelated)chosentoshowhowCSPcansuccessfullymodel,andFDRcansolve,interesting,difficultproblemsfromotherapplicationareasThefirstappendix,asdescribedabove,isanintroductiontomathematicaltopicsusedinPartIIThesecondgivesabriefdescriptionofthemachinereadableversionofCSPandthefunctionalprogramminglanguageitcontainsformanipulatingprocessstateThethirdexplainstheoperationofFDRintermsofthetheoryofCSP,andinparticulardescribestheprocesscompressionfunctionsitusesAttheendofeachchapterinPartsIIandIIIthereisasectionentitled‘Notes’Theseendeavour,necessarilybriefly,toputthematerialofthechapterincontextandtogiveappropriatereferencestorelatedworkExercisesareincludedthroughoutthebookThoseinPartIaremainlydesignedtotestthereader’sunderstandingoftheprecedingmaterialmanyofthemhavebeenusedinclassatOxfordoverthepastthreeyearsSomeofthoseinPartsIIandIIIhavetheadditionalpurposeofdevelopingsidelinesofthetheorynototherwisecoveredExceptforoneimportantchange(thedecisionnottouseprocessalphabets,seepage),IhaveendeavouredtoremainfaithfultothenotationandideaspresentedinHoare’stextThereareafewotherplaces,particularlyinmytreatmentoftermination,variableusageandunboundednondeterminism,whereIhaveeithertidieduporextendedthelanguageandoritsinterpretationBillRoscoeMayAcknowledgementsIhadthegoodfortunetobecomeTonyHoare’sresearchstudentin,whichgavemetheopportunitytoworkwithhimonthedevelopmentofthe‘processalgebra’versionofCSPanditssemanticsfromthefirstIhaveconstantlybeenimpressedthatthedecisionshetookinstructuringthelanguagehavestoodsowellthetwintestsoftimeandpracticaluseincircumstanceshecouldnothaveforeseenTheworkinthisbookallresults,eitherdirectlyorindirectly,fromhisvisionThosePrefacexiiifamiliarwithhisbookwillrecognizethatmuchofmypresentation,andmanyofmyexamples,havebeeninfluencedbyitMuchofthetheorysetoutinChapters,,andwasestablishedbytheearlysThetwopeoplemostresponsible,togetherwithTonyandmyself,forthedevelopmentofthisbasictheoreticalframeworkforCSPwereSteveBrookesandErnstRudigerOlderog,andIamdelightedtoacknowledgetheircontributionsWewere,naturally,muchinfluencedbytheworkofthosesuchasRobinMilner,MatthewHennessyandRoccodeNicolawhowereworkingatthesametimeonotherprocessalgebrasOvertheyears,bothCSPandmyunderstandingofithavebenefitedfromtheworkoftoomanypeopleformetolisttheirindividualcontributionsIwouldliketothankthefollowingpresentandformerstudents,colleagues,collaboratorsandcorrespondentsfortheirhelpandinspiration:SamsonAbramsky,PhilArmstrong,GeoffBarrett,StephenBlamey,PhilippaHopcroft(ne´eBroadfoot),SadieCreese,NaiemDathi,JimDavies,RichardForster,PaulGardiner,MichaelGoldsmith,AnthonyHall,JifengHe,HuangJian,JasonHulance,DavidJackson,LalitaJategaonkarJagadeesan,AlanJeffrey,MarkJosephs,RankoLazic´,EldarKleiner,GavinLowe,HelenMcCarthy,JeremyMartin,AlbertMeyer,MichaelMislove,NickMoffat,LeeMomtahan,TomNewcomb,DavidNowak,JoelOuaknine,AtaParashkevov,DavidPark,SriramRajamani,JoyReed,MikeReed,JakobRehof,BillRounds,PeterRyan,JeffSanders,BryanScattergood,SteveSchneider,BrianScott,KarenSeidel,JaneSinclair,AnttiValmari,DavidWalker,WangXu,JimWoodcock,BenWorrell,ZhenzhongWu,LarsWulf,JayYantchev,IrfanZakiuddinandZhouChaoChenManyofthemwillrecognizespecificinfluencestheirworkhashadonmybookAfewofthesecontributionsarereferredtoinindividualchaptersIwouldalsolikethankallthosewhotoldmeabouterrorsandtyposintheoriginaleditionSpecialthanksareduetothepresentandformerstaffofFormalSystems(someofwhomarelistedabove)fortheirworkindevelopingFDR,andlatterlyProBETheremarkablecapabilitiesofFDRtransformedmyviewofCSPandmademerealizethatwritingthisbookhadbecomeessentialBryanScattergoodwaschieflyresponsibleforboththedesignandtheimplementationoftheASCIIversionofCSPusedontheseandothertoolsIamgratefultohimforwritingAppendixBonthisversionofthelanguageThepassageofyearssincehasonlyemphasisedtheamazingjobhedidindesigningCSPM,andthehugeexpressivepoweroftheembeddedfunctionallanguageRankoLazic´hasbothprovidedmostoftheresultsondataindependence(seeSection),anddid(in)mostoftheworkinpresentingitinthiseditionManyofthepeoplementionedabovehavereadthroughdraftsofmybookandpointedouterrorsandobscurities,ashavevariousstudentsThequalityofxivPrefacethetexthasbeengreatlyhelpedbythisIhavehadvaluableassistancefromJimDaviesinmyuseofLATEXMyworkonCSPhasbenefitedfromfundingfromseveralbodiesovertheyears,includingEPSRC,DRA,ESPRIT,industryandtheUSOfficeofNavalResearchIamparticularlygratefultoRalphWachterfromthelastofthese,withoutwhommostoftheresearchonCSPtoolswouldnothavehappened,andwhohasspecificallysupportedthisbookandtheassociatedwebsiteThisbookcouldneverhavebeenwrittenwithoutthesupportofmywifeCobyShereadthroughhundredsofpagesoftextonatopicentirelyforeigntoher,expertlypointingouterrorsinspellingandstyleMoreimportantly,sheputupwithmewritingitInterneteditionTheversionherewasextensivelyupdatedbymein,withtheadditionofsomenewmaterial(inparticularanewsectionforChapter)Variouserrorshavealsobeencorrected,butpleasecontinuetoinformmeofanymoreAgreatdealmoreinterestingworkhasbeendoneonCSPsincethanthisversionofthebookreportsMuchofthatappears,orisreferenced,inpaperswhichcanbedownloadedfrommywebsiteorfromthoseofothercurrentandformermembersoftheOxfordConcurrencygroupsuchasGavinLowe,ChristieBoltonandRankoLazic´AsIwritethisIanticipatetheimminentpublication(inLNCS)oftheproceedingsoftheBCSFACSmeetinginJulylastyearon“yearsofCSP”ThiswillprovideanexcellentsnapshotofmuchrecentworkonCSPIhavegivenabriefdescriptionofsomeofthisextraworkinparagraphsmarked,mainlyinthenotessectionsattheendsofchaptersThesecontainafewcitationsbutdonotattempttocoverthewholeliteratureofinterestIfanyonereadingthishasanyfeedbackonanysortofbook–eitherfollowingonfrom(partof)thisoneorsomethingcompletelydifferent–thatyouwouldliketoseewrittenonCSP,pleaseletmeknowBillRoscoeAprilChapterIntroductionCSPisanotationfordescribingconcurrentsystems(ie,oneswherethereismorethanoneprocessexistingatatime)whosecomponentprocessesinteractwitheachotherbycommunicationSimultaneously,CSPisacollectionofmathematicalmodelsandreasoningmethodswhichhelpusunderstandandusethisnotationInthischapterwediscussthereasonsforneedingacalculuslikeCSPandsomeofthehistoricalbackgroundtoitsdevelopmentBackgroundParallelcomputersarestartingtobecomecommon,thankstodevelopingtechnologyandourseeminglyinsatiabledemandsforcomputingpowerTheyprovidethemostobviousexamplesofconcurrentsystems,whichcanbecharacterizedassystemswherethereareanumberofdifferentacti

用户评价(0)

关闭

新课改视野下建构高中语文教学实验成果报告(32KB)

抱歉,积分不足下载失败,请稍后再试!

提示

试读已结束,如需要继续阅读或者下载,敬请购买!

评分:

/49

VIP

在线
客服

免费
邮箱

爱问共享资料服务号

扫描关注领取更多福利