Garbage collector verification for proof-carrying code

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<ST 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;addr<ED;addr++) a11oc(){ stackpop(){ if (markbit(addr)==WHITE){ if (freeptr==NULL)gc() return *(--top); addr->first=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 969 ! < & # 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

￾     ￾        ￾ ￾  0  ! 0 & #   39 +; - " ￾ #!              "   ￾ ￾       ￾  ￾ ￾ / ' &￾$"       7￾) !    !  1#=#        %                    % #      %          ! %   .   ￾   1#<# &           ! , %      # /    !    8    ?   ￾   1#<# "  $  ! ?           @   8         +   /    7￾)  &￾$"              % # 1    %          .                 !    1#<#          '    &￾$"          %       #                       %  7￾)                      # ! 1 5 +; - % &'             !        # &    !       '              ￾ # *         &￾$"  !                    ￾￾   !  1#E#   &￾$"      !           !  # / !  ￾              ￾￾#       !   ! = &     9

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

0!  ￾     ! " #$$%!  ##! & '    3<5# 1      !                        ￾￾# /          +            F :        + #      #       ,       %   3?;5                         !           .    ! 35 # /               '   3<5     8   %    !            #   &' (' ! ?   ￾         +   G  8   ￾        +   ￾  ￾      A           !  ￾        # 1  '    .         8               # /    %    .                     # % #'    /       &￾$"        !  # 1 !       !     #  !      2  !      # 1 !         2     # %￾ #'    )  /   1#4            !        #          B !   !        2            E !   0    ,# $                      ,#        ￾     # *           # $     ￾                     ,  #               ,           # 1   %   !            !   '         !   Æ#      ￾   1#4   ,  !     # $     !                     #              ! # $   ,         !  #        ￾   ￾          ' !   ,         ! ￾ # *   !     ￾      !      !     #    !          9# ! > &    % ( *  &' +  ,!   ￾            ￾    ￾          !              %   ,  !       #          %        # %   - &'  ,      2        &   ?#?   0 !             #      0      2     1#?B#            ,#       %      ,    !    !      %              F    8#  % %                !   !          ,#    2              2   #          !            #            %               # %% #'    )  /  0  &￾$"        2      1#??#     ￾         #