翻譯以原文和在同一文件中前

MichaelvonNICTA*andUniversityofNewSouthWalesSydney,Australia此，由于形式化驗證的復雜性，過去研究者將注意要集中在了單處理器內核。但是，核。這個升級框架，支持總序列（totalstoreorder,TSO）的多處理器體系結構，該體系結構展示出的是一種弱內存序列。對把這個升級框架運用于seL4內核中的這項工作的所有形式化定義與證明均是在交互式定理證明器Isabelle/HOL中經過機 的軟件每一千行代碼平均含有6個錯誤以及用做好的技術我們可以達到每一千行代碼有0.51個。但是，這在國防、航空這樣的高保障計算機系統的內核中，是不夠的。堅程，中斷處理程序CPU。前者可以通過設計一個不可搶占的內核限制為只支持單個CPU或者單個。CPU上。這將成為一個很麻煩的問題，因為制造商們是通過增加的CPU和來內核。處理由引入多CPU造成的并發(fā)性的能力，通過一種模塊化非侵入式的方法，加入到了現有驗證框架中。這個升級框架，支持總序列（totalstoreorder,TSO）的多為了證明升級框架的實用性，說明其應用在seL4中的經驗。Isabelle/HOL[14]中經 與其他工作相結合，并在第6章總結結論。 —使程序的推理更加簡單，相 （在另一方面，我們可以避免共個受限的多核[1]設計，在這之中的每個CPU都實例。作為的結果，在節(jié)點的內核之間不存在通信，同時節(jié)點間不存在內核數據結CPU在用戶層（IPC之間的通信，必須通過共戶級內存實現的。這樣的高靈活性。當然，我們希望最好兩者兼?zhèn)?，這意味著我們衡根據用戶級應用1CPUCPU可以在一個節(jié)點中集群化。在每個節(jié)點中，我們采用了大鎖設計，以同步它的CPU。圖CPU封裝內的多節(jié)點之間的還允許集群被用來繪制性能邊界的實時系統。在性能域內部，我們可以利用一個大鎖的內核的靈活性。 升級框架把一個驗證單處理器內核變成了集群化的多內核和形式化地升級單處理seL4微內核。盡管如此，我們要求它可（2這允許另外的部件之間的受控通信。為了處理并發(fā)，seL4只支持單處理器，同時它Isabelle/HOL中的抽象規(guī)格描述。IsabelleHOL中實seL4ARMv6平臺上。這是被形式化驗證的版本。x86版本最初是直seL4seL4::CMK的群集seL4x86版本。主要的性的評價要求的NUMA和大量的。內核數據。它被修改為啟動節(jié)點的其余的CPU在結束。為了使本地靜態(tài)內核數據節(jié)點和被開頭的方式更改配置數據，進一步細微的修改是必要的。x86的任務狀態(tài)段（TSS）的。它包含了指向當前運行的線程，因此需要CPU本地的。40行的匯編代碼不得不為了實現一個大鎖設計進行修改。CCPU本地狀態(tài)需要在匯編級行時階段（第4.4節(jié)，我們希望能夠以推理證明每一個的節(jié)點。內核定理保證節(jié)點的內核器之間，由兩部分組成。關于引導階段第一內核內存定內核內存定理表明，內核引導時，每一個CPU的觀察順序語義在當地，這是抽象的規(guī)范依賴于正確的行為與問候并發(fā)。該定理是制定對內存的歷史水平：CPU和內存的位置，任何讀之間或寫其次是閱讀任何時間后，沒有寫另一個CPU發(fā)生?！北凰腿胍粋€多處理器架構的運作模式產生的高級指令（器讀/寫，內存圍欄，CPU開始）的序列。該模型計算的內存所有可能的交錯，考慮到CPU的導致啟動這是必要的，因為引導的第一部分本質上是并行。第一CPU需要在那里將同時通過它剛剛開始的其他節(jié)點的CPU中一個器位置的一些全局配置。有的內存模式的實現也可能執(zhí)行。為這項工作開發(fā)的的弱內存模型是基于x86-TSO運作模式[16]，它與CPU的啟動其它CPU（也嵌套）支持擴展。不像模型，它是一個通用的TSO（總序列）模型，而不是特定于x86的。數被直接從子系統執(zhí)行。最TSO結構支持緩沖轉發(fā)，從而將直接從緩沖介紹的（和圖2中所示）的TSO模型包括緩沖的轉發(fā)和區(qū)域。圖明包括1000行代碼。它的模型器對寫入被重新排序，以開始另一個CPU的信號的可能性建模。雖然這x86CPU中從未被觀察到（程序員往往依靠它不會發(fā)生，無論是英特爾，也所以我們寫了從頭開始完成多內核引導規(guī)格描述（1300行代碼。證明內核定理和內核內存定理需要6400行代碼。同時，需要考慮內存柵欄和一個正確的CPU啟動順序的證明（3）在引導中，seL4L4.verified是一個不變的特例。這個可以用幾十個行CPU的動作。在一自動機的一個組成平行運行多個CPU上。4.2CPU本地部分與含有“當前運并行自動機完成一個過渡，它就有可能改變自己的CPU本地狀態(tài)和共享狀態(tài)，但不能意細化到自動機本身具有的原始狀態(tài)的參數化分割成共享和CPU本地部分的并聯組成。在新的并行自動機的每個過渡由合并在CPU本地和共享的狀態(tài)到初始狀態(tài)，執(zhí)行原來的過渡和所產生的狀態(tài)返回到新的共享和CPU本地狀態(tài)。的轉換被交錯非確定性。CPU的本地部分和共享部分的分離和獨立修改可能與不變量相悖。在語句中，規(guī)范和證明在Isabelle/HOL中包括150行代碼。CPU的本地狀態(tài)，而線在了seL4的不分離型不變量確保當前運行的線程的有效狀態(tài)。試圖直接在新的并CC代碼改為：線程缺失問題了是seL4特有的，一個很好的例子中顯示的bug能力定理seL4API允許擁有一種能力的一個線任何其他線程是修改/CPUseL4::CMKB可以BB的狀態(tài)不是有效的，當它被在另一個CPU中的線程A運行刪除，因為在CPU的本地狀態(tài)當前線程的指針來回移動。行代碼，加入了新要求同樣需要1000行代碼的證明。 的多內核是多內核，它與Barrelfish引入的設計的一個擴展[1]，并選擇由Corey[3]。Barrelfish是一個操作系統，旨在為高度可擴展性，適用于異構多處理。它遵seL4啟發(fā)。CoreyBarrelfishCPU的本地太多，但系統軟件允許選擇哪個內核數據應該在CPU之間共享。90年代初。Hurricane[18]NUMA的多處理器數據局部性，而Hive[5]是針對集群之間的故障的。雖然表現良好，對于某Tornado[9]試圖克服這些問題，盡管有非常不同的方法。Disco旨在通過恢復虛擬化的想法，這將允許在大型NUMA多處理器重用通用的操作系統降低實施成本和復雜性。Tornado通過進一步提高數據局部性，旨在更好的可伸縮性。該方法是構建內核在其中在形式化方面，微軟的VCC驗證環(huán)境允許推理驗證并發(fā)的系統級C代碼。證明由同時并發(fā)數據結構（如鎖）被額外處理順序上下文中考慮。VerisoftXT的項目中使用的VCC，正式確認了微軟的Hyper-V虛擬機管理程序的多處理器的主要部分[6]。已經證明體功能的正確性定理。此外，由于VCC規(guī)范語言非常接近C，這導致低層次的規(guī)范很 群集的多內核能發(fā)揮其作為一個多處理器設計能夠把一個單處理器內核到多處理4這樣一個在一個大型項目驗證的單處理器內核。個校對工作（包括缺失對應的證明估計代碼行數）1200020萬行代碼[12]L4.verified的整體尺寸的證明，這是比較小的。C進行了修改時對應的證明也需要修改。對于seL4::CMK，兩個正確性證明還未完成。seL4的單處理器版本中是4.4.1節(jié)中的解決方案線程缺失問題的證明。在其完成之后，最終細化定理可延伸至到C語言級。核[1]的配套工作，但是沒有一個關于大鎖的切換與執(zhí)行的確切的。早期的Linux經驗可以讓我們期待其可擴展性。然而，多核系統之前的系統，其之間是緊密耦合。此外，如果內核是足夠?。ㄈ缥群嘶蛱摂M機管理程序，它很可能是大鎖擴CPUOKL4Microvisor[15]，這過15億多核之上。OKL4上的NaviEngine平臺（4ARM11MPCore的CPU）的初步指標顯示，可擴展性除了比大鎖本身[13]外更受緩存的影響。換句話說：細粒度90年代初的研究來看并不十分樂觀（5節(jié)，然而，這些效果評估NUMA機器的。今天的機器與他們的緊耦合內核和大型分層緩存的seL4::CMK進行 A.Baumann,P.Barham,P.-E.Dagand,T.Harris,R.Isaacs,S.Peter,T.Roscoe,A.Schüpbach,andA.Singhania.Themultikernel:AnewOSarchitectureforscalablemulticoresystems.In22ndSOSP,BigSky,MT,USA,Oct2009.ACM.W.R.Bevier.Kit:Astudyinoperatingsystemverification.Trans.Softw.Engin.,15(11):1382–1396,1989.S.Boyd-Wickizer,H.Chen,R.Chen,Y.Mao,F.Kaashoek,R.Morris,A.Pesterev,L.Stein,M.Wu,Y.Dai,Y.Zhang,andZ.Zhang.Corey:anoperatingsystemformanycores.In8thOSDI,SanDiego,CA,USA,Dec2008.E.Bugnion,S.Devine,andM.Rosenblum.Disco:Runningcommodityoperatingsystemsonscalablemultiprocessors.In16thSOSP,St.Malo,France,Oct1997.J.Chapin,M.Rosenblum,S.Devine,T.Lahiri,D.Tsiu,andA.Gupta.Hive:Faultcontainmentforshared-memorymultiprocessors.In15thSOSP,CopperMountain,CO,USA,Dec1995.E.Cohen,M.Dahlweid,M.Hillebrand,D.Leinenbach,M.Moskal,T.Santen,W.Schulte,andS.Tobies.VCC:ApracticalsystemforverifyingconcurrentC.InS.Berghofer,T.Nipkow,C.Urban,andM.Wenzel,editors,22ndTPHOLs,volume5674ofLNCS,pages23–42,Munich,Germany,2009.Springer-Verlag.M.Daum,J.D?rrenb?cher,andB.Wolff.Provingfairnessandimplementationcorrectnessofamicrokernelscheduler.JAR:SpecialIssueOperat.Syst.Verification,42(2–4):349–388,M.Daum,N.W.Schirmer,andM.Sidt.Implementationcorrectnessofareal-timeoperatingsystem.InInt.Conf.Softw.Engin.&FormalMethods,pages23–32,Hanoi,Vietnam,2009.Comp.Soc.B.Gamsa,O.Krieger,J.Appavoo,andM.Stumm.Tornado: isinglocalityandconcurrencyinasharedmemorymultiprocessoroperatingsystem.In3rdOSDI,pages87–100,NewOrleans,LA,USA,Feb1999.L.Hatton.Re-examiningthefaultdensity-componentsizeconnection.Softw.,14(2):89–97,1997.G.Klein.Operatingsystemverification—anoverview.Sˉadhanˉa,34(1):27–69,FebG.Klein,K.Elphinstone,G.Heiser,J.Andronick,D.Cock,P.Derrin,D.Elkaduwe,K.Engelhardt,R.Kolanski,M.Norrish,T.Sewell,H.Tuch,andS.Winwood.seL4:FormalverificationofanOSkernel.In22ndSOSP,pages207–220,BigSky,MT,USA,Oct2009.A.Lyons.Efficientconcurrencycontrolforhigh-performancemicrokernels.BScthesis,SchoolComp.Sci.&Engin.,UniversityNSW,Sydney2052,Australia,Jul2011.Availablefrompublicationspageathtt T.Nipkow,L.Paulson,andM.Wenzel.Isabelle/HOL—AProofAssistantforHigher-OrderLogic,volume2283ofLNCS.Springer-Verlag,2002. P.Sewell,S.Sarkar,S.Owens,F.Z.Nardelli,andM.O.Myreen.x86-TSO:Arigorousandusableprogrammer’smodelforx86multiprocessors.CACM,53(7):89–97,Jul2010.J.Shapiro,M.S.Doerrie,E.Northup,S.Sridhar,andM.Miller.Towardsaverified,general-purposeoperatingsystemkernel.In1stNICTAWSOperat.Syst.Verification,Sydney,Australia,Oct2004.R.Unrau,O.Krieger,B.Gamsa,andM.Stumm.Hierarchicalclustering:Astructureforscalablemultiprocessoroperatingsystemdesign.J. p.,9:105–134,1993.M.vonTessin.Towardshigh-assurancemultiprocessorvirtualisation.In6thVERIFY,Edinburgh,UK,Jul2010.B.J.Walker,R.A.Kemmerer,andG.J.Popek.SpecificationandverificationoftheUCLAUnixsecuritykernel.CACM,23(2):118–131,1980.TheClusteredMultikernel:AnApproachtoFormalVerificationofMultiprocessorOSKernelsSydney,Australia Operating-systemkernelsarecriticalsoftwarecomponentsincom-putersystems.Buildingsecure,safeandreliablecomputersystemstheimplementationlevel.Kernelverificationhasattractedmuchre-searchinterest.Forexample,theL4.verifiedprojecthasprovedthattiprocessor/multicoresystemsgainingpopularity,alsoinembeddedsystems,theneedforverifiedmultiprocessorkernelsarises.averifieduniprocessorkernelandreusesitsproofstoobtainaframeworksupportstotal-store-order(TSO)multiprocessorarchi-experiencewithapplyingtheliftingframeworktoseL4.checkedintheinctivetheoremproverIsabelle/HOL.Operating-system(OS)kernelsarecriticalsoftwarecomponentsThisisnotenoughforkernelsinhigh-assurancecomputersystemsused,forexample,indefence,aviationandthelike.ifyingakerneldowntotheimplementationlevel.Thehistoryofkernelverificationstartsinthe70sand80s[2,20],butnoneofthese?NICTAisfundedbytheAustralianernmentasrepresentedbytheDepartmentofBroadband,CounicationsandtheDigi-CentreofExcellenceprogram.Permissiontomakedigitalorhardcopiesofallorpartofthisworkforrepublish,topostonserversortoredistributetolists,requirespriorspecificpermissionand/orafee..

tationproofs”[11].Inthefirstdecadeafter2000thetopicattractednewinterest.Verifyingakernelwaspartofseveralverificationsayingthattheimplementationadherestoaformalspecificationofthedesiredfunctionality.level,thekernelsmentionedabovehavetwothingsincommon:First,theyarerelativelysmall,intheorderofafewkLOC.Sec-tipleCPUsinparallel.Theformercanbe ebymakingakernelnon-preemptibleorevent-basedwithwell-definedpreemp-abovearerestrictedtoonlysupportasingleCPU(orcore1).Insummary,thecurrentstateofresearchrestrictscomputerThisisaproblembecausemanufacturersincreasecomputingpowerintotheembeddedworldnow.Verifyingankerneldowntoimplementationlevelrequiresalargeeffort,whichoftenincludesthedevelopmentoftheverification theexistingverificationframeworkinamodularandnon-intrusiveway.Theliftingframeworksupportstotal-store-order(TSO)multi-processorarchitectures,whichexhibitweakmemoryordering.Forthispurpose,theformalTSOmodelwhichitbuildsonexplic-memoryreportonourexperiencewithapplyingittoseL4.checkedintheinctivetheoremproverIsabelle/HOL[14].trueforthetermsmultiprocessorandmulticore.Thepapercontinuesasfollows:Section2summarizesback-frameworkanditsapplication—aredescribedinSection3andSec-andconcludeinSection6.Formalverificationofconcurrentsystemsishardand intractableveryquickly.Incaseofamodel-checkingapproachwhereallpossiblestatesareenumeratedandchecked,thecomplex-canbe afractionofthenumberofstatesinmodelcheckingandcanbetoproveeachofthesescenarios.animplementationrefinesaspecification.Arefinementproofisinterruptsdependingonthestateitisin(e.g.kernel/userlevel/idle).which,inthecaseofakernel,modelsthatkernel’sbootstrapphase.“Running”theautomatonmodelstheruntimephaseoftheingcorrespondencebetweentheconcreteand istoprovethatalltheseinvariantshold.stractleveldowntotheconcretelevel.Weleveragethatfactbyprovingthenecessarytheoremsonthe wouldbemuchharder.normallydesignedforsequentialreasoningonlyastheneedtorea-sonaboutconcurrencycanbeavoidedbymakingakernelnon-supportconcurrency.Mostly,theyarebasedonaninterleavingmodel.However,suchmodelsareproblematicinarefinementcon-textbecauseoftheatomicitymismatchof andconcreteop-erations.Furthermore,concurrent aminimum.or(2)toavoidsharing(ofdatastructures).

parallelonmultipleCPUs,kernelcallscan eabottleneck.Ontheothersideofthespectrum,wecanavoidsharingwitharestrictedmultikernel[1]designinwhicheachCPUbootsupitsNevertheless,amultikernelcanbebootstrappedwithprovisionforWhilethemultikerneldoesnothavethescalabilityproblemofhastodealwiththeconsequencesofmultiplenodes,suchasex-workswithinanode,communicationacrossnodeshastobeibilitywhiletheoppositeistrueforthemultikerneldesign.Oftion.Thisispossiblewithaclusteredmultikernel,whichisacon-weapplythebig-lockdesigntosynchroniseitsCPUs.sharedsharednodenodeFigure1:TheClusteredtheunderlyinghardwareinmind.Forexample,multiplecoreswithinaCPUpackagecanbeclusteredintoanodebecausescal-ingalsosuitsarchitectureswith“islandsofcachecoherence”.bilityofabig-lockkernel.TheclusteredmultikernelresemblestheclusteredkernelsofHur-ricane[18]andHive[5]whicharediscussedinSection5.Theliftingframeworkturnsaverifieduniprocessorkernelintoaclusteredmultikernelandformallyliftstheuniprocessorrefinementreusingtheprovedtheoreminamoregenericcontext.Forexample,atheoremaboutakernel-internalfunctioncanbedirectlyreusediftheliftingframeworkensuresthatnoconcurrencyisintroducedforthatparticularfunction.Themainchallengesfortheliftingframeworkare:(1)howtocorrectlyhandletheconcurrencythatcannotbeavoidedintheclus-teredmultikernel;(2)howtonon-intrusivelyextendagivenunipro-cessorverificationframework;and(3)howtoreuseasmuchaspossiblefromtheuniprocessorproof.lectionofprovedkernel-agnostictheorems.kernelonly.Nonetheless,weclaimthatitcanbeappliedtoanarbitraryuniprocessorkernelunderthefollowingassumptions:(1)linedinSection2(distinctbootstrapandruntimephases);andTheseL4withtheexceptionoftwowell-definedpreemptionpoints.verifiedthattheCimplementationrefinesanintermediateexecutablerefinesan istheversionthatisformallyverified.Thex86versionwasinitiallyspecificationaddedlater.Therearenstowritean ificationandprovethatitisrefinedbytheimplementation.forthisistheabundantavailabilityofx86multiprocessor/multicoreinmindrequiringNUMAandahighnumberofcores.lowingchangestotheimplementationandthespecification.ingCPUs:TheveryfirstCPUdiscoversdevices,configuresthetform,allocatesmemorytonodes,writestheconfigurationtoaspecificregionofmemoryandstartsthefirstCPUofeachWithineachnode,theoriginaluniprocessorbootstrap

kerneldata.ItwasmodifiedtostarttheremainingCPUsofthetheconfigurationdataisreadatthebeginning.sharedbetweenCPUsofthesamenode.MostofthestateendedandthereforeneedstobeCPU-local.ondpartofbootstrapistheoriginaluniprocessorbootstrapwithafewdozenLOCofmodifications.Fortheruntimephase,only40LOCofassemblycodehadtobemodifiedinordertoim-plementabig-lockdesign.NochangesontheClevelwerenec-implementedcompleyontheassemblylevel.cationsarerelativelysmall.LiftingtheBootstrapKernelIsolationnodeinisolation.theruntimephase:“Kerneldatastructuresarenevercreatedoutsidethedesignatedmemoryregion.”specificationrelieson.Thetheoremisformulatedonthecation,betweenanyreadorwritefollowedbyareadanytimelater,nowritebyanotherCPUoccurs.”ingsofmemoryaccesses,takingintoaccounttheresultingstartoryordering(Section4.3.3).ThisisnecessarybecausethefirstpartofbootstrapistheCPUsoftheothernodeswhichithadjuststarted.Provingthekernel-memory-accesstheoremonthe ispermissiblebecausememoryaccessesareoverapproximated.Thismeansthatinsteadofdirectlymodellingeveryassemblyinstructionthataccessesmemory(whichisimpossibleonthe areperformedforaspecific operation.Themodelthenplementationcouldpossiblyperform.withsupportforCPUsstartingotherCPUs(alsonested).Unlikeandnotspecifictox86.ture.WheneveraninstructionexecutedbytheCPUretiresandtrig-storebuffer—whichdelayswritingittothememorysubsystem2bystore-bufferforwardingandmemoryfences.rempresentedabove) passes1000LOCinIsabelle/HOL.Thenoveltyofthismodelisthecombinationofhandlingnesteditmodelsthepossibilityofamemorywritebeingreorderedwiththeobservedonx86CPUs(andprogrammersoftenrelyonitnottoaretoexplicitlyallowstaleconfigurationdatawrittenbytheCPUithasbeenstartedfrom.ofL4.verified.Hence,therewasnoexisting thekernel-memory-accesstheoremrequired6400LOC.colsensuresequentialconsistencyofthememorysubsystem.

TheprimarysourcesofproofcomplexityturnedouttocometheotherCPUsviaaspecificregionofmemory.Becausethisre-andcouldthereforebeprovedwithafewdozenLOC.Intheme ,anintermediateHaskellspecificationoftheandacorrespondenceproofiscurrentlybeingworkedon.LiftingtheRuntimereasonabouteachnodeinisolation.multikernel,wehavemultipleCPUsrunninginparallel,whichrequiresustomodeleachnodeasaparallelcompositionoftheuniprocessorrefinementautomaton.statebutitcannotmodifyanotherCPU’sstate.Thismaysounduniprocessorworld.operationwith merliftsanarbitraryrefinementautomatonintoaparallelcompo-intosharedandCPU-localparts.EachtransitioninthenewparallelautomatonconsistsofmergingtheCPU-localandsharedstatesintotheoriginalstate,executingtheoriginaltransitionandsplittingtheputsabiglockaroundtheentirekerneltransition.operationtotherefinementautomataofboth andconcretelevelsofanarbitraryrefinementproof,theconcreteparallelrefine-mentautomatonrefinesthe parallelrefinementautomatonrefinementautomaton.”Thetheoremcanonlybeappliedifcertainpropertiesabouttheliftingparametershold.Mostofthemaretrivialorobvious,e.g.thatthesplittingfunctionsplitstheentirebutallthemorecriticalassumption:Theoriginalinvariantsneedtobesplittable.Whatdoesthismean?RememberthatcorrespondenceproofsgenerallyrequireanantsdonottalkaboutthesharedandtheCPU-localstateatthesametime”,orinotherwords,“relatethemtoeachotherinanytomatoncanbeautomaticallylifted.Theautomatonliftingoperationandtheorempresentedhereare—stateintosharedandlocalparts.SpecificationandproofsinIs-abelle/HOLcomprise150LOC.Theliftingtheoremrequirescertainpropertiesaboutthelift-ingparameterstohold.Mostofthemaretrivialandcouldbeertyturnedouttobenastytoprove.Morethanthat,itdoesnotevenholdforseL4:Thereareahandfulofinvariantswhichre-latethesharedwiththeCPU-localpartofthestate.Specifically,thatwehadtoderiveamoregenericversionoftheliftingtheo-remwhichprovidesthepossibilityofdividinguptheinvariantsdledautomaticallywhereastheunsplittableoneshavetobeprovedInseL4,theunsplittableinvariantsensurethevalidstateoftheoverthenewparallelrefinementautomatonrevealedanunexpectedified/deletedwithoutcoordinationasthiswouldresultincorruptionlocalstateisnowlemrequiredonly80LOCofCcodeandasimilaramountonthelevel.Thissoundsrelativelyharmless.Nevertheless,duefixinguptheinvariantproofsoverthe amoderateeffort(100LOCmodified,300LOCadded),addinganewlyrequiredinvariantrequireda1000-LOCproof.afterthosechanges.Theclusteredmultikernelisanextensionofthemultikernel,whichisthedesignintroducedwithBarrelfish[1]andalsochosenby

byseL4.CoreyisanOSwithalmostthesameaimsasBarrelfish.KerneldataisCPU-localtoo,butsystemsoftwareisallowedtochoosewhichkerneldatashouldbesharedbetweenCPUs.mance.Inthelate90s,Disco[4]andTornado[9]triedto OSesonlarge-scaleNUMAmultiprocessors.Tornadoaimedatwastoconstructthekernelinanobject-orientedmannerwhichen-allowedkerneldatalocalitytobefine-tuned.Ontheformalside,’sVCCverificationenvironmentallowstoreasonaboutconcurrentsystem-levelCcode.Proofsseparay.TheVerisoftXTprojectusedVCCcessorversionwithminormodificationswhileonlyintroducingasmallamountofconcurrency.Theliftingframeworkispracti-large-scaleproject.Wearenotawareofasuccessfulrefinementproofofamulti-[12],thisisrelativelysmall.FutureCorrespondenceofCTheliftingframeworkconcentratesonthe spondenceproofsneedtobefixedifthecodeinquestionwasmod-ified.ForseL4::CMK,twocorrespondenceproofsaremissing.ThisproofwasalsomissinginseL4’suniprocessorversiontoseL4::CMK.Thisrequiressomefixesduetotheslightlymodi-tionalcorrespondenceproof.Thesecondmissingcorrespondenceproofbelongstothesolu-tionofthethread-deletionproblemfromSection4.4.1.Afteritscompletion,thefinalrefinementtheoremcanbeextendedtoreachdowntotheClevel.ThemissingcorrespondenceproofscanbecarriedoutinthesamewayandwiththesameverificationframeworktheyhadbeencarriedoutinseL4’spast.Thereisnothingconcurrency-specificinPerformanceOnthesystemsside,theimpactoftheclusteredmultikernel’slimitationsisstillunclear.Whilethereisalreadyplentyofsupport-ingworkforthemultikernel[1],noconclusiveevaluationexistsonhowfarandunderwhichworkloadsexactlyabig-lockkernelscales/performs.ExperiencewithearlyLinuxletsusexpectscala-bilityproblems.However,thiswasbeforetheadventofmulticoresystemswiththeirtightcouplingbetweencores.Furthermore,ifthekernelissufficientlysmall(e.g.amicrokernelorhypervisor)itislikelythatthebiglockscalesuptoareasonablenumberofCPUs.AnexamplethatsupportsthisconjectureistheOKL4Microvi-sor[15],asmallcommercialmicrokernel/hypervisorimplementedinthebig-lockdesign:Ithasbeensuccessfullydeployedinover1.5billionmulticore phonestodate.PreliminarybenarksofOKL4onaNaviEnginetform(4ARM11MPCoreCPUs)re-vealedthatscalabilitywasdegradedmorebycachecontentionthanthebiglockitself[13].Inotherwords:Fine-grainedlockswouldnotremovethescalabilityproblem.Lookingatclustering,researchfromtheearly90sdoesnotlookverypromising(Section5.However,theseperformanceevalua-tionsarebasedonlarge-scaleNUMAmachinesofthattime.To-day’smachineswiththeirtightcouplingofcoresandlarge,hier-archicalcachesrequiredifferenttrade-offs.Furthermore,wecon-jecturethatthehighcomplexityandunpredictableperformanceofthesesystemsareintroducedbytryingtohideclusteringfromtheapplicationandprovideasingle-systemimage.Wethatthisisnotnecessaryformostoftheapplicationsyouwouldrunonaclusteredmultikerneltoday.Consequently,thenextstepinthisworkisathoroughperfor-manceandscalabilityevaluationoftheclustered-multikernelde-signbasedonbenarksofseL4::CMK.Theevaluationshouldanswerthefollowingquestion.Fromasystemdesigner’spointofview,amultiprocessorkernelusingtraditionalsynchronisationprimitives(suchasfine-grainedlocks,lock-)givesus(1)goodscalabilityand(2)flexiblekernel-resourceusageacrossCPUsatthesametime.Forverificationrea-sons,werestrictourselvestoaclusteredmultikernelwhereweneedtotradeonefortheother.Sothequestionis:For“anyinteresting”multiprocessorworkload,canweclusterintonodesonlythepartsrequiringflexiblekernel-resourceusageand(re)writetherestoftheworkloadtorunasadistributedsystemofnodesandstillper-S.Peter,T.Roscoe,A.Sc