Foundational Typed Assembly Language with Certified Garbage Collection

Foundational Typed Assembly Language with Certified Garbage Collection Chunxiao Lint Andrew McCreight Zhong Shaot Yiyun Chent Yu Guof Department of Computer Science and Technology IDepartment of Computer Science University of Science and Technology of China Yale University Hefei,Anhui 230026,China New Haven,CT06520-8285,U.S.A cxlin3,guoyu @mail.ustc.edu.cn yiyun @ustc.edu.cn aem,shao @cs.yale.edu Abstract Some recent research focuses on building type-safe garbage collectors to remove the collector from the TCB of Type-directed certifying compilation and typed assembly a TAL system.Wang and Appel [26]and Monnier et al.[19] language(TAL)aim to minimize the trusted computing base propose to use languages with region-based type systems of safe languages by directly type-checking low-level ma- and intensional type analysis for type-checking a standard chine code.However,the safety of TAL still heavily relies on copying garbage collector [14].But their approaches work its safe interaction with the underlying garbage collector. only with specific GC algorithms and not,for example,with Based on a recent variant of foundational proof-carrying mark-sweep collectors.The complexity of the type system code(FPCC),we introduce a general methodology for com- may also increase the TCB of their systems. bining foundational TAL with a certified garbage collector. GTAL [11]uses a linear type system to encode new types We demonstrate the practicality of this approach by link- from individual memory words.By building up appropriate ing a typical TAL with a conservative garbage collector. abstractions,GTAL is capable of type-checking a variety of This includes proving the safety of the collector,the sound- garbage collection mechanisms.Still,the new features in ness of TAL,and the safe interaction between TAL programs the type system result in a large TCB.Also,the metatheory and the garbage collector.Our work is fully mechanized in of GTAL is not mechanized. the Cog proof assistant and the certified programs can be Foundational proof-carrying code (FPCC)[1,9]can shipped immediately as FPCC packages. eliminate a large portion of TAL's TCB by mechanically proving the soundness of its type system,the correctness of the type checker,and the safety of the associated garbage 1.Introduction collector in a foundational logic.The minimized TCB con- tains only the soundness of the foundational logic,the cor- Type-safe languages such as Java and C#provide several rectness of its proof checker,and the machine model.The protection mechanisms for the safe execution of programs. recently proposed separation logic [24]also provides a pow- The implementation of a safe language,on the other hand, erful approach to reasoning about the safety of garbage col- is a complex system with many components which must be lectors,as demonstrated by the work of Birkedal et al.[2]. trusted.These unverified components form the trusted com- In this paper we present a new methodology for build- puting base(TCB).Techniques such as type-directed certi- ing foundational TAL with a certified garbage collector.We fying compilation and typed assembly language (TAL)[21] combine the general framework for mutator-collector verifi- reduce the size of the TCB of these type safe languages.By cation by McCreight et al.[17]with the open FPCC system preserving type information during compilation and directly by Feng et al.[8,7].We demonstrate the practicality of type-checking the assembly code,these techniques remove our approach by linking a TAL with a simple conservative the compiler from the TCB of a type-safe language. garbage collector [3]in the FPCC setting.This includes However,the safety of a TAL system still relies on the proving the safety of the collector,the soundness of TAL, soundness of its type system,the correctness of the type- and the safe interaction between TAL programs and the col- checker,and the correct implementation of macro instruc- lector.Our paper makes the following new contributions: tions such as malloc.Because it is difficult to certify the implementation of free in the presence of memory alias- As far as we know,the work presented in this pa- ing.TAL often requires a trusted garbage collector be part per is the first to successfully link a TAL program of the memory management run-time. with a garbage collector to generate complete FPCC

Foundational Typed Assembly Language with Certified Garbage Collection Chunxiao Lin† Andrew McCreight‡ Zhong Shao‡ Yiyun Chen† Yu Guo† †Department of Computer Science and Technology ‡Department of Computer Science University of Science and Technology of China Yale University Hefei, Anhui 230026, China New Haven, CT 06520-8285, U.S.A {cxlin3,guoyu}@mail.ustc.edu.cn yiyun@ustc.edu.cn {aem,shao}@cs.yale.edu Abstract Type-directed certifying compilation and typed assembly language (TAL) aim to minimize the trusted computing base of safe languages by directly type-checking low-level ma￾chine code. However, the safety of TAL still heavily relies on its safe interaction with the underlying garbage collector. Based on a recent variant of foundational proof-carrying code (FPCC), we introduce a general methodology for com￾bining foundational TAL with a certified garbage collector. We demonstrate the practicality of this approach by link￾ing a typical TAL with a conservative garbage collector. This includes proving the safety of the collector, the sound￾ness of TAL, and the safe interaction between TAL programs and the garbage collector. Our work is fully mechanized in the Coq proof assistant and the certified programs can be shipped immediately as FPCC packages. 1. Introduction Type-safe languages such as Java and C# provide several protection mechanisms for the safe execution of programs. The implementation of a safe language, on the other hand, is a complex system with many components which must be trusted. These unverified components form the trusted com￾puting base (TCB). Techniques such as type-directed certi￾fying compilation and typed assembly language (TAL) [21] reduce the size of the TCB of these type safe languages. By preserving type information during compilation and directly type-checking the assembly code, these techniques remove the compiler from the TCB of a type-safe language. However, the safety of a TAL system still relies on the soundness of its type system, the correctness of the type￾checker, and the correct implementation of macro instruc￾tions such as malloc. Because it is difficult to certify the implementation of free in the presence of memory alias￾ing, TAL often requires a trusted garbage collector be part of the memory management run-time. Some recent research focuses on building type-safe garbage collectors to remove the collector from the TCB of a TAL system. Wang and Appel [26] and Monnier et al. [19] propose to use languages with region-based type systems and intensional type analysis for type-checking a standard copying garbage collector [14]. But their approaches work only with specific GC algorithms and not, for example, with mark-sweep collectors. The complexity of the type system may also increase the TCB of their systems. GTAL [11] uses a linear type system to encode new types from individual memory words. By building up appropriate abstractions, GTAL is capable of type-checking a variety of garbage collection mechanisms. Still, the new features in the type system result in a large TCB. Also, the metatheory of GTAL is not mechanized. Foundational proof-carrying code (FPCC) [1, 9] can eliminate a large portion of TAL’s TCB by mechanically proving the soundness of its type system, the correctness of the type checker, and the safety of the associated garbage collector in a foundational logic. The minimized TCB con￾tains only the soundness of the foundational logic, the cor￾rectness of its proof checker, and the machine model. The recently proposed separation logic [24] also provides a pow￾erful approach to reasoning about the safety of garbage col￾lectors, as demonstrated by the work of Birkedal et al. [2]. In this paper we present a new methodology for build￾ing foundational TAL with a certified garbage collector. We combine the general framework for mutator-collector verifi- cation by McCreight et al. [17] with the open FPCC system by Feng et al. [8, 7]. We demonstrate the practicality of our approach by linking a TAL with a simple conservative garbage collector [3] in the FPCC setting. This includes proving the safety of the collector, the soundness of TAL, and the safe interaction between TAL programs and the col￾lector. Our paper makes the following new contributions: • As far as we know, the work presented in this pa￾per is the first to successfully link a TAL program with a garbage collector to generate complete FPCC

packages.The type system of our TAL contains non- trivial features such as mutable references,recursive (Prog) P = (C,S,) C types,and union types,and is capable of typing muta- (CdHeap) := {f} (State) S = (H,R) ble recursive data structures.The collector we verified (Heap) H = {1}* is a conservative variant of a standard stop-the-world (RFile) R = {r~中w}* mark-sweep collector [14]. (Reg) “= rkjkeio...31) Although our current paper only shows how to safely (Wd,Lab) w,f = 011|2|. link TAL with a certified conservative collector,our (Address) 1 = 0|4|81… methodology is general,capable of verifying more (ISeq) = c;I beqrs,rt,f;I bners:rt,f;I complex situations,such as the TAL type system keep- jf jalf,fret jrra ing complex information for an accurate collector or (Comm) C addu rd,rs,rt addiu ra,rs,w even an incremental collector with read/write barriers. subu rd,ra,rt|srl rd,rs,1 We specify the collector using the stack-based cer- sltu rd,ra,rt andi rd,re,7 1w ra,w(rs)swrs,W(ra) tified assembly programming (SCAP)framework [8] extended with separation-logic primitives [24].Our specification asserts the machine-level behavior of the Figure 1.Abstract machine syntax collector and is general enough for various mutator safety requirements besides type safety.The safety Inductive Construction (CiC)[23].as implemented in the proof of our collector,which is done using SCAP,is Cog proof assistant [5].CiC is a higher-order predicate a nontrivial work by itself. logic extended with inductive definitions.The CiC terms The work presented in this paper is fully mechanized in this paper are written using standard logical notation.We within the Coq proof assistant [5].Thus,the linked let Prop be the universe of all logical propositions and Set code of the mutator and collector can immediately be be the universe of all computational terms. shipped as an FPCC package with a minimal TCB. We have also developed various mechanisms in Coq 2.1.Abstract machine to simplify proof construction. Figure I gives the syntax of our abstract machine.A pro- In Section 2,we introduce the preliminary knowledge gram P is a triple of a code heap C,a machine state S and needed to understand the rest of the paper.In Section 3, an instruction sequence I.A code heap C is a partial map we present our general methodology for building TAL with from code labels f to instruction sequences I.A machine certified garbage collection.In Sections 4-6 we apply this state S contains a data heap H and a register file R.A data methodology to verify the safe interaction of a TAL with heap H is a partial map from 4-byte aligned addresses 1 to a conservative collector.We discuss the implementation in word values w,while a register file R is a map from registers Section 7.Finally,we discuss related work and conclude. r to word values,with ro always mapped to 0.A command Note that all lemmas and theorems in this paper are me- c is a non-control-flow instruction such as a register add or chanically proved in Coq.Their detailed proofs are avail- a heap load.An instruction sequence I,or code block,is a able on our project web site [16]. series of commands and branches followed by an uncondi- tional jump instruction.For simplicity,we separate the code 2.Basic setting heap C from the mutable data heap H.Also,we use an in- struction sequence instead of the standard pc register.This Before presenting our general methodology we give a results in the additional return address fret in the jump and general introduction to the FPCC system that our work uses. link instruction jal f,fret.By expanding this instruction This includes a MIPS32-style [18]abstract machine model to the MIPS instruction pair jal f and j fret,all our certi- and the lightweight open framework for certified assembly fied code [16]can directly run on the SPIM simulator [15]. programming [7](LOCAP),a program logic for reasoning Following [18].we give the small step operational se- about the interaction of two different verification systems. mantics of the abstract machine in Figure 2.We write X(2) We also present the embedding of SCAP [8]in LOCAP.As for the value bound to z in the map X,and Xfv}for demonstrated by Feng et al.[8,7],SCAP is suitable for the map obtained by updating the binding of z to v in X. certifying system level libraries,and we use it to construct Note that for a 1w/sw command,if the source address is not the safety proof for our garbage collector. in the domain of the heap,the next state is undefined.The Both the machine model and the program logic are for- next step of a program is undefined if it jumps to an invalid malized within a mechanized meta-logic,the Calculus of label or the next state of its first command is undefined

packages. The type system of our TAL contains non￾trivial features such as mutable references, recursive types, and union types, and is capable of typing muta￾ble recursive data structures. The collector we verified is a conservative variant of a standard stop-the-world mark-sweep collector [14]. • Although our current paper only shows how to safely link TAL with a certified conservative collector, our methodology is general, capable of verifying more complex situations, such as the TAL type system keep￾ing complex information for an accurate collector or even an incremental collector with read/write barriers. • We specify the collector using the stack-based cer￾tified assembly programming (SCAP) framework [8] extended with separation-logic primitives [24]. Our specification asserts the machine-level behavior of the collector and is general enough for various mutator safety requirements besides type safety. The safety proof of our collector, which is done using SCAP, is a nontrivial work by itself. • The work presented in this paper is fully mechanized within the Coq proof assistant [5]. Thus, the linked code of the mutator and collector can immediately be shipped as an FPCC package with a minimal TCB. We have also developed various mechanisms in Coq to simplify proof construction. In Section 2, we introduce the preliminary knowledge needed to understand the rest of the paper. In Section 3, we present our general methodology for building TAL with certified garbage collection. In Sections 4–6 we apply this methodology to verify the safe interaction of a TAL with a conservative collector. We discuss the implementation in Section 7. Finally, we discuss related work and conclude. Note that all lemmas and theorems in this paper are me￾chanically proved in Coq. Their detailed proofs are avail￾able on our project web site [16]. 2. Basic setting Before presenting our general methodology we give a general introduction to the FPCC system that our work uses. This includes a MIPS32-style [18] abstract machine model and the lightweight open framework for certified assembly programming [7] (LOCAP), a program logic for reasoning about the interaction of two different verification systems. We also present the embedding of SCAP [8] in LOCAP. As demonstrated by Feng et al. [8, 7], SCAP is suitable for certifying system level libraries, and we use it to construct the safety proof for our garbage collector. Both the machine model and the program logic are for￾malized within a mechanized meta-logic, the Calculus of (Prog) P ::= (C, S,I) (CdHeap) C ::= {f ❀ I} ∗ (State) S ::= (H, R) (Heap) H ::= {l ❀ w} ∗ (RFile) R ::= {r ❀ w} ∗ (Reg) r ::= {rk} k∈{0...31} (Wd, Lab) w, f ::= 0 | 1 | 2 | . . . (Address) l ::= 0 | 4 | 8 | . . . (ISeq) I ::= c;I | beq rs, rt, f;I | bne rs, rt, f;I | j f | jal f, fret | jr rs (Comm) c ::= addu rd, rs, rt | addiu rd, rs, w | subu rd, rs, rt | srl rd, rs, 1 | sltu rd, rs, rt | andi rd, rs, 7 | lw rd, w(rs) | sw rs, w(rd) Figure 1. Abstract machine syntax Inductive Construction (CiC) [23], as implemented in the Coq proof assistant [5]. CiC is a higher-order predicate logic extended with inductive definitions. The CiC terms in this paper are written using standard logical notation. We let Prop be the universe of all logical propositions and Set be the universe of all computational terms. 2.1. Abstract machine Figure 1 gives the syntax of our abstract machine. A pro￾gram P is a triple of a code heap C, a machine state S and an instruction sequence I. A code heap C is a partial map from code labels f to instruction sequences I. A machine state S contains a data heap H and a register file R. A data heap H is a partial map from 4-byte aligned addresses l to word values w, while a register file R is a map from registers r to word values, with r0 always mapped to 0. A command c is a non-control-flow instruction such as a register add or a heap load. An instruction sequence I, or code block, is a series of commands and branches followed by an uncondi￾tional jump instruction. For simplicity, we separate the code heap C from the mutable data heap H. Also, we use an in￾struction sequence instead of the standard pc register. This results in the additional return address fret in the jump and link instruction jal f, fret. By expanding this instruction to the MIPS instruction pair jal f and j fret, all our certi- fied code [16] can directly run on the SPIM simulator [15]. Following [18], we give the small step operational se￾mantics of the abstract machine in Figure 2. We write X(z) for the value bound to z in the map X, and X{z ❀ v} for the map obtained by updating the binding of z to v in X. Note that for a lw/sw command, if the source address is not in the domain of the heap, the next state is undefined. The next step of a program is undefined if it jumps to an invalid label or the next state of its first command is undefined

then (C,(H,R),I) (CdSpec) 0 “= 4……… jf if f E dom(C),(C,(H,R),C(f) (ChSpec) : {(1,0)} jalf,fret iff∈dom(C), (Assert) a S ChSpec→State-Prop (C,(H,R(r31fre}),C(f)) (Interp) uD CdSpec-Assert jrra ifR(r.)∈dom(C), a→a' 兰 亚，S.a亚S→a'亚S (C,(H,R),C(R(r=)) 亚C亚 兰 beqrs,rt,f;I ifR(r.)≠R(r:),(C,(H,R),), (E,0).(任，)∈亚→(E,0∈亚 else if f E dom(C).(C,(,R),C(f)) (av 兰λ亚，S.亚'C亚∧a亚S bne rs,rt,f;I' if R(r)=R(r).(C,(H,R),I'). else if f E dom(C),(C,(H,R),C(f)) Figure 3.LOCAP specification constructs c:I' if Next((HR))=S',(C.S',I') if c= then Nexte(H,R)= 亚上P(Wel-formed Program) addu ra,rs,rt H,RraR(r.)+R(r}】 亚上C:亚(a亚S)上{a}I addiu ra,rs,w (H,RaR(ra)+w)) (PROG) ΨH(C,S,) subu rd,rs,It H,R{raR(r.)-R(re)】 srl ra,rs,1 (H,R{ra+R(r=)/2) 亚kC:亚r'(Wel-formed Code Heap) slturd,rs,rt (H.Rfrak) 卜{II)w}C(E)∀（任，）∈Ψ' if R(r:)<R(rt),k 1,else=0 (CDHP) 亚卜C:亚 andira,rs,7 (H,R{ra→R(r.)mod8】 lwra,(rs】 if(R(r:)+)∈dom(H), aI (Well-formed Instruction Sequence) (H,R{raH(®(r:)+)}) if(R(ra)+)∈dom(H), a→λ亚，S.30.(任，0)∈亚Λ【0例亚S sW Is,W(rd) (H{R(ra)+→R(r)},R) {a)jf ) a÷入亚，(H,R).30. Figure 2.Abstract machine semantics (®(r:),)∈亚Al业(H,R) (JR) {a)jrra 2.2.Program logic a→入亚，(H,R).30. (任，0)∈亚A【]亚(L,R{r31fr) (JAL) The readers may view LOCAP as a simplified OCAP [7]. 卜{a}jalf,fxet or an extended CAPO [8].We use it to embed two verifica- 卜{a}Ia→λ亚，S.a'亚Nextc(S) tion systems,namely TAL and SCAP.As listed in Figure 3, (SEQ) Ffac:I the specification of a code block is given by 0.This may be a state predicate in Hoare logic [12],a register file type in TAL,or anything else.LOCAP is a simplification of OCAP Figure 4.LOCAP inference rules(excerpt) because there are only two kinds of code block specifica- tions,so the language dictionary of OCAP is not needed.A The weakening lemma states that if a code block is well- code heap specification is a set of(f,)pairs.Therefore, formed with some a',it is also well-formed with a stronger a code block may have more than one kind of specification assertion a,and the proof of a well-formed code block can in We utilize this property to specify the GC interface for be lifted from a local亚to a global亚'. TAL.The interpretation function]translates into a pred- icate a over the environment and the machine state,to Lemma 1(Weakening). allow a to specify the code pointers (labels of code blocks) 1.If a=a'and a'}I,then:a}I; in Both and [I]will be instantiated for TAL and SCAP 2.If亚≤亚'andF{(a)w}I,then:F{(a)w}I. in our following discussion.Finally,is the implication relation on assertions and a lifted assertion (a)combines The soundness-correctness theorem of the CAP system a with all the information in ensures that a well-formed program will run forever without reaching any undefined steps in Figure 2,and the partial We show the LOCAP inference rules in Figure 4.A well-formed program is a well-formed code heap with an correctness of the program against its specification holds. appropriate initial state.A code heap C is well-formed with Theorem 1 (Soundness-Correctness). respect to if each pair in corresponds to a well-formed If(C,S,I),for all natural number n there exists code block in C.Interested readers may find the detailed a (C,S,I'),such that (C,S,In (C,S',I');and if explanation of the rules in [7],but this is not required for (C,,I')(C,S",C(f)),then there exists a 0,such understanding the rest of the paper. that(f,)∈亚and [e]亚s

if I = then (C,(H, R),I) 7−→ j f if f ∈ dom(C), (C,(H, R), C(f)) jal f, fret if f ∈ dom(C), (C,(H, R{r31 ❀ fret}), C(f)) jr rs if R(rs) ∈ dom(C), (C,(H, R), C(R(rs))) beq rs, rt, f;I ′ if R(rs) 6= R(rt), (C,(H, R),I ′ ), else if f ∈ dom(C), (C,(H, R), C(f)) bne rs, rt, f;I ′ if R(rs) = R(rt), (C,(H, R),I ′ ), else if f ∈ dom(C), (C,(H, R), C(f)) c;I ′ if Nextc((H, R)) = S ′ , (C, S ′ ,I ′ ) if c = then Nextc(H, R)= addu rd, rs, rt (H, R{rd ❀ R(rs) + R(rt)}) addiu rd, rs, w (H, R{rd ❀ R(rs) + w}) subu rd, rs, rt (H, R{rd ❀ R(rs) − R(rt)}) srl rd, rs, 1 (H, R{rd ❀ R(rs)/2}) sltu rd, rs, rt (H, R{rd ❀ k}) if R(rs) < R(rt), k = 1, else k = 0 andi rd, rs, 7 (H, R{rd ❀ R(rs) mod 8}) lw rd, w(rs) if (R(rs) + w) ∈ dom(H), (H, R{rd ❀ H(R(rs) + w)}) sw rs, w(rd) if (R(rd) + w) ∈ dom(H), (H{R(rd) + w ❀ R(rs)}, R) Figure 2. Abstract machine semantics 2.2. Program logic The readers may view LOCAP as a simplified OCAP [7], or an extended CAP0 [8]. We use it to embed two verifica￾tion systems, namely TAL and SCAP. As listed in Figure 3, the specification of a code block is given by θ. This may be a state predicate in Hoare logic [12], a register file type in TAL, or anything else. LOCAP is a simplification of OCAP because there are only two kinds of code block specifica￾tions, so the language dictionary of OCAP is not needed. A code heap specification Ψ is a set of (f, θ) pairs. Therefore, a code block may have more than one kind of specification in Ψ. We utilize this property to specify the GC interface for TAL. The interpretation function [[ ]] translates θ into a pred￾icate a over the environment Ψ and the machine state, to allow a to specify the code pointers (labels of code blocks) in Ψ. Both θ and [[ ]] will be instantiated for TAL and SCAP in our following discussion. Finally, ⇒ is the implication relation on assertions and a lifted assertion haiΨ combines a with all the information in Ψ. We show the LOCAP inference rules in Figure 4. A well-formed program is a well-formed code heap with an appropriate initial state. A code heap C is well-formed with respect to Ψ if each pair in Ψ corresponds to a well-formed code block in C. Interested readers may find the detailed explanation of the rules in [7], but this is not required for understanding the rest of the paper. (CdSpec) θ ::= · · · | · · · (ChSpec) Ψ ::= {(l, θ)} ∗ (Assert) a ∈ ChSpec → State → Prop (Interp) [[ ]] ∈ CdSpec → Assert a ⇒ a ′ def = ∀Ψ, S. a Ψ S → a ′ Ψ S Ψ ⊆ Ψ ′ def = ∀(f, θ). (f, θ) ∈ Ψ → (f, θ) ∈ Ψ ′ haiΨ′ def = λΨ, S. Ψ ′ ⊆ Ψ ∧ a Ψ S Figure 3. LOCAP specification constructs Ψ ⊢ P (Well-formed Program) Ψ ⊢ C : Ψ (a Ψ S) ⊢ {a} I Ψ ⊢ (C, S,I) (PROG) Ψ ⊢ C : Ψ′ (Well-formed Code Heap) ⊢ {h[[θ]]iΨ} C(f) ∀(f, θ) ∈ Ψ ′ Ψ ⊢ C : Ψ′ (CDHP) ⊢ {a} I (Well-formed Instruction Sequence) a ⇒ λΨ, S. ∃θ. (f, θ) ∈ Ψ ∧ [[θ]] Ψ S ⊢ {a} j f (J) a ⇒ λΨ,(H, R). ∃θ. (R(rs), θ) ∈ Ψ ∧ [[θ]] Ψ (H, R) ⊢ {a} jr rs (JR) a ⇒ λΨ,(H, R). ∃θ. (f, θ) ∈ Ψ ∧ [[θ]] Ψ (H, R{r31 ❀ fret}) ⊢ {a} jal f, fret (JAL) ⊢ {a ′ } I a ⇒ λΨ, S. a ′ Ψ Nextc(S) ⊢ {a} c;I (SEQ) Figure 4. LOCAP inference rules (excerpt) The weakening lemma states that if a code block is well￾formed with some a ′ , it is also well-formed with a stronger assertion a, and the proof of a well-formed code block can be lifted from a local Ψ to a global Ψ′ . Lemma 1 (Weakening). 1. If a ⇒ a ′ and ⊢ {a ′} I, then: ⊢ {a} I; 2. If Ψ ⊆ Ψ′ and ⊢ {haiΨ} I, then: ⊢ {haiΨ′} I. The soundness-correctness theorem of the CAP system ensures that a well-formed program will run forever without reaching any undefined steps in Figure 2, and the partial correctness of the program against its specification holds. Theorem 1 (Soundness-Correctness). If Ψ ⊢ (C, S,I), for all natural number n there exists a (C, S ′ ,I ′ ), such that (C, S,I) 7−→n (C, S ′ ,I ′ ); and if (C, S ′ ,I ′ ) 7−→ (C, S ′′ , C(f)), then there exists a θ, such that (f,θ) ∈ Ψ and [[θ]] Ψ S ′′

(SPred) p,q∈State一Prop (Guar） TAL Collector g State→State-Prop (Cdspec）0 =(P,g) Well-formed State GC Inv wfst(0,q,亚)兰∀(H,R).q(,R)一 1Mx17,4x17) Well-formed State GC Inv T.((r31),)∈亚ATuΨ(L,R) Well-formed State GC Inv a110c: wfst(m+1,q,亚)兰(，R).q(H,R)→ 1al allo0write addiu r31,0 3p,g.(R(r31),(p,g)∈亚∧p(H,R)A Well-formed state GC Inv 1工ra wfst(n,g(H,R),Ψ) write: Well-formed State GC Inv I(p,g)IscAP兰Ψ，S.pSA3n.wfst(n,gS,Ψ) 亚FSCAP{P,g)}I兰上{《I(p,g)SCAP))w}I Figure 6.TAL and GC steps sexp{(p,g)}I (Well-formed Instruction Sequence Lemmas) the collector to form a well-formed complete code heap in (任，(p',g)∈亚（任xet,(p",g")∈Ψ LOCAP.Following Theorem 1.the code in a well-formed V(H,R).p (H,R)-p'(HI,R(r31fret ))A code heap will run safely forever from a correct initial state. S.g(L,R{r31fet})S一 This is exactly what we want.as it implies the safe inter- p”SAS”.g"s's”一g(H,R)S action of the TAL program and the garbage collector.This (H,R),(四，R). leads to the following steps to combine foundational TAL g(H,R)(,R)→R(r31)=R'(x31) (CALL) with certified garbage collection: FscaP {(p,g)}jal f,fret ∀s.pS→gSS Certifying the collector.We prove the well-formedness of (RETURN) the collector with SCAP specifications.For each collector 亚SCAP{(p,g)}jrr31 routine with the specification(p,g),assertion p should in- Figure 5.SCAP in LOCAP clude all of the information required by the collector rou- tine,while g should capture its basic safety guarantee. Embedding of SCAP.Following [7].we show the embed- Embedding of TAL.We get a foundational TAL by em- ding of SCAP in LOCAP in Figure 5.An SCAP code speci- bedding its type system in LOCAP(much like how we em- bed SCAP in LOCAP in Section 2.2).The soundness of fication is a pair consisting of a precondition p and a guaran- TAL follows directly from the soundness of LOCAP.The tee g.Here p resembles a precondition in Hoare logic while g relates the current state to the return state (of the current type system of TAL must also reflect our choice of collector in that it must contain enough information to meet the re- procedure).A guarantee g at the entry of a procedure can be used to assert its safety guarantee,as we will see later. quirements of the SCAP specifications of the collector rou- tines. The SCAP interpretation [(p,g)IscAP asserts that the whole machine state satisfies p,and there is a well-formed Collector interface compatibility.We must also provide control stack somewhere in the state.The abstract stack the TAL specifications for the collector routines to type- predicate wfst(n,g S,generally asserts that the current check the TAL client codes.Therefore in the code heap function can return to the label stored in r31 in the re- specification of the global code heap(which contains both turn state.n is the number of stack frames.When n is the client and the collector),we have both the SCAP and 0,the caller of the SCAP function must be a TAL program. TAL specifications for the collector interface.For each col- A set of lemmas is also proved for building well-formed code blocks with SCAP code specifications.A detailed lector interface,we supply the missing proof required by the CDHP rule using Lemma 1,if the interpretation of its TAL knowledge of wfst and the lemmas is not needed for under- specification implies the interpretation of its SCAP one. standing the rest of the paper;interested readers may refer to [8,7]for their explanations. In the rest of this section,we discuss several general as- pects of embedding TAL into LOCAP with respect to vari- 3.The general methodology ous garbage collectors. Our basic idea comes from the analysis in Section 2.2:if 3.1.Typed assembly language in LOCAP we are able to prove that the client program is well-formed using a TAL-style type system,and that the collector is The register file type I of the original TAL [21]is a nat- well-formed using SCAP,then we can link the client with ural candidate for the TAL instantiation of the LOCAP code

(SPred) p, q ∈ State → Prop (Guar) g ∈ State → State → Prop (CdSpec) θ ::= (p, g) wfst(0, q, Ψ) def = ∀(H, R). q (H, R) → ∃Γ. (R(r31), Γ) ∈ Ψ ∧ [[Γ]]TAL Ψ (H, R) wfst(n + 1, q, Ψ) def = ∀(H, R). q (H, R) → ∃p, g. (R(r31),(p, g)) ∈ Ψ ∧ p (H, R)∧ wfst(n, g (H, R), Ψ) [[(p, g)]]SCAP def = λΨ, S. p S ∧ ∃n. wfst(n, g S, Ψ) Ψ ⊢SCAP {(p, g)} I def = ⊢ {h[[(p, g)]]SCAPiΨ} I Ψ ⊢SCAP {(p, g)} I (Well-formed Instruction Sequence Lemmas) (f,(p′ , g ′ )) ∈ Ψ (fret,(p′′ , g ′′)) ∈ Ψ ∀(H, R). p (H, R) → p ′ (H, R{r31 ❀ fret})∧ ∀S ′ . g ′ (H, R{r31 ❀ fret}) S ′ → p ′′ S ′ ∧ ∀S ′′ . g ′′ S ′ S ′′ → g (H, R) S ′′ ∀(H, R),(H ′ , R ′ ). g ′ (H, R) (H ′ , R ′ ) → R(r31) = R ′ (r31) Ψ ⊢SCAP {(p, g)} jal f, fret (CALL) ∀S. p S → g S S Ψ ⊢SCAP {(p, g)} jr r31 (RETURN) Figure 5. SCAP in LOCAP Embedding of SCAP. Following [7], we show the embed￾ding of SCAP in LOCAP in Figure 5. An SCAP code speci- fication is a pair consisting of a precondition p and a guaran￾tee g. Here p resembles a precondition in Hoare logic while g relates the current state to the return state (of the current procedure). A guarantee g at the entry of a procedure can be used to assert its safety guarantee, as we will see later. The SCAP interpretation [[(p, g)]]SCAP asserts that the whole machine state satisfies p, and there is a well-formed control stack somewhere in the state. The abstract stack predicate wfst(n, g S, Ψ) generally asserts that the current function can return to the label stored in r31 in the re￾turn state. n is the number of stack frames. When n is 0, the caller of the SCAP function must be a TAL program. A set of lemmas is also proved for building well-formed code blocks with SCAP code specifications. A detailed knowledge of wfst and the lemmas is not needed for under￾standing the rest of the paper; interested readers may refer to [8, 7] for their explanations. 3. The general methodology Our basic idea comes from the analysis in Section 2.2: if we are able to prove that the client program is well-formed using a TAL-style type system, and that the collector is well-formed using SCAP, then we can link the client with ￾
 
  
    ￾
       ￾
 
  
     ￾  ￾ ￾  
   ￾
 
  
   
       ￾
 
  
                    ￾
 
  
     ￾ ￾   ￾
     ￾
   Figure 6. TAL and GC steps the collector to form a well-formed complete code heap in LOCAP. Following Theorem 1, the code in a well-formed code heap will run safely forever from a correct initial state. This is exactly what we want, as it implies the safe inter￾action of the TAL program and the garbage collector. This leads to the following steps to combine foundational TAL with certified garbage collection: Certifying the collector. We prove the well-formedness of the collector with SCAP specifications. For each collector routine with the specification (p, g), assertion p should in￾clude all of the information required by the collector rou￾tine, while g should capture its basic safety guarantee. Embedding of TAL. We get a foundational TAL by em￾bedding its type system in LOCAP (much like how we em￾bed SCAP in LOCAP in Section 2.2). The soundness of TAL follows directly from the soundness of LOCAP. The type system of TAL must also reflect our choice of collector in that it must contain enough information to meet the re￾quirements of the SCAP specifications of the collector rou￾tines. Collector interface compatibility. We must also provide the TAL specifications for the collector routines to type￾check the TAL client codes. Therefore in the code heap specification of the global code heap (which contains both the client and the collector), we have both the SCAP and TAL specifications for the collector interface. For each col￾lector interface, we supply the missing proof required by the CDHP rule using Lemma 1, if the interpretation of its TAL specification implies the interpretation of its SCAP one. In the rest of this section, we discuss several general as￾pects of embedding TAL into LOCAP with respect to vari￾ous garbage collectors. 3.1. Typed assembly language in LOCAP The register file type Γ of the original TAL [21] is a nat￾ural candidate for the TAL instantiation of the LOCAP code

mark_field(val){ if (val ST II val >ED)return null=0 if (val mod 8 !=0)return; st,ed =8116|24|. if (markbit(val)==BLACK)return; ptrs 些 {1|(1mod8=0)A(st≤1first); reach(H,1,1) mark_field(ptr->second); rchrts(,R),1)兰r∈roots..reach(H,R(r),) for(addr ST;addr ED;addr ++ if (markbit(addr)==WHITE){ addr->first freeptr;freeptr addr; Figure 8.Pointer validity and reachability else markbit(addr)=WHITE; } On the other hand,to prove collector interface compat- a11oc()[ ibility,we must show that the successful execution of each if (freeptr ==NULL)gc(); collector routine also preserves these invariants,as shown in if (freeptr ==NULL)loop(); Figure 6.That is,for each collector routine,its guarantee g 1=freeptr;freeptr freeptr->first; satisfies the following relation,where I and I'are defined return 1; by the behavior of this routine. y ∀w,S,S.gSS'→ITraΨS→TIat亚S Figure 7.A conservative collector Next we will present a case study that demonstrates the practicality and effectiveness of our methodology. specification 0,and its interpretation[AL,as shown bel- low,is a variant of the one used in [7]. 4.A certified conservative collector T兰A亚，(H,R).H. 亚卜L(Hr,R):TAgc_inv(H,R),H) Like TALx86 [20]and TALT [6],we choose a conser- The interpretation allows us to partition the state,reason- vative garbage collector [3].This kind of collector treats ing about TAL code as though it were running on a virtual all values as potential pointers,eliminating the need to keep heap Hr provided by the collector.Both the TAL state typ- complex pointer location information in the TAL type sys- ing rules and the collector invariant depend on the collector tem and simplifying the collector interface. used.With an precise collector,HTAL (H,R):I must Our collector is a standard stop-the-world mark-sweep contain pointer information for each heap object,while with collector [14]and uses the valid pointer check procedure of a conservative collector this is not necessary.The gc_inv in- the Boehm-Demers-Weiser collector [3].To simplify the variants of various precise collectors are described in [17]. problem,our collector only allocates heap chunks with a The invariantAL(Hr,R):I corresponds to the fixed size of two words.The pseudo code of our collector well-formed state relation of the original TAL,but with ad- is presented in Figure 7. ditional information required by the collector routines to correctly trace the live objects in H.The garbage collec- 4.1.The specification interface tor representation invariant gc_inv((H,R),H)specifies the collector's data structures in (H,R)and their relationship We define in Figure 8 the view of the heap that the col- with the virtual heap Hr accessed by TAL clients. lector and TAL must agree on.The constant address null is In addition.the TAL instruction sequence lemmas, 0.The variables st and ed are the lower and upper bounds which correspond to the instruction typing rules of the orig- of the collector's allocatable heap,and are aligned at 8,the inal TAL,must ensure that the invariants of TAL hold at size of a heap chunk.Thus,a value 1 is a valid pointer any step in the execution of a well-formed instruction se- (vptr(1))only if it falls in the range of the allocatable heap quence proved with these lemmas,as shown in Figure 6. and points to the start of a heap chunk. That is,the execution of TAL code preserves state well- The reachability predicate reach(H,1,1)is inductively formedness,and never breaks the collector's invariant. defined.In the base case,a valid pointer is reachable from

mark_field(val) { if (val = ED) return; if (val mod 8 != 0) return; if (markbit(val) == BLACK) return; markbit(val) = BLACK; stack_push(val); } gc() { mark_field(root1); ... mark_field(rootn); while(!stack_empty()){ ptr = stack_pop(); mark_field(ptr->first); mark_field(ptr->second); } for(addr = ST; addr first = freeptr; freeptr = addr; } else markbit(addr) = WHITE; } alloc() { if (freeptr == NULL) gc(); if (freeptr == NULL) loop(); l = freeptr; freeptr = freeptr->first; return l; } Figure 7. A conservative collector specification θ, and its interpretation [[ ]]TAL, as shown bel￾low, is a variant of the one used in [7]. [[Γ]]TAL def = λΨ,(H, R). ∃HT. Ψ ⊢TAL (HT, R) : Γ ∧ gc inv((H, R), HT) The interpretation allows us to partition the state, reason￾ing about TAL code as though it were running on a virtual heap HT provided by the collector. Both the TAL state typ￾ing rules and the collector invariant depend on the collector used. With an precise collector, Ψ ⊢TAL (HT, R) : Γ must contain pointer information for each heap object, while with a conservative collector this is not necessary. The gc inv in￾variants of various precise collectors are described in [17]. The invariant Ψ ⊢TAL (HT, R) : Γ corresponds to the well-formed state relation of the original TAL, but with ad￾ditional information required by the collector routines to correctly trace the live objects in HT. The garbage collec￾tor representation invariant gc inv((H, R), HT) specifies the collector’s data structures in (H, R) and their relationship with the virtual heap HT accessed by TAL clients. In addition, the TAL instruction sequence lemmas, which correspond to the instruction typing rules of the orig￾inal TAL, must ensure that the invariants of [[Γ]]TAL hold at any step in the execution of a well-formed instruction se￾quence proved with these lemmas, as shown in Figure 6. That is, the execution of TAL code preserves state well￾formedness, and never breaks the collector’s invariant. null ::= 0 st, ed ::= 8 | 16 | 24 | . . . ptrs def = {l | (l mod 8 = 0) ∧ (st ≤ l < ed)} vptr(l) def = l ∈ ptrs roots def = {r17, r18, r31, r0} vptr(l) reach(H, l, l) (REFL) vptr(l) vptr(l ′ ) reach(H, l ′′ , l ′ ) H(l) = l ′′ ∨ H(l + 4) = l ′′ reach(H, l, l ′ ) (NEXT) rchrts((H, R), l) def = ∃r ∈ roots. reach(H, R(r), l) Figure 8. Pointer validity and reachability On the other hand, to prove collector interface compat￾ibility, we must show that the successful execution of each collector routine also preserves these invariants, as shown in Figure 6. That is, for each collector routine, its guarantee g satisfies the following relation, where Γ and Γ ′ are defined by the behavior of this routine. ∀Ψ, S, S ′ . g S S′ → [[Γ]]TAL Ψ S → [[Γ′ ]]TAL Ψ S ′ Next we will present a case study that demonstrates the practicality and effectiveness of our methodology. 4. A certified conservative collector Like TALx86 [20] and TALT [6], we choose a conser￾vative garbage collector [3]. This kind of collector treats all values as potential pointers, eliminating the need to keep complex pointer location information in the TAL type sys￾tem and simplifying the collector interface. Our collector is a standard stop-the-world mark-sweep collector [14] and uses the valid pointer check procedure of the Boehm-Demers-Weiser collector [3]. To simplify the problem, our collector only allocates heap chunks with a fixed size of two words. The pseudo code of our collector is presented in Figure 7. 4.1. The specification interface We define in Figure 8 the view of the heap that the col￾lector and TAL must agree on. The constant address null is 0. The variables st and ed are the lower and upper bounds of the collector’s allocatable heap, and are aligned at 8, the size of a heap chunk. Thus, a value l is a valid pointer (vptr(l)) only if it falls in the range of the allocatable heap and points to the start of a heap chunk. The reachability predicate reach(H, l, l ′ ) is inductively defined. In the base case, a valid pointer is reachable from

(IFlag) p“=1|0 eq(H)兰λ.=H (WTy) “=a|nul int (T,T)IHa.TITVT gc_inv(H,R),H)兰B,E (RfTy) T“={rT} sted_ok(R)A BUF=ptrs A (CdSpec) = dom(H)={1,1+4|1∈B}A (DhSpec）Φr= {1(r,r)} HIeq()flst(F,R)*mbits(ptrs,0)*mstack(0,R) 亚FLT:I兰上{《T]a)w}I chkeq(H,H',1)兰H(1)='(a)AH(1+4)='(1+4) gc-step(L,R),(,R')当 L T:I (Well-formed Instruction Sequence Lemmas) (v1.rchrts((HR).1)-chkeg(H,H',1))A (r∈roots.R(r)=R'(r) (任，T)∈亚上LT≤Y (J) 亚上TALT:jf alloc step((,R),(H R)) 1年dom(H)A(1+4)年dom(H)A (任，T')∈亚（任t,")∈Ψ I'=H{1-}H1+4-}ΛR'=R{x181} LT{r31~T"}≤ (JAL) pa兰S..gc-inv((S,H) 亚卜rLT:jalf,fre g兰A(L,R),(',R').Hr.gc_inv(L,R),)一 T(r:)=T上LT≤T'亚FL「{raT'}:I Rt.gc_inv((,R),)A -(MOV) 亚frLT:addiura,ra,O; gc-step((H,R),(HR))A alloc.step((H,R),() 亚(f)='T(r.)=nul VT 上aLT{r:nul≤T'亚上LT{raT}:I' -(NULL) 业FLT:beqrs,r0,f: Figure 9.Collector interface specification Figure 10.TAL in LOCAP itself.In the inductive case,I'is reachable from 1 if it is reachable from the pointers in the heap chunk at 1. The global heap H contains the allocated subheap Hr, We define the collector's root set roots as the set of reg- the free list with the head pointer in R(flst(F,R)),the isters used by TAL.For simplicity,we have four registers in mark bits for all the pointers in ptrs(mbits(ptrs,0)). this set.but it would not be difficult make more registers us- and the mark stack with the stack pointers stored in R able in TAL.The predicate rchrts(S,1)asserts that 1 points (mstack(0R)). to a live heap chunk in state S. The guarantee ga specifies the situation where a free 4.2.Specification and proof construction chunk is successfully allocated.It simply divides the state transition of alloc into a collection phase and an allocation phase with an auxiliary state (H,),and asserts that: We now present the collector's safety specification and a discussion of the construction of the safety proof. The representation invariant gc_inv is preserved be- tween the entry state (H,R)and the return state SCAP Specification.Our specification of the collector in- (H',R'),with allocated subheaps H and H,respec- terface(alloc)includes the precondition pa and the guar- tively. antee ga,as defined in Figure 9. The collector's representation invariant gc_inv is defined The collection phase turns (Hr,R)into (H,R)and using separation logic [24].We write HI P if the heap the gc-step relation asserts that the live chunks are predicate P,which has the type Heap-Prop,is valid equal in the two heaps,while the values of the root with H.HP*Q is valid if H can be split into two registers are equal in the two register files.The allo- disjoint subheaps H and H2,such that both HP and cation phase turns (H,R)into (HR')and the al- H2Qare valid propositions.The precondition of alloc, loc_step relation asserts that H has exactly one more as defined with gc_inv,asserts that: heap chunk than H,with its pointer stored in R'(r18). Proof Construction.The verification of the collector in- The heap boundaries st and ed are stored in R volves two main steps.We first form the verification envi- (sted_ok(R)).The set of allocatable pointers(ptrs)is ronment Vcc with the SCAP specifications for each label 1 split into the allocated subset B and the free subset F, in the collector's code heap Coc.Then for each 1 we prove while the allocated subheap Hr contains exactly the the CAP well-formedness of the corresponding code block heap chunks in B. Coc(1)with the SCAP lemmas in Figure 5.Due to space

eq(H) def = λH ′ . H ′ = H · · · gc inv((H, R), HT) def = ∃B, F. sted ok(R) ∧ B ∪ F = ptrs ∧ dom(HT) = {l, l + 4 | l ∈ B} ∧ H ° eq(HT) ∗ flst(F, R) ∗ mbits(ptrs, 0) ∗ mstack(∅, R) chkeq(H, H ′ , l) def = H(l) = H ′ (l) ∧ H(l + 4) = H ′ (l + 4) gc step((H, R),(H ′ , R ′ )) def = (∀l. rchrts((H, R), l) → chkeq(H, H ′ , l))∧ (∀r ∈ roots. R(r) = R ′ (r)) alloc step((H, R),(H ′ , R ′ )) def = ∃l. l ∈/ dom(H) ∧ (l + 4) ∈/ dom(H)∧ H ′ = H{l ❀ −}{l + 4 ❀ −} ∧ R ′ = R{r18 ❀ l} pa def = λS. ∃HT. gc inv(S, HT) ga def = λ(H, R),(H ′ , R ′ ). ∀HT. gc inv((H, R), HT) → ∃H ′ T , H † T , R † . gc inv((H ′ , R ′ ), H ′ T) ∧ gc step((HT, R),(H † T , R † )) ∧ alloc step((H † T , R † ),(H ′ T , R ′ )) Figure 9. Collector interface specification itself. In the inductive case, l ′ is reachable from l if it is reachable from the pointers in the heap chunk at l. We define the collector’s root set roots as the set of reg￾isters used by TAL. For simplicity, we have four registers in this set, but it would not be difficult make more registers us￾able in TAL. The predicate rchrts(S, l) asserts that l points to a live heap chunk in state S. 4.2. Specification and proof construction We now present the collector’s safety specification and a discussion of the construction of the safety proof. SCAP Specification. Our specification of the collector in￾terface (alloc) includes the precondition pa and the guar￾antee ga, as defined in Figure 9. The collector’s representation invariant gc inv is defined using separation logic [24]. We write H ° P if the heap predicate P, which has the type Heap → Prop, is valid with H. H ° P ∗ Q is valid if H can be split into two disjoint subheaps H1 and H2, such that both H1 ° P and H2 ° Q are valid propositions. The precondition of alloc, as defined with gc inv, asserts that: • The heap boundaries st and ed are stored in R (sted ok(R)). The set of allocatable pointers (ptrs) is split into the allocated subset B and the free subset F, while the allocated subheap HT contains exactly the heap chunks in B. (IFlag) ϕ ::= 1 | 0 (WTy) τ ::= α | nul | int | Γ | hτ ϕ , τ ϕ i | µα.τ | τ ∨ τ (RfTy) Γ ::= {r ❀ τ} ∗ (CdSpec) θ ::= Γ (DhSpec) Φ ::= {l ❀ (τ ϕ , τ ϕ )} ∗ Ψ ⊢TAL Γ : I def = ⊢ {h[[Γ]]TALiΨ} I Ψ ⊢TAL Γ : I (Well-formed Instruction Sequence Lemmas) (f, Γ ′ ) ∈ Ψ ⊢TAL Γ ≤ Γ ′ Ψ ⊢TAL Γ : j f (J) (f, Γ ′ ) ∈ Ψ (fret, Γ ′′) ∈ Ψ ⊢TAL Γ{r31 ❀ Γ ′′} ≤ Γ ′ Ψ ⊢TAL Γ : jal f, fret (JAL) Γ(rs) = τ ⊢TAL τ ≤ τ ′ Ψ ⊢TAL Γ{rd ❀ τ ′ } : I ′ Ψ ⊢TAL Γ : addiu rd, rs, 0;I ′ (MOV) Ψ(f) = Γ′ Γ(rs) = nul ∨ τ ⊢TAL Γ{rs ❀ nul} ≤ Γ ′ Ψ ⊢TAL Γ{rs ❀ τ} : I ′ Ψ ⊢TAL Γ : beq rs, r0, f;I ′ (NULL) Figure 10. TAL in LOCAP • The global heap H contains the allocated subheap HT, the free list with the head pointer in R (flst(F, R)), the mark bits for all the pointers in ptrs (mbits(ptrs, 0)), and the mark stack with the stack pointers stored in R (mstack(∅, R)). The guarantee ga specifies the situation where a free chunk is successfully allocated. It simply divides the state transition of alloc into a collection phase and an allocation phase with an auxiliary state (H † T , R † ), and asserts that: • The representation invariant gc inv is preserved be￾tween the entry state (H, R) and the return state (H′ , R ′ ), with allocated subheaps HT and H′ T , respec￾tively. • The collection phase turns (HT, R) into (H † T , R † ) and the gc step relation asserts that the live chunks are equal in the two heaps, while the values of the root registers are equal in the two register files. The allo￾cation phase turns (H † T , R † ) into (H′ T , R ′ ) and the al￾loc step relation asserts that H′ T has exactly one more heap chunk than H † T , with its pointer stored in R ′ (r18). Proof Construction. The verification of the collector in￾volves two main steps. We first form the verification envi￾ronment ΨGC with the SCAP specifications for each label l in the collector’s code heap CGC. Then for each l we prove the CAP well-formedness of the corresponding code block CGC(l) with the SCAP lemmas in Figure 5. Due to space

上ra*上raL*≤*(Well-formed Type,Subtyping) ftv(7)=0 T(r)=T FTAL T廿r∈dom(T)roots (WORD) FIAL T 卜ALT (RFILE) Φ(1)=(ro,T4)上Ti vptri(1)1∈dom(④) (HEAP) PTALΦ (r)='(r)r∈dom() T(r)=μa.r (SUB) 卜ALT≤Y FLTST(UNFOLD) I(r)=Tlua.T/a] (FOLD) FLTP≤rP (REFL) 上LT≤T{r+Ha.T} u7P≤0(0-l) HLT≤TVT(UNIONL) FaLT≤TVT(UNIONR) (NULL-INT) FTAL nul≤int 亚；Φ上rat*:*亚上atS:T(Value,Heap,Rfle,State Typing) 亚；ΦFL0:nU(NULL) ;ΦFaL:int(NT) (任，)∈亚 ;电FLf:T(CoDE) 上TAL fst(④(1)≤T0上Lsnd(④(1)≤T4 亚；④上LN:T卜LT≤T (TUPLE) (SUBTY) 亚：Φ上1L1:(0,rP4) Ψ：Φ上LW:T' 亚；Φ上rt:Tμa.T/a 亚；重上AL日：T 亚：Φ上L日：μ0.T -(REC) Ψ：Φ上aL:T -(INIT) 业；电FL:P(UNK) 上④Φ(1)=(r,T4)亚；Φ上LH(1+):T1∈dom(Φ) -(HEAP) 亚：Φ卜ALH:Φ FLT亚；④FL.R(r):T(r)Vr∈dom(T) Ψ：重上rALH:重Ψ；④上LR:T Ψ；Φ上LR:T ·(RFILE) 亚FLS:T (STATE) Figure 11.TAL state typing rules limitations,we omit detailed discussion of the collector's with a size of two words.This does not reduce the expres- proof construction.Interested readers will find the assem- siveness of our type system,since a tuple with arbitrary size bly code implementation,SCAP specification and proof of can be encoded into a list of our fixed-sized tuples. the collector in [16]. The TAL typing rules listed in Figure 11 are similar to those of the original TAL.However,we require that the do- 5.A typed assembly language with GC main of a well-formed code heap specification contains only valid heap pointers,and a well-formed register file type as- We show in Figure 10 our definition of TAL types, serts only the root register set roots defined in Figure 8. which includes code types,mutable reference types,recur- As partly listed in Figure 10,our TAL lemmas for CAP sive types and union types.We do not include a polymor- resemble the instruction typing rules of the original TAL. phic code type,as it is orthogonal to our primary concern, The definition of AL T:I is based on the TAL interpre- memory management,and this extension should not be hard tationAL in Section 3.1,and the representation invariant for our system. gc-inv in Figure 9.Instead of using the malloc macro of the Our TAL type system is built over the abstract machine original TAL,our TAL supports heap allocation by making in Section 2.1 and based on the definitions in Section 4.1, a function call to the garbage collector (jal alloc,fret). and thus is different from the original TAL [21]in several The readers should note that there are other possible sets ways.Since both the registers and heap cells contain only of TAL lemmas for our type system besides the ones we word-size values,we use one value type r for all values,in- used.The choice of these lemmas may also depend on the stead of having small value and heap value types as in the actual type-checking algorithm. original TAL.We also use fixed-sized tuple types to make it A well-formed TAL instruction sequence proved with consistent with our collector,which allocates heap chunks the TAL lemmas keeps the invariant that at any step of its

⊢TAL ∗ ⊢TAL ∗ ≤ ∗ (Well-formed Type, Subtyping) ftv(τ ) = ∅ ⊢TAL τ (WORD) Γ(r) = τ ⊢TAL τ ∀ r ∈ dom(Γ) ⊆ roots ⊢TAL Γ (RFILE) Φ(l) = (τ ϕ0 0 , τ ϕ4 4 ) ⊢TAL τi vptr(l) ∀ l ∈ dom(Φ) ⊢TAL Φ (HEAP) Γ(r) = Γ′ (r) ∀ r ∈ dom(Γ′ ) ⊢TAL Γ ≤ Γ ′ (SUB) Γ(r) = µα.τ ⊢TAL Γ ≤ Γ{r ❀ τ [µα.τ/α]} (UNFOLD) Γ(r) = τ [µα.τ/α] ⊢TAL Γ ≤ Γ{r ❀ µα.τ} (FOLD) ⊢TAL τ ϕ ≤ τ ϕ (REFL) ⊢TAL τ 1 ≤ τ 0 (0-1) ⊢TAL τ ≤ τ ∨ τ ′ (UNIONL) ⊢TAL τ ′ ≤ τ ∨ τ ′ (UNIONR) ⊢TAL nul ≤ int (NULL-INT) Ψ; Φ ⊢TAL ∗ : ∗ Ψ ⊢TAL S : Γ (Value, Heap, Rfile, State Typing) Ψ; Φ ⊢TAL 0 : nul (NULL) Ψ; Φ ⊢TAL w : int (INT) (f, Γ) ∈ Ψ Ψ; Φ ⊢TAL f : Γ (CODE) ⊢TAL fst(Φ(l)) ≤ τ ϕ0 0 ⊢TAL snd(Φ(l)) ≤ τ ϕ4 4 Ψ; Φ ⊢TAL l : hτ ϕ0 0 , τ ϕ4 4 i (TUPLE) Ψ; Φ ⊢TAL w : τ ⊢TAL τ ≤ τ ′ Ψ; Φ ⊢TAL w : τ ′ (SUBTY) Ψ; Φ ⊢TAL w : τ [µα.τ/α] Ψ; Φ ⊢TAL w : µα.τ (REC) Ψ; Φ ⊢TAL w : τ Ψ; Φ ⊢TAL w : τ ϕ (INIT) Ψ; Φ ⊢TAL w : τ 0 (JUNK) ⊢TAL Φ Φ(l) = (τ ϕ0 0 , τ ϕ4 4 ) Ψ; Φ ⊢TAL H(l + i) : τ ϕi i ∀ l ∈ dom(Φ′ ) Ψ; Φ ⊢TAL H : Φ′ (HEAP) ⊢TAL Γ Ψ; Φ ⊢TAL R(r) : Γ(r) ∀ r ∈ dom(Γ) Ψ; Φ ⊢TAL R : Γ (RFILE) Ψ; Φ ⊢TAL H : Φ Ψ; Φ ⊢TAL R : Γ Ψ ⊢TAL S : Γ (STATE) Figure 11. TAL state typing rules limitations, we omit detailed discussion of the collector’s proof construction. Interested readers will find the assem￾bly code implementation, SCAP specification and proof of the collector in [16]. 5. A typed assembly language with GC We show in Figure 10 our definition of TAL types, which includes code types, mutable reference types, recur￾sive types and union types. We do not include a polymor￾phic code type, as it is orthogonal to our primary concern, memory management, and this extension should not be hard for our system. Our TAL type system is built over the abstract machine in Section 2.1 and based on the definitions in Section 4.1, and thus is different from the original TAL [21] in several ways. Since both the registers and heap cells contain only word-size values, we use one value type τ for all values, in￾stead of having small value and heap value types as in the original TAL. We also use fixed-sized tuple types to make it consistent with our collector, which allocates heap chunks with a size of two words. This does not reduce the expres￾siveness of our type system, since a tuple with arbitrary size can be encoded into a list of our fixed-sized tuples. The TAL typing rules listed in Figure 11 are similar to those of the original TAL. However, we require that the do￾main of a well-formed code heap specification contains only valid heap pointers, and a well-formed register file type as￾serts only the root register set roots defined in Figure 8. As partly listed in Figure 10, our TAL lemmas for CAP resemble the instruction typing rules of the original TAL. The definition of Ψ ⊢TAL Γ : Iis based on the TAL interpre￾tation [[ ]]TAL in Section 3.1, and the representation invariant gc inv in Figure 9. Instead of using the malloc macro of the original TAL, our TAL supports heap allocation by making a function call to the garbage collector (jal alloc, fret). The readers should note that there are other possible sets of TAL lemmas for our type system besides the ones we used. The choice of these lemmas may also depend on the actual type-checking algorithm. A well-formed TAL instruction sequence proved with the TAL lemmas keeps the invariant that at any step of its

execution the machine state of TAL is well-formed and the chase(list i){ collector's invariant holds.We follow the soundness proof while(i next; i=a11oc(0,1); the TAL state typing relation.The preservation of the col- lector's invariant is proved by observing the fact that well- formed TAL instructions never change the heap's domain. Figure 12.An example 5.1.Collector interface compatibility Lemma 5(Allocation step). As the final step,we prove that the SCAP specification If alloc_step(S,(H',R')),TAL S:I,HTAL To,and of the collector interface in Figure 9 is compatible with its 卜LT4,then:亚FT(H,R):T{r:(8,T)} TAL specification Ia,which asserts that the function returns a pointer to a new heap chunk in register r18 and that the types of the other TAL registers are preserved. The proof of Lemma 4 resembles the proof of the heap extension lemma of the original TAL.Lemma 5 is trivially Theorem 2(Collector interface compatibility). derivable from Lemma 4. For any code heap specification and any instantiation of word value types Ta,To,To and T4,we have: (T]》w→((pa,ga川》w 6.An example of linked code where: .兽{r17Ta,r0Tb,31 We now give an example to show the safe linking of code {r17Ta,r0n,r18(r8,)} verified in TAL with our collector.The pseudo code of After unfolding the two interpretations,we get Pa di- chase is given in Figure 12,which repeatedly removes a rectly from ([al).Then,we instantiate the first pa- node from a list and appends a new one.If i is not null initially,the program will surely run out of memory with- rameter of wfst to 0.From Lemmas 3 and 5,we out a collector.We type check the assembly implementation know from ga that the return state of alloc satisfies Cc in Figure 13 with the following code heap specification. (r17 Ta,ro:o,r18 (To,)}])as required by the The skipped Is are listed at the corresponding labels in Fig- unfolded wfst predicate.We list here the most important ure 13. lemmas for proving Theorem 2. 亚c Lemma 2(Heap pruning). 兰{a11oc, r17 list,ro int,r31 IfΨ；④-TAL H:④and乎；④FrLR:T,then: {r17list,r0int,r18→(int°，Iist)}), 1.亚；Φ/但，R)卜LH:④/但R) (init,…),(chase,…）,(write,…）,(ret,…)} 2.;④/I,R)FTAL R:T. where /s is the data heap specification formed with ex- When the instructions pass type checking,for each(1,T) actly the live labels in the state S from pair in Vc we get the proof that: The proof of Lemma 2 follows the proof of the heap up- 上{T)we}Cc(1) date lemma of the original TAL,but with additional case analysis to separate root-reachable pointers from the rest of From Section 4,we have for each(1,(p,g))pair in the the word values. collector's code heap specification Vcc that: Lemma 3(GC step). F{《Ip,g))wac}Ccc(1) If gc_step(S,S')and HTAL S:I,then:HTAL S'I. We also obtain from Theorem 2 and Lemma 1 that: Lemma 3 is proved using Lemma 2 by observing that 上{I(T.)》woc}Ccc(alloc) both亚FrLS:Tand亚TAL S':T can be proved using the same data heap specification/s. We form the global code heap C and its specification: Lemma 4 (Heap extension). C些CeUCae亚g亚cU亚cc If亚；④FaLH:重，vptr(1),1生dom(H),rLT,and 上ALT,then: With Lemma 1,we have for each (1,0)pair in that: 1.亚；Φ'FALR:T. 卜{（平(1）I)w}C(1) 2.IfΨ；④FL0:To,and亚；ΦrrL4:T,then Ψ；Φ'FLH{1→o}{1+4w4}:Φ. Finally,we obtain the well-formedness of the linked whereΦ'stands forΦ{1(o,TP)}. code C with the CDHP rule in Figure 4

execution the machine state of TAL is well-formed and the collector’s invariant holds. We follow the soundness proof of the original TAL to prove that the execution preserves the TAL state typing relation. The preservation of the col￾lector’s invariant is proved by observing the fact that well￾formed TAL instructions never change the heap’s domain. 5.1. Collector interface compatibility As the final step, we prove that the SCAP specification of the collector interface in Figure 9 is compatible with its TAL specification Γa, which asserts that the function returns a pointer to a new heap chunk in register r18 and that the types of the other TAL registers are preserved. Theorem 2 (Collector interface compatibility). For any code heap specification Ψ and any instantiation of word value types τa, τb, τ0 and τ4, we have: h[[Γa]]iΨ ⇒ h[[(pa, ga)]]iΨ where: Γa def = {r17 ❀ τa, r0 ❀ τb, r31 ❀ {r17 ❀ τa, r0 ❀ τb, r18 ❀ hτ 0 0 , τ 0 4 i}}. After unfolding the two interpretations, we get pa di￾rectly from h[[Γa]]iΨ. Then, we instantiate the first pa￾rameter of wfst to 0. From Lemmas 3 and 5, we know from ga that the return state of alloc satisfies h[[{r17 : τa, r0 : τb, r18 : hτ 0 0 ,τ 0 4 i}]]iΨ, as required by the unfolded wfst predicate. We list here the most important lemmas for proving Theorem 2. Lemma 2 (Heap pruning). If Ψ;Φ ⊢TAL H : Φ and Ψ;Φ ⊢TAL R : Γ, then: 1. Ψ;Φ/(H,R) ⊢TAL H : Φ/(H,R) ; 2. Ψ;Φ/(H,R) ⊢TAL R : Γ. where Φ/S is the data heap specification formed with ex￾actly the live labels in the state S from Φ. The proof of Lemma 2 follows the proof of the heap up￾date lemma of the original TAL, but with additional case analysis to separate root-reachable pointers from the rest of the word values. Lemma 3 (GC step). If gc step(S, S ′ ) and Ψ ⊢TAL S : Γ, then: Ψ ⊢TAL S ′ : Γ. Lemma 3 is proved using Lemma 2 by observing that both Ψ ⊢TAL S : Γ and Ψ ⊢TAL S ′ : Γ can be proved using the same data heap specification Φ/S. Lemma 4 (Heap extension). If Ψ;Φ ⊢TAL H : Φ, vptr(l), l ∈/ dom(H), ⊢TAL τ ϕ0 0 , and ⊢TAL τ ϕ4 4 , then: 1. Ψ;Φ′ ⊢TAL R : Γ. 2. If Ψ;Φ ⊢TAL w0 : τ ϕ0 0 , and Ψ;Φ ⊢TAL w4 : τ ϕ4 4 , then Ψ;Φ′ ⊢TAL H{l ❀ w0}{l + 4 ❀ w4} : Φ′ . where Φ ′ stands for Φ{l ❀ (τ ϕ0 0 , τ ϕ4 4 )}. chase(list * i) { while(i <> NULL){ i = i->next; i = alloc(0, i); } } Figure 12. An example Lemma 5 (Allocation step). If alloc step(S,(H′ , R ′ )), Ψ ⊢TAL S : Γ, ⊢TAL τ0, and ⊢TAL τ4, then: Ψ ⊢TAL (H′ , R ′ ) : Γ{r : hτ 0 0 , τ 0 4 i}. The proof of Lemma 4 resembles the proof of the heap extension lemma of the original TAL. Lemma 5 is trivially derivable from Lemma 4. 6. An example of linked code We now give an example to show the safe linking of code verified in TAL with our collector. The pseudo code of chase is given in Figure 12, which repeatedly removes a node from a list and appends a new one. If i is not null initially, the program will surely run out of memory with￾out a collector. We type check the assembly implementation CC in Figure 13 with the following code heap specification. The skipped Γs are listed at the corresponding labels in Fig￾ure 13. ΨC def = {(alloc, {r17 ❀ list, r0 ❀ int, r31 ❀ {r17 ❀ list, r0 ❀ int, r18 ❀ hint0 , list0 i}}), (init, · · ·),(chase, · · ·),(write, · · ·),(ret, · · ·)}. When the instructions pass type checking, for each (l, Γ) pair in ΨC we get the proof that: ⊢ {h[[Γ]]iΨC } CC(l) From Section 4, we have for each (l,(p, g)) pair in the collector’s code heap specification ΨGC that: ⊢ {h[[(p, g)]]iΨGC } CGC(l) We also obtain from Theorem 2 and Lemma 1 that: ⊢ {h[[(Γa)]]iΨGC } CGC(alloc) We form the global code heap C and its specification Ψ: C def = CC ∪ CGC Ψ def = ΨC ∪ ΨGC With Lemma 1, we have for each (l,θ) pair in Ψ that: ⊢ {h[[Ψ(l)]]iΨ} C(l) Finally, we obtain the well-formedness of the linked code C with the CDHP rule in Figure 4

Iist兰μa.nulV(int',a)》 Lines Component 833 Basic properties and tactics init: r17 list,ro int} 1941 Abstract machine encoding and lemmas j chase unfold 1263 Finite set library chase: fr17nul V (int',list'),ro int} 884 Separation logic library null elim 398 LOCAP beq r17,r0,ret r17(int',list),ro int} 1188 TAL in LOCAP 1wr17,4(r17) load next 874 Reachability properties 237 [r17 list,ro int} GC Safety for TAL 360 SCAP in LOCAP.VCGen and related tactics jal alloc,write 154 Code,specification and proof of chase write: {r17list,r18(int°，Iist),r0int} 2618 Code,specification and proof of the collector swr0,0(r18) write val 276 Link up chase and the collector in LOCAP fr17 list,r18(int',list),ro int} swr17,4(r18) write next Figure 14.Proof script size (17 list,r18 (int',list),ro int} addiu r17,r18,0 move [r17nul V(int',list),r18(int',list),ro int} since it is orthogonal to the main goal of this work.Building j chase sub domain a certified TAL type checker is not hard since it has a very straight-forward(and decidable)type-checking algorithm. ret: {} In Figure 14 we give a breakdown of the size of our jret proofs for our foundational TAL with certified GC.For each Figure 13.An example(assembly) component we give the number of non-empty lines of Cog proof scripts.The work took several man-months (by pro- grammers who are familiar with the Coq system)to com- 7.Implementation plete.Interested readers can obtain the Coq implementation from our project web site [16]. Our verification is fully mechanized within Coq [5],an interactive theorem prover that uses CiC as its underlying 8.More related work and conclusion logic,where specifications and proofs are constructed as types and terms in CiC,respectively.Proof checking in Coq is thus type checking of terms in CiC,which is easier to im- Much work has been done concerning TAL and garbage plement and more trustworthy.Coq also provides a rich collector safety in addition to those mentioned in Section 1. language for defining both logical and computational con- TALT [6]considered the impact of garbage collection on structors,with the ability to construct inductive predicates the soundness of its type system and mechanically proved and well-formed recursive functions.Using this,we build GC safety assuming a conservative collector,but the type the abstract machine model and the sound program logics. system interface for the collector is not clearly defined and The tricky part of the implementation is to obtain the it is unclear how their definition of GC safety can be used pruned data heap specification s mentioned in Sec- to link with a real collector.Vanderwaart and Crary [25] tion 5.1,which implies that every label 1 in its domain sat- proposed a type system with an interface for an accurate isfies rchrts(S,1).As is a mapping function in the Set garbage collector.But again,this work addresses only the universe,we cannot get /s by a case analysis on the proof mutator (TAL)side of GC safety,while our work comple- of the decidability of rchrts(S.1)(if it can be constructed ments their work by mechanically proving the safety of both directly),as this will break the proof-irrelevance axiom that TAL and the collector,including their interaction. is commonly accepted.To solve this problem,we define in Earlier work on mechanized verification of garbage col- the Set universe a well-formed recursive Boolean function lectors (such as [13,10,4])focused mostly on abstract al- which is equivalent to the predicate rchrts,and obtains gorithms.Our certified collector,on the other hand,is a real by case analysis on the return value of this function machine-level implementation with concrete specifications To simplify the proof construction,we have imple- and it can run directly on real machine.However,our ver- mented (in Coq)a verification condition generator(VCGen) ification only addresses the safety of the collector,not any for SCAP and proved its correctness.We have also built var- liveness properties. ious automated proof tactics such as those involving sepa- The work on CAP systems [27,22,8,7]provides a nice ration logic.This results in a proof which is about 1/4 the way to build FPCC packages.Our work builds on the CAPO size of our first proof and is much easier to follow. system in [8]and the OCAP system in [7].Feng et al.[7] We omit the implementation of a type-checker for TAL, described linking TAL with a certified malloc function

list def = µα.nul ∨ hint1 , α1 i init: {r17 ❀ list, r0 ❀ int} j chase # unfold chase: {r17 ❀ nul ∨ hint1 , list1 i, r0 ❀ int} beq r17, r0, ret # null elim {r17 ❀ hint1 , list1 i, r0 ❀ int} lw r17, 4(r17) # load next {r17 ❀ list, r0 ❀ int} jal alloc, write write: {r17 ❀ list, r18 ❀ hint0 , list0 i, r0 ❀ int} sw r0, 0(r18) # write val {r17 ❀ list, r18 ❀ hint1 , list0 i, r0 ❀ int} sw r17, 4(r18) # write next {r17 ❀ list, r18 ❀ hint1 , list1 i, r0 ❀ int} addiu r17, r18, 0 # move {r17 ❀ nul ∨ hint1 , list1 i, r18 ❀ hint1 , list1 i, r0 ❀ int} j chase # sub domain ret: { } j ret Figure 13. An example (assembly) 7. Implementation Our verification is fully mechanized within Coq [5], an interactive theorem prover that uses CiC as its underlying logic, where specifications and proofs are constructed as types and terms in CiC, respectively. Proof checking in Coq is thus type checking of terms in CiC, which is easier to im￾plement and more trustworthy. Coq also provides a rich language for defining both logical and computational con￾structors, with the ability to construct inductive predicates and well-formed recursive functions. Using this, we build the abstract machine model and the sound program logics. The tricky part of the implementation is to obtain the pruned data heap specification Φ/S mentioned in Sec￾tion 5.1, which implies that every label l in its domain sat￾isfies rchrts(S, l). As Φ is a mapping function in the Set universe, we cannot get Φ/S by a case analysis on the proof of the decidability of rchrts(S, l) (if it can be constructed directly), as this will break the proof-irrelevance axiom that is commonly accepted. To solve this problem, we define in the Set universe a well-formed recursive Boolean function which is equivalent to the predicate rchrts, and obtain Φ/S by case analysis on the return value of this function. To simplify the proof construction, we have imple￾mented (in Coq) a verification condition generator (VCGen) for SCAP and proved its correctness. We have also built var￾ious automated proof tactics such as those involving sepa￾ration logic. This results in a proof which is about 1/4 the size of our first proof and is much easier to follow. We omit the implementation of a type-checker for TAL, Lines Component 833 Basic properties and tactics 1941 Abstract machine encoding and lemmas 1263 Finite set library 884 Separation logic library 398 LOCAP 1188 TAL in LOCAP 874 Reachability properties 237 GC Safety for TAL 360 SCAP in LOCAP, VCGen and related tactics 154 Code, specification and proof of chase 2618 Code, specification and proof of the collector 276 Link up chase and the collector in LOCAP Figure 14. Proof script size since it is orthogonal to the main goal of this work. Building a certified TAL type checker is not hard since it has a very straight-forward (and decidable) type-checking algorithm. In Figure 14 we give a breakdown of the size of our proofs for our foundational TAL with certified GC. For each component we give the number of non-empty lines of Coq proof scripts. The work took several man-months (by pro￾grammers who are familiar with the Coq system) to com￾plete. Interested readers can obtain the Coq implementation from our project web site [16]. 8. More related work and conclusion Much work has been done concerning TAL and garbage collector safety in addition to those mentioned in Section 1. TALT [6] considered the impact of garbage collection on the soundness of its type system and mechanically proved GC safety assuming a conservative collector, but the type system interface for the collector is not clearly defined and it is unclear how their definition of GC safety can be used to link with a real collector. Vanderwaart and Crary [25] proposed a type system with an interface for an accurate garbage collector. But again, this work addresses only the mutator (TAL) side of GC safety, while our work comple￾ments their work by mechanically proving the safety of both TAL and the collector, including their interaction. Earlier work on mechanized verification of garbage col￾lectors (such as [13, 10, 4]) focused mostly on abstract al￾gorithms. Our certified collector, on the other hand, is a real machine-level implementation with concrete specifications and it can run directly on real machine. However, our ver￾ification only addresses the safety of the collector, not any liveness properties. The work on CAP systems [27, 22, 8, 7] provides a nice way to build FPCC packages. Our work builds on the CAP0 system in [8] and the OCAP system in [7]. Feng et al. [7] described linking TAL with a certified malloc function

Our idea of using interpretation to specify the TAL/collector Proc.17th Annual IEEE Symp.on Logic in Computer Sci- interface is borrowed from this work. ence,pages 89-100,July 2002. We introduce in this paper a general methodology based [10]K.Havelund.Mechanical verification of a garbage collector on a new variant of FPCC for combining foundational TAL In FMPPTA'99.1999. with a certified garbage collector.We demonstrate the prac- [11]C.Hawblitzel,H.Huang.L.Wittie,and J.Chen.A garbage- collecting typed assembly language.In Proc.3rd ACM SIG- ticality of this approach by linking a typical TAL with a con- PLAN Int'l Workshop on Types in Lang.Design and Impl. servative garbage collector.Our work is fully mechanized ACM Press,Jan.2007. in the Coq proof assistant and the certified programs can be [12]C.A.R.Hoare.An axiomatic basis for computer program- shipped immediately as FPCC packages.In the future we ming.Communications of the ACM,Oct.1969. plan to extend this work by applying our methodology to [13]P.Jackson.Verifying a garbage collection algorithm.In link TAL with more complex accurate collectors. Proc.of 1Ith Int'l Conference on Theorem Proving in Higher Order Logics TPHOLs'98,volume 1479 of Lecture Notes in Computer Science,pages 225-244.Canberra,Sept. Acknowledgment 1998.Springer-Verlag. [14]R.E.Jones.Garbage Collection:Algorithms for Automatic Dynamic Memory Management.Wiley,1996. This research is based on work supported in part by [15]J.Larus.SPIM:a MIPS32 simulator.v7.3.2006. National Science Foundation (of USA)under Grant CCR- [16]C.Lin,A.McCreight,Z.Shao,Y.Chen,and Y.Guo. 0524545,gifts from Intel (USA),Microsoft,and Intel China Foundational typed assembly language with certified Research Center,Innovation Funds from Chinese Academy garbage collection (documents and Cog implementa- of Sciences,and the National Natural Science Foundation tion). http://flint.cs.yale.edu/publications/ of China under Grant No.60673126.Any opinions.find- talgc.html,2007. ings,and conclusions contained in this document are those [17]A.McCreight,Z.Shao,C.Lin,and L.Li.A general frame- of the authors and do not reflect the views of these agencies. work for certifying garbage collectors and their mutators.In PLDI '07:Proc.of the 2007 ACM SIGPLAN conference on Prog.Lang.Design and Impl.,June 2007. References [18]MIPS Technologies,Inc.MIPS32TM Architecture For Pro- grammers Volume II:Instruction Set.v2.50. [19]S.Monnier,B.Saha,and Z.Shao.Principled scavenging [1]A.W.Appel.Foundational proof-carrying code.In Symp.on In Proc.2001 ACM Conf.on Prog.Lang.Design and Impl.. Logic in Comp.Sci.(LICS'01).pages 247-258.IEEE Comp. pages 81-91,New York,2001.ACM Press. Soc..June 2001. [20]G.Morrisett,K.Crary,N.Glew,D.Grossman,R.Samuels, [2]L.Birkedal,N.Torp-Smith,and J.C.Reynolds.Local rea- F.Smith,D.Walker,S.Weirich,and S.Zdancewic.TALx86: soning about a copying garbage collector.In Proc.of the A realistic typed assembly language.In 1999 ACM SIG- 31st ACM symp.on Principles of Prog.Lang..pages 220- PLAN Workshop on Compiler Support for System Software, 231.New York.NY.USA.2004.ACM Press pages 25-35.Atlanta.GA.USA.May 1999. [3]H.-J.Boehm and M.Weiser.Garbage collection in an [21]G.Morrisett,D.Walker,K.Crary,and N.Glew.From sys- uncooperative environment.Software Practice and Exp., tem F to typed assembly language.TOPLAS,21(3):527- 18(9:807-820.1988. 568.1999. [4]L.Burdy.B vs.Coq to prove a garbage collector.In R.J. [22]Z.Ni and Z.Shao.Certified assembly programming with Boulton and P.B.Jackson,editors,14th Int'l Conference embedded code pointers.In Proc.33rd ACM SIGPLAN- on Theorem Proving in Higher Order Logics:Supplemen- SIGACT symp.on Principles of prog.lang.,Jan.2006. tal Proc.,pages 85-97,Sept.2001.Report EDI-INF-RR- [23]C.Paulin-Mohring.Inductive definitions in the system 0046,Division of Informatics,University of Edinburgh. Coq-rules and properties.In Proc.TLCA,volume 664 of [5]Coq Development Team.The Coq proof assistant reference Lecture Notes in Computer Science,1993 manual.Coq release v8.0,Oct.2005. [24]J.C.Reynolds.Separation logic:A logic for shared mutable [6]K.Crary.Toward a foundational typed assembly language. data structures.In LICS '02:Proc.of the 17th Annual IEEE In Proc.of the 30th ACM Symp.on Principles of Prog. Symp.on Logic in Comp.Sci.,pages 55-74.Washington, Lang..pages 198-212,Jan.2003. DC.USA,2002.IEEE Computer Society. [7]X.Feng.Z.Ni,Z.Shao,and Y.Guo.An open framework [25]J.C.Vanderwaart and K.Crary.A typed interface for for foundational proof-carrying code.In Proc.3rd ACM garbage collection.In Proc.Ist ACM SIGPLAN Int'l Work. Workshop on Types in Language Design and Implementa- shop on Types in Lang.Design and Impl.,pages 109-122, tion,pages 67-78.Nice,France,Jan.2007.ACM Press. New York,NY,USA,2003.ACM Press. [26]D.C.Wang and A.W.Appel.Type-preserving garbage col- [8]X.Feng,Z.Shao,A.Vaynberg,S.Xiang,and Z.Ni.Mod- ular verification of assembly code with stack-based control lectors.In Proc.28th ACM Symp.on Principles of Prog. Lang.,pages 166-178.ACM Press.2001. abstractions.In PLDI'06:Proc.of the 2006ACM SIGPLAN [27]D.Yu,N.A.Hamid,and Z.Shao.Building certified libraries conference on Prog.Lang.Design and Impl.,June 2006. for PCC:Dynamic storage allocation.Science of Computer [9]N.A.Hamid,Z.Shao,V.Trifonov,S.Monnier.and Z.Ni.A syntactic approach to foundational proof-carrying code.In Programming,50(1-3):101-127,2004

Our idea of using interpretation to specify the TAL/collector interface is borrowed from this work. We introduce in this paper a general methodology based on a new variant of FPCC for combining foundational TAL with a certified garbage collector. We demonstrate the prac￾ticality of this approach by linking a typical TAL with a con￾servative garbage collector. Our work is fully mechanized in the Coq proof assistant and the certified programs can be shipped immediately as FPCC packages. In the future we plan to extend this work by applying our methodology to link TAL with more complex accurate collectors. Acknowledgment This research is based on work supported in part by National Science Foundation (of USA) under Grant CCR- 0524545, gifts from Intel (USA), Microsoft, and Intel China Research Center, Innovation Funds from Chinese Academy of Sciences, and the National Natural Science Foundation of China under Grant No. 60673126. Any opinions, find￾ings, and conclusions contained in this document are those of the authors and do not reflect the views of these agencies. References [1] A. W. Appel. Foundational proof-carrying code. In Symp. on Logic in Comp. Sci. (LICS’01), pages 247–258. IEEE Comp. Soc., June 2001. [2] L. Birkedal, N. Torp-Smith, and J. C. Reynolds. Local rea￾soning about a copying garbage collector. In Proc. of the 31st ACM symp. on Principles of Prog. Lang., pages 220– 231, New York, NY, USA, 2004. ACM Press. [3] H.-J. Boehm and M. Weiser. Garbage collection in an uncooperative environment. Software Practice and Exp., 18(9):807–820, 1988. [4] L. Burdy. B vs. Coq to prove a garbage collector. In R. J. Boulton and P. B. Jackson, editors, 14th Int’l Conference on Theorem Proving in Higher Order Logics: Supplemen￾tal Proc., pages 85–97, Sept. 2001. Report EDI–INF–RR– 0046, Division of Informatics, University of Edinburgh. [5] Coq Development Team. The Coq proof assistant reference manual. Coq release v8.0, Oct. 2005. [6] K. Crary. Toward a foundational typed assembly language. In Proc. of the 30th ACM Symp. on Principles of Prog. Lang., pages 198–212, Jan. 2003. [7] X. Feng, Z. Ni, Z. Shao, and Y. Guo. An open framework for foundational proof-carrying code. In Proc. 3rd ACM Workshop on Types in Language Design and Implementa￾tion, pages 67–78, Nice, France, Jan. 2007. ACM Press. [8] X. Feng, Z. Shao, A. Vaynberg, S. Xiang, and Z. Ni. Mod￾ular verification of assembly code with stack-based control abstractions. In PLDI ’06: Proc. of the 2006 ACM SIGPLAN conference on Prog. Lang. Design and Impl., June 2006. [9] N. A. Hamid, Z. Shao, V. Trifonov, S. Monnier, and Z. Ni. A syntactic approach to foundational proof-carrying code. In Proc. 17th Annual IEEE Symp. on Logic in Computer Sci￾ence, pages 89–100, July 2002. [10] K. Havelund. Mechanical verification of a garbage collector. In FMPPTA’99, 1999. [11] C. Hawblitzel, H. Huang, L. Wittie, and J. Chen. A garbage￾collecting typed assembly language. In Proc. 3rd ACM SIG￾PLAN Int’l Workshop on Types in Lang. Design and Impl. ACM Press, Jan. 2007. [12] C. A. R. Hoare. An axiomatic basis for computer program￾ming. Communications of the ACM, Oct. 1969. [13] P. Jackson. Verifying a garbage collection algorithm. In Proc. of 11th Int’l Conference on Theorem Proving in Higher Order Logics TPHOLs’98, volume 1479 of Lecture Notes in Computer Science, pages 225–244, Canberra, Sept. 1998. Springer-Verlag. [14] R. E. Jones. Garbage Collection: Algorithms for Automatic Dynamic Memory Management. Wiley, 1996. [15] J. Larus. SPIM: a MIPS32 simulator. v7.3, 2006. [16] C. Lin, A. McCreight, Z. Shao, Y. Chen, and Y. Guo. Foundational typed assembly language with certified garbage collection (documents and Coq implementa￾tion). http://flint.cs.yale.edu/publications/ talgc.html, 2007. [17] A. McCreight, Z. Shao, C. Lin, and L. Li. A general frame￾work for certifying garbage collectors and their mutators. In PLDI ’07: Proc. of the 2007 ACM SIGPLAN conference on Prog. Lang. Design and Impl., June 2007. [18] MIPS Technologies, Inc. MIPS32TM Architecture For Pro￾grammers Volume II: Instruction Set, v2.50. [19] S. Monnier, B. Saha, and Z. Shao. Principled scavenging. In Proc. 2001 ACM Conf. on Prog. Lang. Design and Impl., pages 81–91, New York, 2001. ACM Press. [20] G. Morrisett, K. Crary, N. Glew, D. Grossman, R. Samuels, F. Smith, D. Walker, S. Weirich, and S. Zdancewic. TALx86: A realistic typed assembly language. In 1999 ACM SIG￾PLAN Workshop on Compiler Support for System Software, pages 25–35, Atlanta, GA, USA, May 1999. [21] G. Morrisett, D. Walker, K. Crary, and N. Glew. From sys￾tem F to typed assembly language. TOPLAS, 21(3):527– 568, 1999. [22] Z. Ni and Z. Shao. Certified assembly programming with embedded code pointers. In Proc. 33rd ACM SIGPLAN￾SIGACT symp. on Principles of prog. lang., Jan. 2006. [23] C. Paulin-Mohring. Inductive definitions in the system Coq—rules and properties. In Proc. TLCA, volume 664 of Lecture Notes in Computer Science, 1993. [24] J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS ’02: Proc. of the 17th Annual IEEE Symp. on Logic in Comp. Sci., pages 55–74, Washington, DC, USA, 2002. IEEE Computer Society. [25] J. C. Vanderwaart and K. Crary. A typed interface for garbage collection. In Proc. 1st ACM SIGPLAN Int’l Work￾shop on Types in Lang. Design and Impl., pages 109–122, New York, NY, USA, 2003. ACM Press. [26] D. C. Wang and A. W. Appel. Type-preserving garbage col￾lectors. In Proc. 28th ACM Symp. on Principles of Prog. Lang., pages 166–178. ACM Press, 2001. [27] D. Yu, N. A. Hamid, and Z. Shao. Building certified libraries for PCC: Dynamic storage allocation. Science of Computer Programming, 50(1-3):101–127, 2004