(StPred) =RegFileX→Heap→Prop MAIN: (True,A1.GI) A1≌i.0≤i<100 (Guar) 总G RegFileX→Heap→Heap→Prop move to ro →(datai=dadl) (Assume） A :=RegFileX→Heap→Heap→Prop addiu t1 ro 100 Gi≌Tue (CdSpec】 (P,总A,G L00P: (p,G2,A2,G) beg to t1 CONT A2≌i.(0≤i<100Ai≥o) Hf∈dom(Ψ)：Ψ；C FCMAP{Ψ'(f)}:C(E) jal YIELD →(daa[d=dawd[j) (CDHP) sw to data to 平FCMAP C:Ψ G2≌i.(0≤i<100Ai<ol) jal YILED →(daa[d=datd i) move a0 CHLD 平(E+1)=(p,G,A,G)瓜，Hp鹿H一→ěRHH move al to 成，H,H'p成H→A反HH→p成 jal SPAWN A3≌i.(0≤i<100Ai>[o]) -(YIELD) →(daa[同=dard[) Ψ；C FCMAP{p,总，A,G)}壮：jalyield (p.G3,A3,G3 jal YIELD G3≌i.(0≤i<100Ai≤ol) →(daua同=data i) Ψ(f+1)=(p,G,A,G)RH.pRH→意RHH addiu toto 1 成，HH'p反H→A成HH一P成H jal YIELD jLOOP A True 成，HpRH→平(@{a0)=(p',G,A',cAp'夜H 成，HH'p'成H→A'成HH一p'成H CONT: (p',G4,A4,G4） G4≌A1 jal EXIT AA G'G GA GA (SPAWN) CHLD: (p”A.G) A2datala]=datd'(al 平：C FCMAP{p总，A,G)}f:jal spawn lw to data al G≌i.(0≤i<100Ai≠[a]） jal YIELD →(daua[d=datd[) 成，H.p成H→点成HH addiu toto 1 (EXIT) 平：CHCMAP{p,总A.G)}f:jal exit jal YIELD p≌0≤ol<100A]=100 where sw to data al p≌o=100 G鸟A成.H.H.G原HH→A顶HH jal EXIT p"≌0≤a<100 Figure 7.CMAP Figure 8.Unbounded thread creation specifications 0.Note that code labels f may be mapped to 平Ex卜CMAP CEX:平Ex OSCAP Or 0CMAP. In OCAP-light,the code specifications written in differ- ent languages should have interaction to form a cooperative 5.Linking CTL to user programs system.Accordingly,the interpretation functionis used to translate the specification 0 to assertion a which is used at The main purpose of CTL is to provide a certified run- OCAP-light level.Each assertion a is a CiC predicate over time for multithreaded user programs.In Section 3.3,we y and machine state S.With interpretation functions,the have already certified a thread library CTL and a multi- specific inference rules of program logics can be proved as threaded program.As to build safety multithreaded pro- lemmas based on a thin layer of Hoare-style inference rules grams,just providing a certified library is insufficient.In over meta-logic.Then the soundness of a program logic is this section,we will complete our work by linking the cer- reduced to the soundness of OCAP-light. tified multithreaded user programs with CTL. The soundness and correctness theorem of OCAP-light As stated in Section 1,we choose OCAP as our com- ensures safety,stated in Section 2.It says that any well- mon certification framework.OCAP uses an extensible and formed program will run forever without reaching any un- heterogeneous program specification.OCAP rules are ex- defined state in Figure 2,and any reachable states satisfy pressive enough to embed most existing verification logic the corresponding assertions in Y. systems for low-level code.We can embed a program logic Theorem 1 (OCAP-light-Soundness and Correctness). and prove system specific rules/axioms as lemmas based on an interpretation function and OCAP rules.Thus,the safety If (C,S),for all natural number n there exists a s= program certified in foreign logic systems can be translated (',H',pc'),such that (C.S)(C,S');and if pc',then down to the OCAP level and then linked with CTL. IΨ(E)IΨS. 5.1.OCAP-light 5.2.Embedding SCAP in OCAP-light. For simplicity,we present a light-weight OCAP(OCAP- As stated in Section 3.3,OscAP is a pair of predicates light)framework in Figure 9.OCAP-light uses heteroge- (p,g).The predicate p is the precondition and the guarantee neous code specifications 0 to support specification lan- g specifies the state at the (function-call)return point and guages of both SCAP and CMAP.The code heap specifi- the relationship between the current point and return point. cation is defined as a map from code labels f to their In our TM,the jal instruction is used to perform function(StPred) p ::= RegFileX → Heap → Prop (Guar) gˇ,G ::= RegFileX → Heap → Heap → Prop (Assume) A ::= RegFileX → Heap → Heap → Prop (CdSpec) θCMAP ::= (p,gˇ,A,G) ∀ f ∈ dom(Ψ′ ) : Ψ;C ⊢CMAP {Ψ′ (f)}f : C(f) Ψ ⊢CMAP C : Ψ′ (CDHP) Ψ(f+1) = (p,G,A,G) ∀R˜ ,H.p R H˜ → gˇ R H H ˜ ∀R˜ ,H,H′ .p R H˜ → A R H H ˜ ′ → p R H˜ ′ Ψ;C ⊢CMAP {(p,gˇ,A,G)}f : jal yield (YIELD) Ψ(f+1) = (p,G,A,G) ∀R˜ ,H.p R H˜ → gˇ R H H ˜ ∀R˜ ,H,H′ .p R H˜ → A R H H ˜ ′ → p R H˜ ′ ∀R˜ ,H.p R H˜ → Ψ(R˜ {a0}) = (p ′ ,G ′ ,A ′ ,G ′ ) ∧ p ′ R H˜ ∀R˜ ,H,H′ .p ′ R H˜ → A ′ R H H ˜ ′ → p ′ R H˜ ′ A ◦⇒ A ′ G ′ ◦⇒ G G ◦⇒ A ′ G ′ ◦⇒ A Ψ;C ⊢CMAP {(p,gˇ,A,G)}f : jal spawn (SPAWN) ∀R˜ ,H.p R H˜ → gˇ R H H ˜ Ψ;C ⊢CMAP {(p,gˇ,A,G)}f : jal exit (EXIT) where G ◦⇒ A , ∀R˜ ,H,H′ .G R H H ˜ ′ → A R H H ˜ ′ Figure 7. CMAP ΨEX ⊢CMAP CEX : ΨEX 5. Linking CTL to user programs The main purpose of CTL is to provide a certified run￾time for multithreaded user programs. In Section 3.3, we have already certified a thread library CTL and a multi￾threaded program. As to build safety multithreaded pro￾grams, just providing a certified library is insufficient. In this section, we will complete our work by linking the cer￾tified multithreaded user programs with CTL. As stated in Section 1, we choose OCAP as our com￾mon certification framework. OCAP uses an extensible and heterogeneous program specification. OCAP rules are ex￾pressive enough to embed most existing verification logic systems for low-level code. We can embed a program logic and prove system specific rules/axioms as lemmas based on an interpretation function and OCAP rules. Thus, the safety program certified in foreign logic systems can be translated down to the OCAP level and then linked with CTL. 5.1. OCAP-light For simplicity, we present a light-weight OCAP (OCAP￾light) framework in Figure 9. OCAP-light uses heteroge￾neous code specifications θ to support specification lan￾guages of both SCAP and CMAP. The code heap specifi- cation Ψ is defined as a map from code labels f to their MAIN: (True,A1,G1) move t0 r0 addiu t1 r0 100 LOOP: (p,G2,A2,G2) beq t0 t1 CONT jal YIELD sw t0 data t0 jal YILED move a0 CHLD move a1 t0 jal SPAWN (p,G3,A3,G3) jal YIELD addiu t0 t0 1 jal YIELD j LOOP CONT: (p ′ ,G4,A4,G4) jal EXIT CHLD: (p ′′ ,A,G) lw t0 data a1 jal YIELD addiu t0 t0 1 jal YIELD sw t0 data a1 jal EXIT A1 , ∀i.0 ≤ i < 100 → (data[i] = data′ [i]) G1 , True A2 , ∀i.(0 ≤ i < 100 ∧ i ≥ [t0]) → (data[i] = data′ [i]) G2 , ∀i.(0 ≤ i < 100 ∧ i < [t0]) → (data[i] = data′ [i]) A3 , ∀i.(0 ≤ i < 100 ∧ i > [t0]) → (data[i] = data′ [i]) G3 , ∀i.(0 ≤ i < 100 ∧ i ≤ [t0]) → (data[i] = data′ [i]) A4 , True G4 , A1 A , data[a1] = data′ [a1] G , ∀i.(0 ≤ i < 100 ∧ i 6= [a1]) → (data[i] = data′ [i]) p , 0 ≤ [t0] < 100 ∧ [t1] = 100 p ′ , [t0] = 100 p ′′ , 0 ≤ [a1] < 100 Figure 8. Unbounded thread creation specifications θ. Note that code labels f may be mapped to θSCAP or θCMAP. In OCAP-light, the code specifications written in differ￾ent languages should have interaction to form a cooperative system. Accordingly, the interpretation function [[ ]] is used to translate the specification θ to assertion a which is used at OCAP-light level. Each assertion a is a CiC predicate over Ψ and machine state S. With interpretation functions, the specific inference rules of program logics can be proved as lemmas based on a thin layer of Hoare-style inference rules over meta-logic. Then the soundness of a program logic is reduced to the soundness of OCAP-light. The soundness and correctness theorem of OCAP-light ensures safety, stated in Section 2. It says that any well￾formed program will run forever without reaching any un￾defined state in Figure 2, and any reachable states satisfy the corresponding assertions in Ψ. Theorem 1 (OCAP-light - Soundness and Correctness). If Ψ ⊢ (C,S), for all natural number n there exists a S ′ = (R ′ ,H′ ,pc′ ), such that (C,S) 7−→n (C,S ′ ); and if pc′ ∈ Ψ, then [[Ψ(f)]] Ψ S ′ . 5.2. Embedding SCAP in OCAP-light. As stated in Section 3.3, θSCAP is a pair of predicates (p,g). The predicate p is the precondition and the guarantee g specifies the state at the (function-call) return point and the relationship between the current point and return point. In our TM, the jal instruction is used to perform function