Garbage collector verification for proof-carrying code.pdf_大学文库

Lin CX,Chen YY,Li L et al.Garbage collector ver ification for proof-carrying code.JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY 22(3):426~437 May 2007 Garbage Collector Verification for Proof-Carrying Code Chun-Xiao Lin(林春晓)，Yi-Yun Chen(陈意云)，Long Li(李隆)，and Bei Hua(华蓓) Department of Computer Science and Technology,University of Science and Technology of China,Hefei 230027,China E-mail:{cxlin3,liwis}@mail.ustc.edu.cn;yiyun,bhua}@ustc.edu.cn Received September 19,2006;revised March 20,2007. Abstract We present the verification of the machine-level implementation of a conservative variant of the standard mark- sweep garbage collector in a Hoare-style program logic.The specification of the collector is given on a machine-level memory model using separation logic,and is strong enough to preserve the safety property of any common mutator program.Our verification is fully implemented in the Coq proof assistant and can be packed immediately as foundational proof-carrying code package.Our work makes important attempt toward building fully certified production-quality garbage collectors. Keywords program verification,garbage collector,proof-carrying code,program safety 1 Introduction tation,is indispensable by the PCC-style mutators for the safe usage of the collector.On the other hand,as The latest developments in theorem provers,certify- we will show later,the major effort we spend in proving ing compilers and other program verification tools have the collector is on the manipulation of language inde- enabled the building of more trustworthy software sys pendent properties like heap predicates and finite sets. tems using the Proof-Carrying Code(PCC)par adigmIll. Thus,verifying a low-level language,especially C,im- A PCC package contains the native code of the software, plementation of the collector would require almost the its safety specification,and a macine checkable proof same effort.And a certifying compiler,if one could be saying that the code behaves as specified.The client can constructed,is still needed for making the C-level veri- then use a tiny checker to check the safety proof before fication useful to other PCC packages. running the software. We use separation logic6l to define the machine- Software verified in a high-level language is hardly level heap predicates for building the specification of trustworthy if the compiler fails to correctly translate the collector.With separation-logic operators,we de- the verified program into native code,which is often the fine new heap predicates to assert reachability on a con- case due to the various bugs in the compiler.However, crete memory model,which could evade troubles caused in the PCC style of verification,the specification and by cyclic links in heap objects.Our specification of the proof are directly given on,or translated to,the ma- collector states that all the live objects are preserved, dhine level,and the compiler is thus removed from the and all the unreachable objects (in a conservative defi- Trusted Computing Base (TCB).Therefore,the PCC nition)are collected,hence is strong enough to preserve packages are endowed with a higher level of safety. the safety of common mut ator programs. However,in existing PCC frameworks like the Our verification is fully mechanized within the Toucstone-PCCl]and Typed Assembly Language Coq proof assistantl7.We follow the Foundational-PCC (TAL)I2,memory management is either regarded as (FPCC)I8]style to give the proof of the collector along trusted primitive instructions,or included in the trusted side the soundness proof of the whole verification fr ame- libr ary.On the other hand,automatic memory manage- work.The collector's proof in SCAP can be ported ment,especially Garbage Collection(GC)13,is adnowl- to an open FPCC frameworkl9 without much difficulty edged as complex and error-prone.Thus,the overall as shown in 9,which enables our collector's possible safety level of the PCC system will be undermined if an interoperability with other mutator systems.Our ve- unverified garbage collector is included in TCB. rification can also be used as a model for other PCC In this paper,we present the formal verification of systems where the verification of a garbage collector is a conservative variantl4]of the standard mark-sweep necessary. garbage collectorl3]in the PCC style.The technical During our verification of the collector,we make highlights and contributions of this paper include: important improvements to the verification framework. Our verification is performed directly on the We build a sound verification condition generator (VC- machine level with the Hoare-style program logic Gen)for the SCAP system,which alleviates the user Stack-based Certified Ass embly Programming(SCAP)5 from understanding the details of the SCAP rules,and Thus,we are forced to specify and prove the concrete introduces the potential for automatic verification of ba- machine-level behavior of the collector,whid though sic safety properties.We also build automatic tactics in often abstracted out in a high-level language implemen- Cog to deal with proof goals involving separation logic Regular Paper Supported by the National Nat ural Science Foundation of China under Gr ant No.60673126(Verification and Compilation of Software Safety);Intel China Research Center

! "#$% &'%% ( $%) **+,-. /*0/,1 " *221 !!" # ! !!$ % &' '( ' '( ' '( ) ** '' +' '* '* , &' '( '' * ' ' ' * ' '* ' * '* ' ( ' '( '' ' '* - &' ( .'/ ''( ) (' ' ''( * ' )* - ') ) ' ' * ( & '' / ** '' '* &' ** '' ''( * ' '* ( ! ! " " # $ " % ! % # % % !# & ! ! ! # ! " # " % ! ! # ! ' " ! % % " $ # ( ) ) % ! ' # " ! # * ! %! " # + ( ! &$"# ! ! " # ( ! ! ! , - ! % # ! ! . - # $ % " %# / # / ! ! ! % ,# ( , , # ( 0 ! . # / ! 1 " 1" ! ! %# 2 &$" 1" ! % ! Æ ! 345 ! 2 ! # ( " ! # 6 ! % ! %# / 7 ) &$" ! &$" # / . ! 3 # &3 3 & !3 3 0201,4*0 +5 6 &7 &-8 ' 9

Chun-Xiao Lin et al.:Garbage Collector Verification for Proof-Carrying Code 427 inf_loop(){while (1); ge()f mark field(val)f markbit (x)f mark_field(root); if (val=ED)return; return (ED+(x-ST)/2) while(!stack_empty()){ if (val mod 8 !0)return; ptr=stack-pop(); if (markbit (val)==BLACK)return; stack-push(ptr)f mark_field(ptr->first); markbit (val)=BLACK; if (top>=buf)inf_loop(); mark.field(ptr->second); stack-push(val); *(top++)=ptr; for(addr=ST;addrfirst=freeptr; if (freeptr==NULL)loop(); freeptr=addr; l=freeptr; stack_empty(){ freeptr=freeptr->first; return(bot=top）; else markbit (addr)=WHITE; return 1; Fig.1.Pseudo code of our collector and finite set operations.These improvements greatly A GC cycle begins with tracing and marking the simplify the proof construction. objects reachable from root.A mark stadk is used to The work presented in this paper is a part of our on- temporarily store the marked objects whose fields are going projecto to build an unified framework for cer- to be examined.Then,the collector examines the mark tifying the mutator-collector interaction based on mod- bits of all the objects,reclaims those unreachable ob- ern garbage collectors like the incremental ones and the jects to form a free list,and resets all the mark bits. generational ones.As an extension to the work in this The free list can then be used by the allocator when the paper,we have successfully linked a TAL with the veri- GC cycle is finished. fied collectorl following the ideas in [however,this part is beyond the scope of this paper.We also believe e31 that our improvements to the verification fr amework will benefit future researches in this field. Mark Bits The rest of this section is a brief introduction to the collector we verified.Then,we introduce in Section 2 99 the verification fr amework and our extension.In Se ction 3,we discuss the heap predicates that form alize the heap during a collection,and give the safety specification of the collector using these predicates.Section 4 outlines the methodology we used to certify the collector in the SCAP framework.In Section 5,we discuss and eval- Record uate our Coq implementation.Finally,we talk about I i Mark Stack the related work in Section 6 and give the conclusion in Section 7. Fig.2.Collector's heap layout. Note that since all the lemm as and theorems in this paper are mechanically proved in Coq,we skip their de- 2 Verification Framework tailed proofs,interested readers may refer to 12. We discuss in this section the three components of our 1.1 Collector verification framework:a MIPS-like abstract machine model;a Hoare-style program logic,the SCAP system; Fig.1 shows the pseudo code of the garbage collector and a heap specification language with separation-logic we verified,a conservative variant of the standard stop- operators. the-world mark-sweep collector.To simplify the prob- The whole framework is formalized within a mecha- lem,we adopt a heap layout shown in Fig.2:the size of nized met a logic,the Calculus of inductive Construction each heap object is two words;all heap objects reside in (CiC)3.CiC is a higher-or der predicate logic extended a continuous subheap;the collector also keeps the mark with inductive definitions.The CiC terms in this paper bits,a mark stadk and a record of global variables.This are written with the standard logic notations.We let simplification implies that our allocator only works with Prop be the universe of all logical propositions,and let mut ators that always require two-word objects. Set be the universe of all computational terms. The conservative valid-pointer ceck in the mark field procedure follows 4].A value is consid- 2.1 Abstract Machine ered as a valid object pointer only if it is inside the boundaries of the allocatable heap,and aligns to the We show the syntax of the abstract machine in Fig.3. size of two words. A program P is a triple of a code heap C,a machine

0 $ ! ! "#$% &' ( ) & * ! ' +,-./ ! ' !' #' +,-./ ! #' ' !' 0"" "" ' 123 45,, ! 0## #' 45,, ' ( #' ! ' 123 ! ! 4 #93 3 # # ! % , ! % % # $ ' ! % ! % $ ! ! 345 ! # / ! % ! # ! # ! & 8 ! % ' # * & 9 ! 0 # & : ! &$" ! %# * & ; ! . # 1 ! % ! % & . ! % 3?85# 1#? ! ! ! %! # ! ! 1#8+ 0 , ! ! @ , @ % % % % # ! % ! ! . ! ! ,# % ! 3:5# $ , 0 ! ! # $ ) ! % , # $ % % % , ! '# ' % , , % # ! ) # ! * :9 3 / ! %+ A*"&% @ &$" @ ! # ! ! % 0 ! 0 # ' ! # ! ! # / # / ! ' 1#9# $

428 h 1 cmpnm SFi.Ifilt ca,Mas 2007,wca22,Nc.3 srare S aet ae iesrrpcrioe seqpeece I.A cote heaPC of rhe cote blods ro rheir sRecificarioes.We also tefiee is a o aPfroo cote label f ro iesrpcrioe seqpeece I.A rhe io Ficarioe relarioe =oe SCAP sRecificarioes. o achiee srare s coeraies a tara heaPH aet a reSisrer file R.A tara heaPH is a o aPfroo attress 1 (aliSes then (C,(H,),I) ro 4)ro wort valpe w,while a reSisrer file R is a o ap if f E dom(C),(C (,)C(f)) froo reSisrer r ro wort valpe,wirh ro always o aks ro jal f,fret if f E dom(C), 0.We pse rhe sraet art MIPS reSisrer aliasesl14l ie rhe (C,(H,RfrsIfret}),C(f)) resr of rhe PaRer.A coo o aet c is a eoe-coerrolflow jrra ifR(r.)∈dom(C), (C,(H,R),C(R(rg))】 iesmrpcrioe spch as a reSisrer att or a heaP loat.Ae beq ra,rt,f;I' fR(r.)≠B(re),(C,(H,2),), iesrrpcrioe seqpe ece I,or cote block,is a series of coo- else if f∈dom(C),(C,(H,),C(f)】 o aets followet by ae pecoetirioeal jpo Piesrrpcrioe. bne re,rt,f;I' f(rg)=B(re),(C,(H,),I), For sio Ficiry,we seParare rhe cote heaP C froo rhe else if f E dom(C),(C,(H,R),C(f)) o prable t ara heaPH Also,we pse iesrrpcrioe seqpeece c;I if Next((H,))=S',(C,S',I') iesreat of rhe sraet art pc reSisrer,aet rhis resplrs ie if c= then Nexte((H,R))= rhe at tirioeal rerpre attress fret ie rhe jpo Paet liek addu ra,ra,rt (H.Rfra R()+R(:)) iesrpcrioe jal f,fret,which cae be viewet as a o acro addiu ra,ra,W (I,8ra÷R(r)+w}) for rhe MIPS iesrrpcrioe Pair jal f aet j fret. subu rd,rs,It (HI,RfraR(r)-R(r)]) srl rd,r:1 (H,R{ra·R(rs)/2}) sltu rd,rs,rt (HRra) (Prog) P (C,S,0 if R(r)<R(rt),=1,else=0 (CdHeap) C ff andi ra,rs,7 (H,B{ra◆R(rs)mod8}) (State) = (H,) lw ra,w(ra) if ((r)+w)E dom(H), (Heap) = {1ww} (H,RraH((r)+w))) (RFile) = {rw}* sWrs,W(rd if((ra)+w)∈dom(H), (Reg) = (rke(0..31) (HR(ra)+R()R) (Wd.Lab)w.f = 01112|3| (Address) 1 = 04181121. Fg.4.Abstract mach ne semantCs (ISeg) = c:I beq rs,rt,f;II bne ra:rt,f:II jf jal f,frat jr ra (SPred) P,q StateProp Comm) addu ra,r,rt addiu rd,r,w Guar) 9 E State→State+Prop subu ra,ra,rt sr1 rd,ra,1 (BSpec) (p,g) altu rd,ra,rt andi rd,ra,7 (CHSpec) = {14o} lwra,(rs）SW ra:W(ra) WFST(0,9,) 33.93g WFST(n,9.S,) VS'.g S SS'.R(ra)E dom()A Fg.3.Abstract mach ne syntax. p3 A WFST(m-1,g,,Ψ) FollowieS 14],we Sive rhe so all sre PoRrarioeal se- where(p,g）=业('.R(ra) o aerics of rhe absrracr o achiee ie FiS4.We wrire X(z) (m,9)→p,g'）gs,p8→(psA(8'gsS→gs8') for rhe valpe bopet ro zie rhe o aPX,aet X{} for rhe o ap obraieet by pptarieS rhe bieties of z ro F0g.5.SCAP spec (ficat (on constr ucts v ie X.We also wrire S.R for rhe reSisrer file ie srare A ser of o Rerarioeal-seo aerics-baset iefereece rples, S.Nore rhar for ae lw or sw coo o aet,if rhe soprce as Parrly showe ie Fis.6,is Fovitet ro bpilt a well- attress is eor ie rhe too aie of rhe heap rhe eexr srare for o et RoStao froo borroo-pP The absrracr srack is petefieet.The eexr srePof a RoSrao is petefieet if Reticare WFST(n,g,S,ie FiS.5 Seeerally asserrs ir jpo R ro a wroeslabel,or rhe eexr srare of irs ieirial rhar rhe cprreer Rocet pre cae rerpre ro rhe label ie coo o aet is petefieet. ra of irs rerpre srare.n ieticares rhe epo ber of srack frao es,oece ir becooes 0,rhe cprreer cote will eever 2.2 Program Logic rerpre.A terailet keowlet Se of rhese rples aet WFST is eor reqpiret for petersraetieS rhe resr of rhe Paper, The SCAP sysreo 151 is a Hoare-sryle RoStao loSic iereresret reaters o ay refer ro 5. for ootplar verificarioe of asseo bly cote wirh Roce- tpre call/rerpr e.Procet pres cae be verifiet sePararely Leo o a 1 srares rhar if a cote block is well-foro et wirh soo e o,ir is also well-foro et wirh a srroeSer as- aet rhee lieket roSerher ro for o a verifiet Rosrao.As showe ie FiS.5,ae SCAP cote sRecificarioe is a Parrial serr o,aet rhe Foof of a well-for o et cote block cae be lifret froo a local亚o a Slobal亚'. correcreess sRecificarioe coeraieieS a Pair of Recoeti- rioe p aet Sparaeree g.p reasseo bles rhe Recoetirioe Lemma 1 (Weakening). ie Hoare lo Sic,while g relares rhe eerry srare of rhe cote 1.1fo→σ'and;σ'卜I,the:亚；o卜I. block ro rhe rerpre srare of rhe corresPetieS Rocetpre. 2.lf亚亚'amd;oI,them:亚'σ卜I. Thps rhe g ar rhe eerry label of a Rocet pre asserrs rhe Theoreo 1 eespres rhar a well-foro et RoSrao will Sparaeree of rhe Focet pre,as we will see ie rhe larer rpe safely wirhopr sroFFieS ar aey RoStao srePpete- secrioes.A cote heap sRecificarioe y o aR rhe labels fieet ie FiS.4

0 1 ! " #$$%! ##! & ' . # $ . # $ # $ ! ! ! ! ! B# / A*"& # $ C ! # $ . % ! , # 1 ! # $ ! . , % ! ! A*"& # ! , 9 6 9; 1 ! 3?:5 ! 1#:# / ! # / ! # > ' # ' , ! ' # &$" ! D# " % # $ ! 1#; &$" # ! % # ! ! # $ % # / &$" # ! / 9 6 969 ! < & # 9 9 39 $ ! 1#< ! # % 1#; # % B ! # $ % ! . 3;5# ? % ! ! ! ! ! % # ! ? @ + ! 8 @ + @ ? ! ! ! 1#:#

1hntro iac i it ht elCl ae2a \fi 1 cafilce wfeikFarict ke beccl aees it V1 cMi 429 更上p(Well-Formed Program) Theorem(Soundness).If (C,S,I),for 亚卜C:亚pS亚：(n,g)上I3m.WFST(m,g,S.) 044pOtjr04pjl ber n there erists (C,S,I),sjch thot 亚F(C,S) (C,S,1)hc(C,S',I). (PROG) We extelld SCAP by bSildilIg for it a VCGell,w CicC C:(Well-Formed Code Heap) is partly sCowlI iⅡFig.7.ro(亚，I)is a code bloc speci 亚'乎(f)上C()1∈dom(乎) ficatiolI formed from tCe code Ceap specificatioll all d (CDHP】上C:中 t Ce code block I.TCe predicate raorci(,I)makes sSre :(p.g)I(Well-Formed Instruction Sequence) t Cat if II calls procedSre f,f will keep SF SIcCallged,as Ψ；(mg)上Ⅱ reqSired by tCe CALL rSle ilI Fig.6.Sill ce it is Card to g.pS→3s.Next(S)=SA寸SA directly embed raorci ilto ro,we jSst make it a stal dalolle predicate.WitCt Cese defillitiolls,we obtaill TCeH ”.g'SS”+gS" (SEQ) orem 2 from Lemma 1 all d tCe CDHP rSle ill Fig.6. Ψ；(p,g)rCI Theorem 2 (VCGen Correctness). ()=(p,g） 1.lfoc ro(亚，I).raorci(亚，I),thep亚；o卜I. s.ps→VSA3.gs8'→gSS (】 2.1f.c(亚，C),hp亚上C:亚. Ψ；p,g)上jf Wit Ct Ce Celp of VCGell,tCe SCAP proof coll strScH ()=(p,g)(E)=(p”,g" tioll is lifted olto tCe code block level.For eacC block, (阻，R.p(H,R)→Y(阻，R{ra+fxet})A ollly tCe proof of a o implicatioll is reqSired,ilstead .g(H,R{ra+frt})→ of tCe proofs of o implicatiolls for eacC ill str Sctiolls fol p”AS”.g”8'S”→9(L,R)SV(阻，R),(田，R. lowilg tCe rSles ill Fig.6.TCis alleviates tCe Sser from SII derstall dillg tCe complex details of te SCAP rSles, g'(H,R)(H',R')+R(ra)='(ra) 业；m,g)Fjalf,ire (CALL) simplifies tCe proof coll strSctioll,all d makes tCe reasoll illg more I atSr al.Besides,by elimil atillg tCe leed for s.pS→g3S (RETURN) iⅡsta tiatiΠg tCe specificatiolls for eacC iⅡstr Sctiol iⅡHl 重：(p,g)Hjr ra side a code bloc,te VCGell iltrodSces tCe potelltial of aStomatic proof coll strSctioll for programs verified Fa.4.Sk2 P aflrIrclr ulls (xclrpt). agaill st simple properties. vc(更，C)g∀f∈dom(业).((E)→wp(业，C(t)Arapred(更，C(t) ifI= then wp(乎，I)= in case that P (AS.p Nextc(S),AS,S'.g Nextc(S)S') wp(,I')=(卫，g) j f (p,9) 亚(f)=(P,9) jal f,fret (A(H,B)p(H,&{rafret}》∧s.g(H,&{rafret)→p"S', (f)=(p,g) A(H,R),S".3'.g'(H,rafret))S'A g"S'S") 亚(fet)=(p",g") jr ra (AS.True,AS,S'.S=S) ifⅡ= then rapred(Ψ，I in case that e;I rapred(亚，T') jf True jal f,fret (Π，R),(',R).g(I,R)(旺'，R)→R(ra=R'(ra) 亚(f)=(p,g) jr ra True Fa.8.VkGIr (lxclrpt) 2.3 Heap Predicate A,B E Heap→Pop T Set 1→w λIH={1} To specify tCe beCavior of a collector,we iltrodSce emp g λH.dom(H)=0 tCe separatiol logic operators.Separatioll logic was true def AH.True origillally proposed as all extellsioll to Hoare logic for A*B世入I.3H1,H2. reasollillg mStable data strSctSresl6l.II order to emH H1世H2=HA(AH1)A(BH2) ploy it ilI tCe SCAP system,we directly embed a set of T.A f λI.3x:T.(A四 separatiol Hogic operators as Ceap predicate coll str ScH (P)det λH.PA(empH tors Ssillg CiC,as sCowlI il Fig.8.TSs,tCe SCAP ,x∈0.A def emp specificatiolls p alld g,wCicC are state predicates,may V.rE (n}US.A der A[n/x]*H.x∈S-n.A colltaill Ceap specificatiolls bSild witCtCese predicates. We write H A if (A H)is a valid propositioll ill Fa.8 Slparator loga op lrators CiC.TCe defillitiolls are coll sistelIt witC tCe semalltics

4. r(Coc f pyl fi btheolwP aP.AAkwl ol..WSo(x descr52ed m 6.For samplscity of present aton,we se ti at tie geld val e at 1 s valsd wati p.A valsd o2- tle same notat on to denote tie separatson-logsc con- ject (ok_obj(pbl))ss composed of two valed 9elds.Tils, nectaves and t1elog5 c connectaves a【.We also】se tie propostt on 1 obj-hp(pp)5s tr]e only f 5s tle standar d separatson-logsc a22revsatsons:1 D GG formed exactly witi tie leap o2jects m p,and all sts for 1o GX 1+4 D Go,1 D a for )0:Natfl D 0 and 9eld val es are valed wati p It ss notewortly tiat once 00n. 1 obj-hp(plp)1olds,wall 2e a ccoged 1eap witi no Tie md ctavely de9ned sterated separatag conj]nc- o]tgomg pomters.Tie relatsons1 p 2etween obj_hp and ton,E pfw,taken from 15],asserts ti at tie 1eap reach 5s stated a Lemma 3. can 2e splt mto a 9nite set of s 21eaps accordag to tie 9nste set p of nat]ral n]m2ers,wi de for eaci mem2er 1 nu:=0 of p,tiere s a n5gl e s 21eap on wi 5c1 w 1cO 1olds. st,ed :: 8116124|. We prove as lemmas tle propertes of tiese ptrs def {1|(1mod8=0)A(st≤1<ed)} separatson-logsc oper ators (axsoms m [6),and provsde vptr(1) 1 E ptrs Lemma 2 for lmkag tie 1eap predscates wti tie oper- rchrt((R),1) e reach(H,R(to),1) at onal semantscs of tle 1G and cG mstr]ct ons. vptr(1) (REFL) Lemma 2(Heap Operations). reach(H,1,1) 1.lf卜11DG(true,then:卜(1)=G. vptr(1)vptr(1')reach(H,1"1') 2.f11Da（w,them:卜1cGs11DG(w. H(1)=1"VH(1+4)=1“ (NEXT) Most of o]r separ at on logsc lemmas follow tie reach(H,1,1') frame-r]lestyle to s pport local reasonag.For exam- ok-val((S,w)ewE ptrs→日∈5 ple,tie neversal gl ant 9 cat on of tie leap predscate w ok fld(S,1)w.(ok val(5))+1 m Lemma 2 ens]res ti at a local 1eap pdate never af- ok_obj(S,1)ok_fld(S,1)*ok_fld(S,1+4) fects tle rest of tle leap.We also se tis kmd of leap objhp(S',S)vS.ok_obj(S') predscate q ant 9 cat on m o]r spec9catsons of tie col- lector to aci seve lo cal reasonmg a s 2-proced]res. ig.9.Sp ecific atit]i]t6rfa6. Lemma 3 (Object Heap Reachability).If1 3 Specification obj-hp(pp),1∈p,and reach(b1b1,them1∈p. By vat]e of tle objhp predscate,we can avosd tle We present m t1s sectson tie S[AP specs9cat on of pro2lem caj sed 2y tie poss2le cyclsc laks m tie o2ject tle collector we proved.Fast,we gave tle reaci a2dty 1eap wien tie reach predscate ss darectly sed.T15 predscate on wiscl o]r spec59cat on 5s 2]t.Tien,we 2ene9t greatly sampls9es o]r ver9catson of tie mark model tie collector's 1eap wati separatson-logsc-2ased pl ase of tie gar2age collect on. leap predscates.Fmally,we gave tle speccatson of tle collector's mterface,tle alloc prooed re. 3.2 Collector's Heap Tie o2ject leap m tie collector's leap layo]t (de- 3.Specification Interface scr52ed a S]2sect on 1.1)s formal:4ed wati tie obj_hp predscate mtrod]ced a tle prevo]ss 2sectson. We de9ne m Fg.9 tie 1eap conceptsons tiat sio]ld 2e consstent 2etween tie collector and tle m]tator. Tie rest of tie formal:4atson of tie collector's 1eap lssted m Fg.10.Tie free lsst ss md]ctavely de9ned 2y Tle constant address null set to 2e 0,wi de tie lower and]pper 2o]ndarses of tie collector's allocata2le 1eap, tie set of free o2jects.Tie leap ti at storag tie mark 2sts 1 for an o2jects set p 5s specaed wati mbits(pbl), st and ed,s1o ld 2ot1 alggn to 8,wi5cl 5s tle s4e of a wl scl asserts tlat tlere 5s a mark 2t 1 for eacl mem2er 1eap o2ject.A val]e 1 s a valsd pomter (vptr(1))only 0 of p at tie address (ed+(0 a st)c2).Tie mark stack f st s tie address of an allocata2le 1eap o2ject. Tie reacia2sty predicate reach(b1bl md]c mstk(plobjr)ss represented 2y a contal o]s memory area,witi tie lower part contamag pomters to a set of tavely de9ned.In tle 2ase case,a valsd pomter 5s self- reaci a2le.And m tie md ctave case,1 reaci a2le o2jects.Tie collector's record gcinfo stores tiree pomt- ers to tie collector's mternal dat a str]ct]res.flist(Cp) from 1 f it ss reacl a2le from tle pomters m tle leap o2- and mstack(Clp)are sed wien tie pomters are loaded ject at 1.Tie predscate rchrt(}bl)asserts ti at 1 pomts to tie correspondang regesters.Tle free lest 1eader 5s to a lave leap o2ject (reaci a2le from tle root)m tie stored m It,and tie stack pomters (lor,bol and buf) state }For tie sake of samplscity,we conssder tie case are stored a If,1 p and 1.. of a sagle root regsster 1 a,wi 5c1 can 2e extended to s]pport more root reg sters watio]t m]ci daffic lty. Tie 1eap predscate obj-hp(pp)m Fg.9 asserts an 3.3 Specification of alloc o2ject 1eap wtl reacl a2dty mformat on.A val e G5s We formal4e tie S AP specs9cat on of tie collec- valsd wsti a pomter set p (ok-val(pG))sf st s estier a tor's mam proced]re alloc m Fg.11.Tie precondst on mem2er of p or a non-pomter valj e.ok fld(p bl)asserts pVSTs de9ned m terms of tie predscate gc_inv.Tie

Chpe-t iao Lie hotE,areast ColltFbr l trirlaloe or vroos-CarrhieS Coot 4(y firpf cdkjrkcf df m)-e(,f,eta lppgrfp falf fag ludclff jgcf aglp f Hpurp 1 kgF d2jgcf lf r aaP OfagrFepgr 12ug d2jgcf pgf Ride cdmpdpgo df fag ludclfgo d2jgcf fce pempuy fdrmgo 2y gxfgkoekc f Fefa 1 kgF d2jgcf pgf B lko fag frgg d2jgcf pgf t Pb ag fdudF kc fFdaglp df fag frgg vpf ep kdf gmpfy k rP pr dpdpefedkp gkprrg falf fag aglp cdkflep lk ludclfgo A mrflfdr prderlm 1ccgppgp dkty fag uevg plrfp df fag pr2aglp fr 1 frgg tepf Fefa aglo lf etr lk gmpfy mlrk ludclfgo d2jgcf aglpP A prdpgr ppgceficlf edk df 1 mrf pflck lko fag rgcdro df pdekfgrpPb ap flefafruy fdudF p flfdr dkty lppgrfp fag vlurgp dr olfl pfrrcfrrgp dk fae fag aglp ulyd血fk8e2P pr2aglpP Skkcg fag crlrlkfgg g,(I gkprrgp falf fag uvg d2jgcf aglp prgpgrvgo 2gfFggk fag gkfry/rgfrrk eq()gλ'H'=H pflfgp df fag cdugcfdrr fag vlueefy df lky mrflfdr pog ppgceficlf edk p prgpgr vgoP Ik faep pgkpgr drr Gm ppgcf flst(1)!(1=nul) ficlfedk p pfrdke gkdrca fd prgpgrvg fag plfgfy df lky flst1,{US)1≠nul)*31'.1→-，1'*flst(1',S-1) cdmmdk mrflfdr prdcrlmpP Ndfg falf fag ppgceficlfedk hdr(1)(ed+(1-st)/2) c evgk agrg 2lpgo dk fag flcf falf 1 mlrkfpFggp cduf mbits(S,n)ES.hdr()n gcfdr kgvgr mdvgp d2jgcfpr farp ef ep kdf pref12 fdr 1 cdpyekc cdugcf drbag rglogr mly fiko 1 ppgceficlfedk array-set(1,0)emp fdr 1 cdpyekc cdugcfdr ulx\P array set(1,wUS)array -set(1+4,S-w) buffer((1,1')gfx∈{|xmod4=0A1≤E<1'}.xH 4 Proof c onstra ction mstk() bag SmAP Fgufdrmgokgpp prddf df fag cdugcfdr ep !(y-x=size(S))array-set(r,S)buffer(y,2) cdkpfrr cfgo lp fdudFpP 8dr glca prdcgorrgr Fg firpfty gcinfo(1,11,12,1g)4g1→11*1+4→12*1+8→13 fdrm 1 udclu cdog aglp ppgceficlf edk C2y cdmpdpeke flst(RS)flst(R(t5),S) fag ppgceficlfedkp fdr luep cdog 2udckp lko fag prdcgf orrgp ef clupP b agkr Fg cgkgrlfg fdr glca cdog 2udck mstack(R,S)mstk(S,R(t3),R(t2),R(t4)) e fag HRG ear lko 2r e fager Fguifdrmgokgpp prddf rpekc b agdrgm 2P Fg.10.Auxfary heap defo)s. Affgr vgr yekc glca prdcgorrg Fefa fp udclu VFg prm rp fag ppgcdficlfedkp fd fdrm 1 cud2lu VpP Wefa gmml 1 lko fag edp rry k 8e 16r Fg prdvg fag Fguf gcinv((H,),Hr,1)F1o,1. fdrmgokgpp df fag cdugcfdr'p cdog aglp F fa WpPA mrf BUF=ptrs A flfdr vgrefigo k SmAP clk fagk ukk fdfa cdog aglp Hed()flst(1.F)mbits(ptrs,0)* fardrca.gmml 1 lko fag edp rruP mstk(0,1p:16:1t)gcinfo(R(t1),1p,1t:1t)A bag frecky plrf df fag prddf cdkpfrr cfedk fd ficrrg Hr I obj_hp(ptrs,B) drf fag cdrrgcf ppgceficlfedk df fag cdugcfdr'p kfgrklu saved-regs e (0.s7,ra,to,t1) cdog 2udckpP Wg prgpgkf fagpg ppgceficlfedkp k fag fduf udF ekc pr2pgcf edkP Affgr falfr Fg 2rfly opcrpp fag reg-ok((H,R).()e vr saved_regs.R(r)=R'(r) fagdrgm pr dvikc epprgP Pawoc.1gc-inv(S) goe世XS,S.reg-ok(S,Sy)A 4.1 c or e Heap Specification H.1e-gc_inv(S,H,1e）→3,1.gc_inv(S,H',1)A b ag SmAP ppgceficlfedkp df fag cdugcfdr'p cdog 2udckp (1:=0→3Hr.dom(Hr)={1,1+4|rcht(8,1)}A fdudF fag plffgrk df ,cs,g,csa k 8 F1P Ukflmaf H非eq(Hr)*trueA er rglogrp mly jrpf cgf fag cgkgrluegl ckpfglo df c dekc 旺'eq(HT）*SR(0)→-，-）N fardrc a fag cdmpugx ppgceficlfedkp 8epP12~1xP (1:≠0→旺eq(H)*S.R(v0)→-，-) Wg rpg fag fdudF ekc padrf alko fardrc adrf fap pgcf fedkPee ilp,pC,c a lppgrfp falf lky rgc opfgr Faeca ep kdf 1 mgm2gr df fag rgc opfgr pgf c p ogkf ecluk p lko F.11.llector spec ficat) p PdoLHt a lppgrfp falf fag ltdclf12tg aglp 2drko f bag crlrlkfgg g,(cdmprepgp fFd plrfpP Ik fag Irgp Irg udlogo ekfd fag cdrrgppdko ke rgc fgrp e p P firpf plrfr iom,ra lppgrfp falf fag MIPS cluggf Wg pf drg d k Ca lko oL k CyP plvgo rgc pfgrp Ga fd c7r lko nCar fdegfagr Fefa fag rddf rgc efgr ta lko fag rgcdro pdekfgr tyr Irg egkfeclu eei啤，p9,can年c中aa=paa k fag fFd pflfgpP doLH a p Caa=d Ap ccya=oLd bag pgcdko plrf lppgrfp falf m)-e(prgpgrvgo r lko r If fag frgg uopf ep gmpfy t Oa lf fag gkfry Mark Stack OLDrations.Wg padF fag lppgm2ty pflfg df Ceeobr 1clr21cg cdugcfedk Faurgmdvg luurkf cdog Fefa ppgceiclfedkp df fag pflckfrgulfgo prdcgorrgp rglcal2g d2jgcfp k f Pbag ludclfgo pr2aglp f c lf fag Gic_hPr tyr r fich lko r or a 8 e F2P Elca prgcdko efedk rgfrrk pf lfg farp cdkflckp gxlcfty fag rkfdr cago wvg d2f cgkgrluy lppgrfp falf fagrg ep 1 mlrk pflck ek fag gkfry

0 , , , , # ! ! ! % % # ! 1#8# ! 42 3; 9 ! 44 9 ! # * A*"& ! ! # # * G B ! , # ' , ! , # (! ' ! ! , # $ , # $ # & , ! D # * ) # > %! , # 3?;5# . ) &$" ! !# 1 ! % # ! % ! 8# $ ! ! # / ? 1#< ! ! 2 ! # $ &$" % ? # % 2 %# / ! # $ ! C # . &' #' &$" 2 % ! 1#??# H , ' 1# ?8?;# / ! # ! # # / # G G G G G $ % / ! ! % 1#?8# I % %

4.T r(Coc fpl yli(fi btHeo/wP aP.AAkwl ol..wSo(x state.Tie gl ar antees ens re tl at f tie precondit ons asserted 2y tie obj-cp predscates on are satss9ed,tie mtended operatsons on tle stack are In tie mark loop,a croa o2ject s popped ato vG performed.Note tiat tie neversally ql ant ed 1eap and tle code 2locks ronva and Vdefinc examme tle predscate G m tie gl arantees ens res tie frame-r]le two 9elds of t15s o2ject.Tle predscate mftnmakes no style lo cal reasonmg. dafferent ti an min Aexcept for splattang o]t tle o2ject m MOrk Op Oiject.Tie Int roduc proced]re s also vCfrom tie crOa o2ject set t.Tie predscate mtnogoes slown m Fg.12.Tie precondtson iheCreq]ares ti at one step f]rtier 2y assertag ti at sf tle 9rst 9eld of tie eitier tie arg]ment R(IC 5s a non-poater valj e,or tie o2ject m vCs a valsd poater,st will poat to a marked 1eap predscate cont ams eno]gi aformat on for clecmg o2ject.Tie call to ~Int-roduc m Vdefinc ret]rns to tle mark 2t of R(IC)and performag stack pl s1.Tie ufifil,wlere we can safely move tle o2ject m vCato g]ar antee eheCyens res tl at tie proced re only mods tle b40ck o2ject set c and get minAagam. 9es a few regssters f tie arg]ment R(IC)s a non-pomter Tlere s no more crOa o2ject on tie ret]rn state of valj e or a pomter to a marked o2ject.Otierwsse,eheCInt.Ti]s we get a closed s 21eap m H-formed witi gl arantees tiat R(IC)ss marked andp]sied totiemark tie lave o2jects m c. stack. sweer PhOse.In Fg.14,we specy tie 9rst two code MOrk Phose.We slow m Fg.13 tie code 2locks a- 2locks of V.ddl m tie same way we speciy tie Int plementag tie mark pl ase of tie collectson.Tie spec- code 2locks.Tie predscate ipg,on tle entry state of 9catsons of tlese code 2locs follow tle same pattern. V ddl s d fferent from mpotnonly m ti at we move tie Eaci precondt on asserts ti at tie correspondag state 1 nreaci a2le o2jects o]t of tie allocated s 21eap H predscates (mpg,minA mftn or mtno)s satss9ed.On In tie sweep loop avarsant tinAt stands for tie o2- tie otier 1 and,eaci g]arantee ens res ti at f tle corre- jects 2efore tie sweep pomter m IC Tie nreaci a2le spondag state predscate s sats9ed,tieInt procedj re o2jects m t are collected mto tie free lsst wati set o, wall ret]rn on a state sat sfyag mpotn and tle mark 2ts of tle reacl a2le o2jects m t are set On tie entry state of mark,as asserted 2y mpg,, to 0.Fmally,t 2ecomes a s]perset of pigt wlen tle all o2jects are allocated and tie leap 2o]ndares are sweep loop 9nss1es.Ti]s all tie nreacia2le o2jects loaded mto tie correspondang regesters.After mark- wall 2e collected ato tle free lest,as asserted 2y tpotn mg tle root regsster ag we reaci tle state wlere tie Tie otier two code 2lock spec9cat ons are samply gen- mark loop myarsant minAiolds.Followag tie trscolor erated 2y tle dp f nctson m S 2sect on 2.2. a2stractson minAasserts tiat tie o2ject set prgt ss Co44ector.Tie rest of tie codes,mcl dag tie Le davsded mto tie sets of b40ck,croa and white o2jects, proced re andtie Iuufie proced]re,are siown m Fg.15. wi scl are separated 2y tlea mark 2ts and tle mark Tie speca9catson of Le 5s a travsal composat on of tle stack.Tie b4Ock and croa o2jects are reaci a2le from Int and V.ddl specs9catons.Tie g]arantee eic as root,and tle reaci a2dty 2etween tie tiree sets are serts ti at tie reaci a2le s 21eap Hs preserved dj rag is_empty:(pEMP,EMP) push:(ppusH,OpUsH) pop:(Ppor,9por) mark_field:(puruD 9MPD) beq $t3 $t2 empty2 addiu Sat $t2 4 addiu $vo $0 4 sltu $t9 $a0 $ko srl1 Sat $at addiu $vo $00 sltu Sat $t4 $1 subu $t2 $t2 $vO bne $t9 $0 return addu Sat $at $ki jr $ra bne Sat $0 stk_loop 1H$v00($t2) sltu $t9 $ao $k1 lw $t9 0 Sat sW$a00($t2) jr $ra beq $t9 $0 return addiu $v1 $0 1 empty2 addiu $t2 $t2 4 subu Sat $a0 $ko beq $t9 $v1 return addiu $vo $0 1 jr $ra stk_loop: andi7 $t9 $at sw $v1 0 Sat jr $ra j stk_loop bne $t9 $0 return j push ).mstack(B5)*true PMPLD::=(H,).sted_ok(R)A pA(,R,(,R').3n.(,R')=(m,R{v0nM -vptr(R(a0))V V.S.Hmstack(R,S)*true vptr(R(a0))A 3G. (m=0→S=0Λ(m≠0→5≠0) ((a0)E GAH I mbits(G,1)mstack(R,G)true)v egA(H,R).aS.R(a0)年SAH非mstack(R,.S)*true (R(a0)生GA grvn)).nin-rid(at)) mbits(G,1)mstack(R,G)*hdr(R(a0))-*true) VS,A.H mstack(R,S)*A gru:=(),().nin-rid(R(t2,v1,at,t9)) mstack(R',S+R(a0))*A (-vptr(RR(a0))V H(hdr(R(a0)))=1 pror().mstack(R,S)*true H=HA R(t2)=R'(t2))A grow),().nin-rid((vo}) (G,A.vptr(R(a0)》+ S≠0，A.Hmstack(R,S)*A+ Hmbits(G,1)*mstack(R,G)*hdr(R(a0)→0*A→ '(vo)E SAH mstack(R',S(vO)*A H'mbits(G +R'(a0),1)*mstack(R',G+(a0)A) Fgd20Assnmbly codnw tg sprc ficat &zs:stack azd StckLCeIdo

0 ! " #$$%! ##! & ' # % # > . # $ % & ! 1#?8# . % % % # ! % ,# (! % % %# $ / ! 1#?9 % % # % ! # I # ( ! # ( % , # $ % ! ! % # 1 ! , ' , ! % % %# , ! # * % , % ' ! ,# % - ' , , # , ! % ,# ! ! , , # , # ! ! , # ' * 1#?: ! ! % ! ! %# - ! , # * ! , ! # , ! % , B# 1 ! ! # , ! # ! % & 8#8# ! 1#?;# # ! 4* 996 7 99. 9?

markfi eld.k ht er lg lco mdllot bdc uooef t lbedk pdc voddpfin lccpekc m dno mark:(PMARK:9MARK) mloop:(PLOOP+9ooP） mfirst:(Pupsr,9Msr) msecond:(PMsD:9MsxD addiu $t6 $ra 0 jal is_empty mloop2 1H$a00($v0) 1w$a04($v0) addiu $ao $to o mloop2: jal mark_field msecond jal mark field mloop jal mark field mloop bne $v0 $0 return1 jal pop mfirst S.3,A.mpre(S,且，A) mpre((HR),),A)sted_ok(R)A hS,'.(VH,A.mpre(S)mpost()) HIeg(H)*mbits(ptrs,0)*mstack()AA nin-rid({t6,a0,at,vo,t9,t2,vi],S.R,S'.R) Hobj-hp(ptrs,ptrs) Pnoor A.minv(S,H) minv(阻，R),H,A)些B,G,W gooeS,S.E,A.minv(S,H,A)→mpost(S,丑，A)A sted_ok(R)A BUGUW=ptrsA nin-rid(fra,t6,a0,at,vo,t9,t2,v1,S.R,S.R)A ok_val(BUG,R(to))A (Vr E(BUG).reach(,R(to),))A S'.R(ra)=S.R(t6) Heq()mbits(B UG,1)mbits(WV,0)mstack(R,G)*AA Pursr.mfst(S) Hobj_hp(BUG,B)*obj_hp(ptrs.GUW) gursrAS,S'.(VH,A.mfst(S,HA)mpost(S',H,A)) minv2((H)A,S1,S2,B.G,W) nin-rid((ra,t6,a0,at,vo,t9,t2,vi],S.R,S'.)A sted_ok(R)A BUGUWU{R(v)}ptrs A S'.R(ra)=S.R(t6) ok val(BUGUR(v),R(to))A Passo AS.A.msnd(,H,) (Vz E BUGU (vO).reach(H,(to),))A usDgλS,S.(VH,A.msnd(S,H,A)→mpost(S,H,A)A Heq(H)*mbits(BUGU{R(vO),1)*mbits(W,0)* mstack(R,G)*A)A ninrid(fra,t6,a0,at,vo,t9,t2,v1),S.R,S'.R)A HI objhp(BUGUR(vO)),B)*obj-hp(ptrs,GUW)* S.R(ra)=S.&(t6) ok_fld(S1,R(vo))ok fld(S2,R(vO)+4) mpost ((HR),A)3B,W.sted_ok(R)ABUW =ptrs ok_val(B,R(to))A (Vr E B.reach(,R(to),r))A mfst(,)BG,W.minv2(,H,A.ptrs,ptrs,B,G,W) eg(H)mbits(B,1)mbits(W,0)*mstack(0)*AA msnd(S,,)3B G,W. Hrobj_hp(B,B)obj_hp(ptrs,W) minv2(S,H,A,BUGUS.R(vo),ptrs,B,G,W) welj Lbss ame gdna V lil ss aglg)Kdss qst ckL 8geep:（(PswEEP,9 SWEEP】 s1o0p:(PsLooP,9sooP】 sadd:(PsADD:9sADD) snext:(PsNxT,9sNxr) addiu $ao $ko 0 sltu Sat $a0 $k1 sw$t54($a0) addiu $ao $a0 8 1w$v00($at》 addiu $t5 $00 beq Sat $0 return addiu $t5 $a0 0 jsloop beg $vo $0 sadd j sloop subu Sat $a0 $ko srl1 Sat $at 8w$00(3at) jsnext return1: return: addiu $ra $t6 0 addu $at Sat $k1 j snext jr $ra jr $ra wrS.A.spre(S spre((R),)3B,W. w nin-rid((a0,5 at,vo). sted_ok(R)A BUW ptrs A VH,A.spre(S.A)spost(S',H,A) ok_val(B,R(to))A (Vr E B.reach(Hr,R(to),))A Pwoor S.A.sinv() eq()*obj-hp(ptrs,W)*mstack(0)s mbits(B,1)*mbits(W,0)*AA sooS'nin-rid((a0,5 at,vo.,)A H I-objhp(B,B) VH,A.sinv(S,HA)spost(',HA) sinv(阻，R),Hr,A)gB,W,E,G. (pxTx wp(sloop(pLoor,Loo,Ixr) sted_ok(R)A ok_val(B,(to))A (PSADD:9sADD)wp((psxxT 9x)},IsADD) G={zE ptrs Ar<R(a0))A spost((H),A)B,W.sted_ok()A BUW ptrsA WnG=0A F C GA(R(a0)-st)mod 8=0A ok_val(B,R(to))A (Vr E B.reach(R(to),))A BUWU F ptrs A (Vc E B.reach(H,(to),))A eq()*flist(R,W)+mbits(ptrs,0)*mstack(R,()*AA HIeq(H)*obj_hp(ptrs,W)*flist(F)*mstack(R)* Hr obj_hp(B.B) mbits(W UFU(BG),0)*mbits(B-G,1)*AA Hr I-obj_hp(B,B) we五VLbssam∈B gdma vihl s sagCg)d径gutwwpL

4 h.1 cmpnm SFi.Ifilt ca,Mas 2007,wca22,Nc.3 gc:(Pec,gec) alloc:(PALLOC,9ALLOC) retp:(PRETP:9RETP) aloop:(PALOOP,9ALOOP) addiu $t7 $ra 0 addiu $t8 $ra 0 addu $t2 $0 $t3 addiu $ra $t8 0 beq $t5 $o loop jal mark gc2 addiu $ko $o st 1w$t58($t1) addiu $vo $t5 0 jretp 8c2: addiu $k1 $o ed bne $t5 $0 retp 1m$t54($t5) loop: addiu $ra $t7 0 1H$t30($t1) jal gc aloop s$t58($t1) j loop j sweep 1m$t44($t1) jr $ra Poe.4.gcpre(S,H) (pr,9)wp(),IErp) goce S.S'.(VH,A.gcpre(S,H,A)gcpost(S,H,A))A (pALoP,wp({loop(AS.True,S,.False), nin_rid(t6,t7,t5,a0,at,vo,t9,v1),S.RR,S'.R) retp (PRETP:9RETP):IALOOP) gcpre((L,R),旺r,A)mpre(l,R{t7R(ra)),皿，A) gcpost(S,H,A)spost(,)AH eq(true Fa.16.2 sslmclp comlwae sp lcaucat aors:ge armdmn-e tg h-ffght-CP TCg pyghifiheth-Cp -f.alltc lp flptgo IC P-qyy-Ylogp e ylhC fe Cc necg F ChC lp e Afg t-ogfiCg FIc H1r e Co tCg -tCgy pyghifibeth-Cp eyg cgCgye tgo Ay tCg A-tC folhe fi e Co h-v ynteth-Cefi tgyv p nplCc IConht 17g ro fn ChtCP h-Cptynht-yp e Co yettgycv ethClCe P4 It CtClp fe Ce necgr Fg An lfo tCg e Aptye ht v ehCCgr t SPAP ynfg pgtr e Co q(e:Pr∈ETc正WISf -tCgy h-v y-CgCtp f-y pyghifyICe tCg h-ffght-yP TCg-ygv yy-7ICc IC P-q lp c-efto lyghtgo e Co te htthH 4 ItC t VP GgC IC SnApght -C 2F2r tCg Fgff Ae pgoPA pgt -f.yygogfiCgo te htlhp lp yy-7logo t-p-f7g tC f-yv go Cgpp yy-fp -f.t h-og Afi-hkp eyg h-Cptynhtgo yy-f.c-efpP TOp IChfinogp tCg Aeplh te htthp fikg appl FItC-nt tCo lyght npg-f.SP AP ynfgpPICptgeor tC v eIc pIcrt e Co slpmr FChC tye Cpf-yv tg c-efi ehh-yo ICc olffihnfty ICtCg yy-f.h-Cptynhth-C lp t-p-fi7g tCgo-v eIc t→tgh-ygpy-CoICe PP tyy ICe ynfgp;eC aCet teh止 pyghifin yy-Afgv PF-y-ny h-ffght-y 7gylfibe th-CrtCg yy-A tihr FChC tylgp t-eyyfy yyg7h-np fgv v ep oghfe ygo ep fgv lp t-yy-7g tC-pg yy-ygyt lgp e A-nt tCg fiCitg pgt e Co OCtp;eCo pg7gyefi yygogfiCgo te htthp ygy ygpgct ICe p-vg tCg Cgey yygo lbe tgr ep tCg pyghifiheth-Cp eyg v e lCfy h-Ch Fgffrgpte Afilp Cgo oghlph-C yy-hgo nygpr pnhCep tCg tmsfa ptynhtgo FItCeppgyth-Cp eA-nt tCgv P te htihr FChC p-f7gp e c-efi IC PygpAnycgy eylt C gtlhP A 4 g tehkfg tOp yy-Afgv Ay AygekICe tg yy-f h-Ch tehtih fe Ce necg lp efp-yy-7logo t-Anlfo npgytogfiCgo ptynhth-C ICt->tF->ptgypP Flyptr Fg yy-7g ep fgv v ep te htlhp nplCc yettgyc v ethCCc-C yy-fc-efpr yghnypl-C tCg h-v v-C yy-ygytlgp -f tg fiCitg pgt e Co tg Cgey eCo -tgy yy-oyev v ICc fehlfitlgpP Ony tehtlhp f-y tC yygo lbe tgr pnhCep tCg Icty-onhth-C/gfilv ICeth-C ynfgp-f. fiCitg pgt eCo tCg Cgey yygo lbetg eyg ogfiCgo nplce tOp tCg pgt -ygyet-ypr e Co tg epp-hleth7g/h-v v n Clbe th7g fe Cc necgP yy-ygytigp -f.tCg pgye yetiCe h-CanChth-C *P TCgpg eyg Ic tCg f-ff-FCc yeyt -f.tCp pghth-Cr Fg Iffnptye tg h-ffghtgo IC tF-fgv ve filAye ylgp f-y tCg fiCitg pgt eCo -ny -q lv yfgv gCteth-C v gt C-o-f-oy FitC pg7gyefigxH tCg Cgey yygo lhetgP t-tctg ficitg pgt e Co tg Cgey ev yfgp:tg ptetg tye Cplth-C fnChth-C f-y h-v v e Cop IC yygo lhetg h-Cte IC C-CHtyl7lefiIConht I7g ogficiti-Cp CChg tCgeAptye ht vehCgr t SP AP yng pgt f-y Fgfflf-yv go It lp ICfgeplAfg t-lv yfgv gct fnffy ent-v etih oghlpl-C ICptynhtC pgqngChgr tg ro fn Chth-C hC VP GgCr e Co yy-hgo nygp f-y glt gy -f.tgv Pt-Fg7gyr tCgyg eyg ptiffi e npgyhogficgo teht ih f-y p-f7ICe c-efp FItC Cgey yygoH ve Cy yettgyCp IC nplCe tCgpg fgv v ep onylCe -ny yy-f. Ibe tgpP ICtgygptgo ygeogyp v ey cgt v -yg ogte lfp -f.-ny h-Cptynhth-CP F-ff-FI tpg yettgyCpr Fg ogplc C en P-q lv yfgv gCteth-C fy-v P t-v etih te ht lhp t-plv yfify tg yy-f.h-Cptynhth-Cr ec gxev yfg -f.pnhCte ht lhp lp pCC IC tCg Cgxt pght -CP 4 ItC tg Fgffhogplc Cgo o-velC py ghifih fgv vefl 5(Cg∈HdoFIIRS HEBT el REt Aye ylgpr tg Fgffff-yv go Cgpp yy-fp -f.tCg h-6g Af-hkp TCg Is,cc fnChth-C IC Flc I5 lp ogfiCgo IC SnApghH eyg h-Cptynhtgo FItC gepgP th-C sH ep tg pv effi ptgy ptetg tye Cplt-C ygfet-C f-y h-v veCopP It lp lv yfgv gCtgo ep e fnChth-C FItC yetH 5）RF CTx,∈T∈SIHS tgyc v ethClCePTCg tecp pnhCep htms eCo Nt Is -C tCg ygtnyC 7e fing -fpnhCfnChth-Cp eyg tCg h-Cptynht-yp -fe C Ony 7gylfibe th-C lp fnffy v ghCe Clzgo FIt Oc tCg P-q -yth-C tyygr flkg tpcpt I scacs ICtCp fnChth-CP A 7efng yy-f.epplpte PP-q lp eC KCtgye ht/7g tCg-ygv yy-7gy FItCe C-yth-Ctyyg lp gitCgye v ge CICe fnfiTefng FItCtCg Aepgo -C tCg f-yv nfeghepltyyg C-tl-crertr FCgyg t tec htmsr -y e Aeo Tefng ygy ygpgCtgo Ay Nt IsP F-y gxH ygv p eCo yy-fp eyg h-Cptynhtgo IC PIP ep tyygp eCo ev yfgr e Nt Is ygtnyCgo Ay tg Cgey ygeo fnChth-C.fs c tgyv pr ygpy ghti7gfyP Py-f.hCghkiCe IC P-q lp tCp tyyg pte Cop f-y e Aeo Cgey 7efingr FOfg e NtIs ygtnyCgo Ay hCghklCe -f.tgyv p IC PiPr FChC lp plv yfg t-v yfgv gCt tCg yy-eyev ptgy fnChth-C pte Cop f-ye ptnhk yy-eyev P e Co v -yg tynptF-ytCy tCec tCg v gtC-o-f-elgp npgo Ay 4 g lv yfgv gCt tCg SPAP Fgffif-yv go ICptynht -CpgH tCg -tCgy pyptgv p fikg PVSP qngChg ynfg pgt ep e yghnypl-C fnChth-C F ChCygyf-yv p

00 ! " #$$%! ##! & ' ! 4< 996 7 99. # 1#?? # . " / / 7) & 8#8 ! % ! &$" # * Æ # 1 ! # / % % ! # 1 ! D D , # ! # # ! # 1 ! ! ' ! ' # / ! ! % ! # 0 1 ' ( 0 ! . # . ! # " % . % ! ! % "7&# . ! # / ! &$" # . # $ # % ! @ ! @ ! ! " # $ # ( # * ! ! . ! ' + &$" ! . 7) ! # * . 3?85# 0 1#?< & 9#? # * ! # ! % # $ ! ! !# 1 ' ! ! ! % # / &$" ! . !

markfi eld.k hotr lg lco mdllot bdc uooeft lbedk pdc v oddpfim lccpekc m dmo 4(5 patterII matcCillg oll tCe illstrSctioll seqSell ce alld reH block. tSrIIs differellt proof obligatiolls based o tCe rSles ill We bSild a tactic g4[,ags,tCat aStomatically Fig.6.TCe (fSII ctioll ill tCe VCGell follows te same matc Ces all d elimill ates tCe idelltical or trivial parts of patterl to gellerate tCe correspoll dillg specificatioll s. tCe Ceap predicates iII tCe Cpot Cesis alld proof goal, leavillg tCe differellt oles for mall Sally provillg.For Definition nextc (c:comm)(s:state):option state : example,tCe followillg goal is trivially provable witC match c with g4[,ag5,· addu rd rs rt = Some (rset s rd (rget s rs rget s rt)) ph,A,B,b dAw Bwb w emp bb w true wBd III most of tCe cases,a code block cCallges ollly a lw rt offset rs = small part of t Ce Ceap.TCis tactic alleviates Ss from match (hget s (rget s rs offset))with complicate reasollilg,alld greatly redSoes te proof Some v =Some (rset s rt v) None =None script si5e.TCe prillciple of g41,ag5,is to regard tCe end Ceap predicates ill te goal alld ypot Ceses as two lists, end. alld prove tCat ole is a permStatioll of allot Cer Ssillg Fixpoint scap_iseq_ok(P:chspec)(p:pre) tCe classic algorit Cmn.mSrillg tCis procedSre,tCe idelH (g:guar)(is:iseq)(struct is]:Prop : tical parts are elimillated Ssilg tCe mollotollic lemma of match is with separatillg colljSIctiol.TCe rSIIig time of t Ce tactic jr r31 =forall s,p s->g ss is boSIded by tCe si5e of tCe Ceap predicates. Punes Component seq c is'=>exists p',exists g', (forall s,p s - 81Z Baslc propert les anv tact(cs match (nextc c s)with 138F hrverev heap tbrary 451 |Some s'=>p's'八 Abstract mach ne encov ng anv temmas 11z3 hrverev finte set tbr ary forall s",g's's"->g s s" 844 Separ at on tog C tbrary None =False 54F SCAPi CGen anv retatev tact cs end)/scap-iseq-ok P p'g'is' 519 Cottector's heap vefin tons anv temmas end. 1930 Coveispec ficat (on anv prootot the cotector Fixpoint wp(P:chspec)(is:iseq)fstruct is option (pre,guar):= Fg.1E.Proot scr pt sZe. match is with We also implemellt ot Cer aStomatic tactics for reaH jr r31 =>(fun s=>True,fun s s'=>s=s') sollilIg aboSt Ceap lookSp all d Spdate,tCe mallipSlatioll of fillite sets,aSto rewritillg oll complicate states valSes seq c is!=> geller ated by VCGell alld so oIl.TCe detailed examples match (wp p is')with of tCese tactics call be foSId il 12]. Some (p',g')=>Some (fun s=> match (nextc c s)with Some s'=>p's'None =False 533 Evl lnl vopz end,fun ss=> Fig.17 lists tCe proof script si5e of oSr Cog impleH match (nextc c s)with meltatioll,ill terms of tCe IISmber of Iolllempty lilles. Some s'=>g's's"None =False end) TCe work takes several mall molltCs for programmers None =None familiar witCtCe Coq system.TCe illtell sive Sse of aSH end tomatic tactics alld tCe VCGell resSlts i as/4 drop of end tCe proof script si5e all d makes tCe proof mScC easier to follow.TCe bellefit of tCese facilities is also demollH Fg.1z.Co;(mp tementat (on strated by oSr evalSatioll oll tCe CmSA example ill [5]. TCe I laadg P55 fSI ctiolls are verified wit Gll two days 5 Tl,ugy fp.p nupml vopz by a sillgle per soll,wCile eacCproof script Cas a lelIgtC of ollly 1/6 w Cell comparillg to tCeir origill al olles. TCe most complicated part of tCe collector's proof OSr implemelltatioll relies Ceavily o tCe Coq stallH lies ilI Ceap mallipSlatiol witC separatiol logic,tCat is dard library.We also extelld tCese libraries wit CvarioSs to say,to prove tCat olle propositioll witC Ceap predi lemmas alldtactics.TCe Ceap model all dt e filite set is cates implies allot Cer.For complex Ceap predicates witC desigled witCt Ce ideas ill [17],wCere a Ceap/set is a list mally separatilg coljSIctiols,like tCe olles melItiolled of data (as i tCe Coq.4gB5B library)toget Cer witC ill SSbsectioll 4.1,tGis will be ellormoSsly difficSlt SsH a proof tCat t Ce list is welllordered all d witC Io redSII illg ollly tCe commSIicative,associative alld mollotollic dall cy.TOSs we obtaill tCe Ceap/set extell sioll ally from properties described ill 6].UsSally CSIdreds of lilles tCe Law of ExclSde Middle,all d tCe Cxpoint fSI ctiolls are leeded to prove olle sScCgoal,all d it is Iot SIcomH oll sets,sScC as tCe iterated separatilg colliSl ctioll all d moll to el coSlIter sever al sScCgoals ill provilg olle code tCe mark stack predicate,call be bSilt witCease