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≤1<ed)} markbit(val)=BLACK;stack_push(val); vptr(1) 蚂 1∈ptrs 2 gc(0[ roots 些 {r17,r18,r31,r0} mark_field(root1); vptr(1) (REFL) 。w reach(H,1,1) mark_field(rootn); while(!stack_empty()){ vptr(1)vptr(1')reach(H,1",1') ptr stack_pop(); H(1)=1"VH(1+4)=1" (NEXT) mark_field(ptr->first); 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 < ST || 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 < ED; addr ++) if (markbit(addr) == WHITE){ 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