A Certified Thread Library for Multithreaded User Programs

A Certified Thread Library for Multithreaded User Programs Yu Guo Xinyu Jiang Yiyun Chen Chunxiao Lin Department of Computer Science and Technology University of Science and Technology of China Hefei,Anhui 230026,China Aguoyu,wewewe,cxlin3 @mail.ustc.edu.cn yiyun @ustc.edu.cn Abstract language level.Xu et al.[24]proposed a logic system to verify deadlock freedom and convergence by rely-guarantee Ensuring the safety of multithreaded software is a task method.Model checkers [9]are developed to verify con- both important and challenging.Currently,most ap- current programs with a fixed number of threads.Flanagan proaches focus on the safety of multithreaded programs et al.[10]used A-G method to check java multithreaded rather than the runtime based on which those concurrent programs.CCAP [26]applied the A-G method to the as- programs run.In order to fundamentally solve this problem, sembly code based on a concurrent abstract machine with a method of ensuring the safety of the runtime should be de- a built-in thread scheduler.CMAP [7]proposed by Feng veloped.Such a runtime could be organized as a thread and Shao supports thread-modular reasoning with dynamic library typically. thread creation and termination. This paper presents the development and certification of However,most of the previous work concentrates on a simple but realistic thread library.The thread library safe multithreaded programming,not the runtime (thread provides common multi-threading features such as dynamic library).Nonetheless,only when the safety of underlying thread creation,termination and joining as well.This li- thread library is guaranteed,can the programs verified by brary also carries machine-checkable proof which guaran- their methods be safe.The thread library often contains tees the library does not violate the safety policies.This lurking flaws which are subtle and hard to detect and fix paper also presents an approach to link the library to exist- due to its complexity,so a fully certified thread library is of ing certified multithreaded user programs to form an inte- urgent necessity.However,the certifying task is full of chal- grated foundational proof-carrying code (FPCC)package. lenges.A thread library generally involves sophisticated Comparing with the uncertified libraries,our work makes manipulations on memory and machine context.The invari- multithreaded applications much more reliable. ants are subtle and hard to specify.Furthermore,the control flow transfers between threads and the scheduler of thread library increase the certification burden. 1.Introduction In this paper,we propose a simple but realistic certified thread library,named CTL,which implements dynamic Multithreaded software is widely employed in realistic thread creation,termination and joining.CTL is written applications.For example,in a web browser,it is common in low-level code and certified thoroughly in the program that while one thread is displaying images or text,another logic SCAP [8].The certification convinces us that the se- thread is retrieving data from the Internet.However,the mantics of CTL conform to its formal specifications.The safety of multithreaded programs is hard to ensure,since the code and its specifications,as well as corresponding safety interference between the simultaneously executing threads proof are all encoded in a foundational mathematical logic must be taken into account. and packed together to form a foundational proof-carrying Many efforts have been devoted to the verification of code (FPCC)package [1,12],in which a neat and consis- concurrent programs.Jones [13]introduced the composi- tent logic system instead of the entire complicated thread tional rely-guarantee method (or A-G method)[26,7,5]to library has to be trusted.In this way,not only multithreaded describe the state changes performed by the environment programs but also CTL itself can be reasoned about and ver- and by the program respectively.Lamport proposed the ified on a solid and rigorous base. Temporal Logic of Action (TLA)[14]as a logic for speci- Even if we have the individual safety proof of them,it is fying and reasoning about concurrent programs at the high- still inadequate to ensure the safety of the interactions be-

A Certified Thread Library for Multithreaded User Programs Yu Guo Xinyu Jiang Yiyun Chen Chunxiao Lin Department of Computer Science and Technology University of Science and Technology of China Hefei, Anhui 230026, China {guoyu,wewewe,cxlin3}@mail.ustc.edu.cn yiyun@ustc.edu.cn Abstract Ensuring the safety of multithreaded software is a task both important and challenging. Currently, most ap￾proaches focus on the safety of multithreaded programs rather than the runtime based on which those concurrent programs run. In order to fundamentally solve this problem, a method of ensuring the safety of the runtime should be de￾veloped. Such a runtime could be organized as a thread library typically. This paper presents the development and certification of a simple but realistic thread library. The thread library provides common multi-threading features such as dynamic thread creation, termination and joining as well. This li￾brary also carries machine-checkable proof which guaran￾tees the library does not violate the safety policies. This paper also presents an approach to link the library to exist￾ing certified multithreaded user programs to form an inte￾grated foundational proof-carrying code (FPCC) package. Comparing with the uncertified libraries, our work makes multithreaded applications much more reliable. 1. Introduction Multithreaded software is widely employed in realistic applications. For example, in a web browser, it is common that while one thread is displaying images or text, another thread is retrieving data from the Internet. However, the safety of multithreaded programs is hard to ensure, since the interference between the simultaneously executing threads must be taken into account. Many efforts have been devoted to the verification of concurrent programs. Jones [13] introduced the composi￾tional rely-guarantee method (or A-G method) [26, 7, 5] to describe the state changes performed by the environment and by the program respectively. Lamport proposed the Temporal Logic of Action (TLA) [14] as a logic for speci￾fying and reasoning about concurrent programs at the high￾language level. Xu et al. [24] proposed a logic system to verify deadlock freedom and convergence by rely-guarantee method. Model checkers [9] are developed to verify con￾current programs with a fixed number of threads. Flanagan et al. [10] used A-G method to check java multithreaded programs. CCAP [26] applied the A-G method to the as￾sembly code based on a concurrent abstract machine with a built-in thread scheduler. CMAP [7] proposed by Feng and Shao supports thread-modular reasoning with dynamic thread creation and termination. However, most of the previous work concentrates on safe multithreaded programming, not the runtime (thread library). Nonetheless, only when the safety of underlying thread library is guaranteed, can the programs verified by their methods be safe. The thread library often contains lurking flaws which are subtle and hard to detect and fix due to its complexity, so a fully certified thread library is of urgent necessity. However, the certifying task is full of chal￾lenges. A thread library generally involves sophisticated manipulations on memory and machine context. The invari￾ants are subtle and hard to specify. Furthermore, the control flow transfers between threads and the scheduler of thread library increase the certification burden. In this paper, we propose a simple but realistic certified thread library, named CTL, which implements dynamic thread creation, termination and joining. CTL is written in low-level code and certified thoroughly in the program logic SCAP [8]. The certification convinces us that the se￾mantics of CTL conform to its formal specifications. The code and its specifications, as well as corresponding safety proof are all encoded in a foundational mathematical logic and packed together to form a foundational proof-carrying code (FPCC) package [1, 12], in which a neat and consis￾tent logic system instead of the entire complicated thread library has to be trusted. In this way, not only multithreaded programs but also CTL itself can be reasoned about and ver￾ified on a solid and rigorous base. Even if we have the individual safety proof of them, it is still inadequate to ensure the safety of the interactions be-

Link 2.Basic settings CTL threaded proof program In order to certify CTL in the FPCC framework.we linked SCAP program CMAP formalize all the related concepts into a mechanized meta- logic.In other words,the machine model,the code of CTL OCAP its specifications,program logics and related safety proof Cic(Coq) are all based on a common formal logic,resulting in smaller trusted computing base for safety.In this section,we will Figure 1.The OCAP framework present these basic settings. tween CTL and multithreaded programs due to the absence The mechanized meta-Logic.We use the calculus of in- of safety proof for the code with respect to linkage.Al- ductive constructions (CiC)[21]as our meta-logic.CiC is though the construction of such safety proof is possible,it supported by the Cog proof assistant [3],which we use to is non-trivial because of the differences between specifica- implement the work presented in this paper. tion languages,as well as certification methods'variety. Recently,Feng et al.[6]proposed an open certification The target machine.A MIPS-style [15]target machine framework(OCAP)to support inter-operation of different (TM)is chosen as our machine model on which our thread certification systems.OCAP serves as a common layer in library runs.We omit some physical machine features which different program logics can be embedded. irrelevant to threading,such as address alignment,bits- Based on OCAP,we demonstrate in this paper the link- arithmetic etc..The target machine and its operational se- age between CTL certified in SCAP and user programs cer- mantics are formally defined in Figure 2.A machine pro- tified in CMAP.and construct the extra safety proof of in- gram P contains a code heap C and an updatable state S.A teraction,as shown in Figure 1. code heap C is a segment of memory mapping addresses to The main contributions of our work are as follows: machine instructions,but C is read-only and isolated from the mutable data heap H.The state S,which specifies the We describe,specify,and certify a simple but real- execution of the program,consists of a register file,muta- istic thread library CTL.It provides common multi- ble data heap H and the program counter pc.The target threading features including thread scheduling,dy- machine has 32 general-purpose registers.Following the namic thread creation,termination and joining. MIPS convention,the table below shows the register alias We define formal specifications to capture the seman- and usage. tics of CTL routines.This library carries machine- checkable proof which ensures that the library does not r0 IO always zero vo-v1 r2-r3 return values a0-a3 r4-r7 arguments to-t7 rs-ris temporary violate the safety policies. k0-k1 r26-r27 reserved ra r31 return address Meanwhile,we adapt and embed CMAP in a simpli- The basic TM instruction set covers the common MIPS fied OCAP framework.Thus.CTL can be linked to instructions for arithmetics,jump,conditional branch and the user programs certified in CMAP to construct an load/store.It is easy to add more instructions in our TM. integrated mechanized FPCC package.As far as we The relation PP indicates that the program state P know,CTL is the first thread library which can be steps to the program state P.The relation PP means safely linked to multithreaded user programs. that P reaches P in k steps,and*is the reflexive and We have formalized the work presented in this paper, transitive closure of the step relation.The auxiliary func- including CTL,OCAP.CMAP,and their soundness proof, tion Next(-)specifies the state transition according to the in the Coq proof assistant [3].Interested readers may find operational semantics instruction t.We use the notation S them on our web site [11]. to denote Next(S). The remainder of this paper is organized as follows:Sec- tion 2 presents the formalization of basic settings.In Sec- Safety.Safety of the program means that:(i)the execution tion 3 we describe and certify the CTL library.We dis- of the programs in CTL will not go stuck;(ii)the code of cuss the verification framework CMAP in which the mul- CTL satisfies certain safety specifications.The code heap tithreaded programs are certified in Section 4.Section 5 specification y is a map from code labels f to code specifi- shows the linkage of CTL and user programs in a simpli- cations 0,as defined below: fied OCAP framework.Section 6 is related work and the (CdSpec）6=… conclusion. (CHSpec）Ψ：={fo}

￾
              
 



  ￾        
                   Figure 1. The OCAP framework tween CTL and multithreaded programs due to the absence of safety proof for the code with respect to linkage. Al￾though the construction of such safety proof is possible, it is non-trivial because of the differences between specifica￾tion languages, as well as certification methods’ variety. Recently, Feng et al. [6] proposed an open certification framework (OCAP) to support inter-operation of different certification systems. OCAP serves as a common layer in which different program logics can be embedded. Based on OCAP, we demonstrate in this paper the link￾age between CTL certified in SCAP and user programs cer￾tified in CMAP, and construct the extra safety proof of in￾teraction, as shown in Figure 1. The main contributions of our work are as follows: • We describe, specify, and certify a simple but real￾istic thread library CTL. It provides common multi￾threading features including thread scheduling, dy￾namic thread creation, termination and joining. • We define formal specifications to capture the seman￾tics of CTL routines. This library carries machine￾checkable proof which ensures that the library does not violate the safety policies. • Meanwhile, we adapt and embed CMAP in a simpli- fied OCAP framework. Thus, CTL can be linked to the user programs certified in CMAP to construct an integrated mechanized FPCC package. As far as we know, CTL is the first thread library which can be safely linked to multithreaded user programs. We have formalized the work presented in this paper, including CTL, OCAP, CMAP, and their soundness proof, in the Coq proof assistant [3]. Interested readers may find them on our web site [11]. The remainder of this paper is organized as follows: Sec￾tion 2 presents the formalization of basic settings. In Sec￾tion 3 we describe and certify the CTL library. We dis￾cuss the verification framework CMAP in which the mul￾tithreaded programs are certified in Section 4. Section 5 shows the linkage of CTL and user programs in a simpli- fied OCAP framework. Section 6 is related work and the conclusion. 2. Basic settings In order to certify CTL in the FPCC framework, we formalize all the related concepts into a mechanized meta￾logic. In other words, the machine model, the code of CTL, its specifications, program logics and related safety proof are all based on a common formal logic, resulting in smaller trusted computing base for safety. In this section, we will present these basic settings. The mechanized meta-Logic. We use the calculus of in￾ductive constructions (CiC) [21] as our meta-logic. CiC is supported by the Coq proof assistant [3], which we use to implement the work presented in this paper. The target machine. A MIPS-style [15] target machine (TM) is chosen as our machine model on which our thread library runs. We omit some physical machine features irrelevant to threading, such as address alignment, bits￾arithmetic etc.. The target machine and its operational se￾mantics are formally defined in Figure 2. A machine pro￾gram P contains a code heap C and an updatable state S. A code heap C is a segment of memory mapping addresses to machine instructions, but C is read-only and isolated from the mutable data heap H. The state S, which specifies the execution of the program, consists of a register file, muta￾ble data heap H and the program counter pc. The target machine has 32 general-purpose registers. Following the MIPS convention, the table below shows the register alias and usage. r0 r0 always zero v0−v1 r2 −r3 return values a0−a3 r4 −r7 arguments t0−t7 r8 −r15 temporary k0−k1 r26 −r27 reserved ra r31 return address The basic TM instruction set covers the common MIPS instructions for arithmetics, jump, conditional branch and load/store. It is easy to add more instructions in our TM. The relation P 7−→ P ′ indicates that the program state P steps to the program state P ′ . The relation P 7−→k P ′ means that P reaches P ′ in k steps, and 7−→∗ is the reflexive and transitive closure of the step relation. The auxiliary func￾tion Nextι( ) specifies the state transition according to the operational semantics instruction ι. We use the notation Sˆ ι to denote Nextι(S). Safety. Safety of the program means that:(i) the execution of the programs in CTL will not go stuck; (ii) the code of CTL satisfies certain safety specifications. The code heap specification Ψ is a map from code labels f to code specifi- cations θ, as defined below: (CdSpec) θ ::= ··· (CHSpec) Ψ ::= {f ❀ θ} ∗

(Program） P =(C,S) &b1 (CodeHeap) 0 :={f+1}" (State) :=(R,H,pc) cth p日分T.T (Memory) H ={1*} hd (RegFile) = frw 34 (Register) ={r4}e031y (Labels)f,1,pc ::n (nat nums) (Word) :=i (integers) (nstr） 1 :=addu rdrsr addiurdrsw Figure 3.Core data structures of CTL subu rd rs r subiurd rsw move rrslirw 1wIt w(rs)SWI(Is) certifications of every routine of CTL.So we concentrate begrs r f bgtz rs f on certifying the yielding routine,which is an essential part jf jalf jrr, of the thread library. (C,但，R,pc)一(C,NextC(pc)(H,Rpc)= 3.1.Overview if C(pc)=1=then Next (H,R.pc)=S= addu rdrsrr (H,R{rdR(r,)+R(r:)}.pc+1) CTL is a lightweight implementation of thread library whose thread model is similar to GNU Pth [4]or FSU 1wr:v(rs) (HRH(R(r,)+w)}:pc+1) when R(r,)+w∈dom(H) pthreads [16],in which threads are implemented in the user- SWI:W(Is) (HR(r:)+R()).R.pc+1) space and the machine context switching is performed by an when R(r:)+w∈dom(Hl) application library without knowledge of the kernel.This beg rs r:f (但，R,pc+1)when R(r)≤R(s) model does not rely on the kernel threads and is adaptable to (H.R.f)when R(r,)>R(r,) various platforms.CTL supports non-preemptive schedul- jalf (H,R{r31+pc+1},f) ing and can directly run on the processors without interrupts jrrs (H.R.R(r,)) handling,for example,the SPIM simulator [20].CTL is fully certified at the assembly level,so the certification of the compiler correctness can be spared. Figure 2.The target machine TM 3.2.Thread model Note that e has different form in different program logic and is defined in Section 5.1. We use pseudo C code to illustrate the prototype of the core data structures and API of CTL. Separation logic.We define some notations common in The core data structures in the CTL space are shown in separation logic [22,19].These notations are defined as Figure 3.The main data structure is a queue,whose el- shorthand and are used in the specifications of CTL to spec- ements are called thread control block(TCB).Each TCB ify the data heap. identifies one dynamic thread and contains one thread id and corresponding executing context.The TCB is proto- HIkA叁AH typed by: AI*A2H.3H1,H2.H1=HAI AH2 IA2 Top H.True struct t_tcb word id; 1→gH.1≠NU儿LAH={1w} /米unique id*/ word pc; /米program counter*/ 1→.H.3w.(HIk1→ word state;/ready,dead or wait * 1一w1,,m兰1→1*1+1一2*..*1十(n-1)一Wm word wait_id;/id of thread to wait * word regfile[28] We use HA if the heap predicate A is valid with H. /array for saving registers * A1 A2 asserts the heapH in which H AI and H2 A2 hold respectively.Top is valid with any heap.1 Meanwhile,an isolated TCB identifies the current running asserts a heap with only one memory cell,at address 1 with thread.Note that the global pointers referring to these data content w. structures are stored in a global pointer array. CTL provides a threading API: 3.CTL:a certified thread library void ctl_yield(void); word ctl_spawn((*void)()); In this section,we give a detailed description of CTL. word ctl_exit(); Because of space limitations,we cannot fully discuss the word ctl_join(int thread_id);

(Program) P ::= (C,S) (CodeHeap) C ::= {f ❀ ι} ∗ (State) S ::= (R,H,pc) (Memory) H ::= {l ❀ w} ∗ (RegFile) R ::= {r ❀ w} ∗ (Register) r ::= {rk} k∈{0...31} (Labels) f,l,pc ::= n (nat nums) (Word) w ::= i (integers) (Instr) ι ::= addu rd rs rt | addiu rd rs w | subu rd rs rt | subiu rd rs w | move rd rs | li rd w | lw rt w(rs) | sw rt w(rs) | beq rs rt f | bgtz rs f | j f | jal f | jr rs (C,(H,R,pc)) 7−→ (C,NextC(pc) (H,R,pc)) = if C(pc) = ι = then Nextι(H,R,pc) = Sˆ ι = addu rd rs rt (H,R{rd ❀R(rs)+R(rt)},pc+1) lw rt w(rs) (H,R{rt ❀H(R(rs)+w)},pc+1) when R(rs)+w ∈ dom(H) sw rt w(rs) (H{R(rs)+w❀R(rt)},R,pc+1) when R(rs)+w ∈ dom(H) beq rs rt f (H,R,pc+1) when R(rs)≤R(rt) (H,R,f) when R(rs)>R(rt) jal f (H,R{r31❀pc+1},f) jr rs (H,R,R(rs)) Figure 2. The target machine TM Note that θ has different form in different program logic and is defined in Section 5.1. Separation logic. We define some notations common in separation logic [22, 19]. These notations are defined as shorthand and are used in the specifications of CTL to spec￾ify the data heap. H ° A , A H A1 ∗A2 , λH.∃H1,H2 .H1⊎H2 =H∧H1 ° A1 ∧H2 ° A2 Top , λH.True l 7→ w , λH.l6=NULL∧H={l❀w} l 7→ , λH.∃w.(H ° l 7→ w) l 7→ w1,...,wn , l 7→ w1 ∗ l+1 7→ w2 ∗ ... ∗ l+(n−1) 7→ wn We use H ° A if the heap predicate A is valid with H. A1 ∗ A2 asserts the heap H1 ⊎H2 in which H1 ° A1 and H2 ° A2 hold respectively. Top is valid with any heap. l 7→ w asserts a heap with only one memory cell, at address l with content w. 3. CTL: a certified thread library In this section, we give a detailed description of CTL. Because of space limitations, we cannot fully discuss the ￾

      ￾
￾ ￾
￾ ￾ ￾ ￾ ￾ ￾ ￾ ￾ ￾ ￾ ￾ ￾ ￾ ￾ ￾ Figure 3. Core data structures of CTL certifications of every routine of CTL. So we concentrate on certifying the yielding routine, which is an essential part of the thread library. 3.1. Overview CTL is a lightweight implementation of thread library whose thread model is similar to GNU Pth [4] or FSU pthreads [16], in which threads are implemented in the user￾space and the machine context switching is performed by an application library without knowledge of the kernel. This model does not rely on the kernel threads and is adaptable to various platforms. CTL supports non-preemptive schedul￾ing and can directly run on the processors without interrupts handling, for example, the SPIM simulator [20]. CTL is fully certified at the assembly level, so the certification of the compiler correctness can be spared. 3.2. Thread model We use pseudo C code to illustrate the prototype of the core data structures and API of CTL. The core data structures in the CTL space are shown in Figure 3. The main data structure is a queue, whose el￾ements are called thread control block(TCB). Each TCB identifies one dynamic thread and contains one thread id and corresponding executing context. The TCB is proto￾typed by: struct t_tcb { word id; /* unique id */ word pc; /* program counter */ word state; /* ready, dead or wait */ word wait_id; /* id of thread to wait */ word regfile[28]; /* array for saving registers */ }; Meanwhile, an isolated TCB identifies the current running thread. Note that the global pointers referring to these data structures are stored in a global pointer array. CTL provides a threading API: void ctl_yield(void); word ctl_spawn((* void)()); word ctl_exit(); word ctl_join(int thread_id);

(StPred) p =State→Pop (Thread-id): (GrPred) g=State→State→Pop (RegFileX):=Rfoko1ra} (CdSpec) 0sCAP ::(P,g) (TCB)Tcb:=(pc,成，ts,om) Hf∈dom(Ψ)：平：C FsCAP{Ψ'(E)}f:C(E) (Th State)ts ::=ready dead wait (CDHP) (Th Queue)Q:={Tcb}UQ 平FsCAP C:Y t=ja1'(p,g)=ΨE)(p",g")=ΨE+1) S.pS一p'S Figure 5.Specification constructs of CTL S,S.S.pc-f→pS-gsS →p"SA(s".g"SS”→gSS"） partial registers file R and a thread state ts.A partial regis- VS,S'.g'SS'-S.R(ra)=S'.R(ra) (CALL) ters file R is a registers file R excluding ro,ko,k1 and ra. Ψ：C HsCAP{p,g)}f:ja1f The registers ko and k1 are preserved for thread scheduling 1=jrra S.pS→gSS and then unusable in user programs.Because the register ro (RET) always holds the value of zero,it needn't to be saved.When :C HsCAP {(p.g))f:jr ra ra is used to call the routines of CTL,its value is saved in the Tcb.pc field.A thread queue Q is a dictionary mapping Figure 4.SCAP o to Tcb and constructed inductively. The routine ctl_yield()causes the current thread to Formal core data structures.We formally specify the yield its execution in favor of another thread with certain core data structures that are used in our thread library CTL scheduling policy.ctl_yield()stores the execution con- As shown in Figure 3,the memory space for CTL is divided text in the queue of the TCBs and picks up one TCB, into four parts,the global pointer array,the isolated TCB for loads it and switches the control to the new continuation. current thread,the thread queue and the free-block list. ct1_yield()adopts the round-robin scheduling algorithm. Thread creation is achieved by using ctl_spawn()with Core(o.Tcb.Q)3gbl.gbl cth,hd,tl.fl a parameter of start code pointer.This function first allo- *QNode(crh,6.Tcb,NULL)TQ(hd,tl,Q)GoodL(fl) cates a new thread control block (TCB).Then the current The global pointers(cth,hd,tl,fl)are saved in the mem- machine context is cloned and stored into the TCB with a ory starting from gbl.cth points to the current thread TCB. new thread id.Lastly,the new TCB is marked with ready hd and tl point to the thread queue.fl points to a memory flag and put into the queue.A thread will be running forever if it does not terminate.The role of ctl_exit()is stopping block list,which is used for dynamic heap allocation. the current thread and marking its TCB with dead flag.The QNode(p.c,(pc,R,ts,ow),q）≌(p-2一q,34) ct1_join()function suspends the calling thread until the *(p一o,pc,ts,ow) specified thread terminates.It takes a thread id as argument. *(p+4→(r1),,蓝(r25),(r28)）,(r29),成(r30) 3.3.Certification of CTL Cth(p.c.Tcb)QNode(p.o.Tcb.NULL) SCAP.We use SCAP [8]to certify CTL.SCAP sup- We define the predicate TQ to model the queue for ports modular certification of assembly code with func- threads.TQ has three arguments,the formal queue Q which tion call/return abstraction,making CTL routines well- is isomorphism to the concrete memory data,a queue-head organized.The specification constructs of SCAP and some pointer hd and a queue-tail pointer tl.TOseg models a queue selected SCAP rules are shown in Figure 4.A code spec- segment in the middle of the queue,with a non-null pointer ification OscAP is a pair of two predicates p and g.p is the pointing to the next node.TOseg is defined inductively on precondition,while g is a predicate over the entry state and the structure of Q. the future return state after jr ra.g relates the entry state of a code to the return state of the corresponding procedure.g TOseg(hd,1l,g) can also be treated as a general postcondition parameterized (hd=11)(hd=q) by the entry state. TOseg(~Tcb).hd,tl,q) (hd=1l)A QNode(hd,G,Tcb.q) Specification constructs.Figure 5 describes the specifi- TOseg(Tcb)ua.hd,rl.q) cation constructs of CTL.We use the word value w to spec- 3'.QNode(hd,o,Tcb.q')*TOseg(Q.q,tl.q) ify the thread id o.The state ts of a thread may be ready, TO(Q.hd.tl) dead or wait.A thread control block Tcb consists of a pc,a TOseg(Q.hd,r/,NULL)

(StPred) p ::= State → Prop (GrPred) g ::= State → State → Prop (CdSpec) θSCAP ::= (p,g) ∀ f ∈ dom(Ψ′ ) : Ψ;C ⊢SCAP {Ψ′ (f)}f : C(f) Ψ ⊢SCAP C : Ψ′ (CDHP) ι = jal f′ (p ′ ,g ′ ) = Ψ(f ′ ) (p ′′ ,g ′′) = Ψ(f+1) ∀S. p S → p ′ Sˆ ι ∀S,S ′ . S.pc = f → p S → g ′ Sˆ ι S ′ → p ′′ S ′ ∧(∀S ′′ . g ′′ S ′ S ′′ → g S S′′) ∀S,S ′ .g ′ S S′ → S.R(ra) = S ′ .R(ra) Ψ;C ⊢SCAP {(p,g)}f : jal f′ (CALL) ι = jr ra ∀S.p S → g S Sˆ ι Ψ;C ⊢SCAP {(p,g)}f : jr ra (RET) Figure 4. SCAP The routine ctl_yield() causes the current thread to yield its execution in favor of another thread with certain scheduling policy. ctl_yield() stores the execution con￾text in the queue of the TCBs and picks up one TCB, loads it and switches the control to the new continuation. ctl_yield() adopts the round-robin scheduling algorithm. Thread creation is achieved by using ctl_spawn() with a parameter of start code pointer. This function first allo￾cates a new thread control block (TCB). Then the current machine context is cloned and stored into the TCB with a new thread id. Lastly, the new TCB is marked with ready flag and put into the queue. A thread will be running forever if it does not terminate. The role of ctl_exit() is stopping the current thread and marking its TCB with dead flag. The ctl_join() function suspends the calling thread until the specified thread terminates. It takes a thread id as argument. 3.3. Certification of CTL SCAP. We use SCAP [8] to certify CTL. SCAP sup￾ports modular certification of assembly code with func￾tion call/return abstraction, making CTL routines well￾organized. The specification constructs of SCAP and some selected SCAP rules are shown in Figure 4. A code spec￾ification θSCAP is a pair of two predicates p and g. p is the precondition, while g is a predicate over the entry state and the future return state after jr ra. g relates the entry state of a code to the return state of the corresponding procedure. g can also be treated as a general postcondition parameterized by the entry state. Specification constructs. Figure 5 describes the specifi- cation constructs of CTL. We use the word value w to spec￾ify the thread id σ. The state ts of a thread may be ready, dead or wait . A thread control block Tcb consists of a pc, a (Thread-id) σ ::= w (RegFileX) R˜ ::= R\ {r0 ❀ ,k0 ❀ ,k1 ❀ ,ra ❀ } (TCB) Tcb ::= (pc,R˜ ,ts,σw) (Th State) ts ::= ready | dead | wait (Th Queue) Q ::= {· } | {σ ❀ Tcb} ∪ Q Figure 5. Specification constructs of CTL partial registers file R˜ and a thread state ts. A partial regis￾ters file R˜ is a registers file R excluding r0, k0, k1 and ra. The registers k0 and k1 are preserved for thread scheduling and then unusable in user programs. Because the register r0 always holds the value of zero, it needn’t to be saved. When ra is used to call the routines of CTL, its value is saved in the Tcb.pc field. A thread queue Q is a dictionary mapping σ to Tcb and constructed inductively. Formal core data structures. We formally specify the core data structures that are used in our thread library CTL. As shown in Figure 3, the memory space for CTL is divided into four parts, the global pointer array, the isolated TCB for current thread, the thread queue and the free-block list. Core(σ,Tcb,Q) , ∃gbl .gbl 7→ cth,hd,tl, f l ∗QNode(cth,σ,Tcb,NULL) ∗ TQ(hd,tl,Q) ∗ GoodL(f l) The global pointers (cth,hd,tl, f l) are saved in the mem￾ory starting from gbl. cth points to the current thread TCB. hd and tl point to the thread queue. f l points to a memory block list, which is used for dynamic heap allocation. QNode(p,σ,(pc,R˜ ,ts,σw),q) , (p−2 7→ q,34) ∗(p 7→ σ,pc,ts,σw) ∗(p+4 7→ R˜(r1),...,R˜(r25),R˜(r28),R˜ (r29),R˜(r30)) Cth(p,σ,Tcb) , QNode(p,σ,Tcb,NULL) We define the predicate TQ to model the queue for threads. TQ has three arguments, the formal queue Q which is isomorphism to the concrete memory data, a queue-head pointer hd and a queue-tail pointer tl. TQseg models a queue segment in the middle of the queue, with a non-null pointer pointing to the next node. TQseg is defined inductively on the structure of Q. TQseg( {} ,hd,tl,q) , (hd = tl) ∧ (hd = q) TQseg( {σ ❀ Tcb} ,hd,tl,q) , (hd = tl) ∧ QNode(hd,σ,Tcb,q) TQseg( {σ ❀ Tcb} ∪ Q ,hd,tl,q) , ∃q ′ .QNode(hd,σ,Tcb,q ′ ) ∗ TQseg(Q,q ′ ,tl,q) TQ(Q,hd,tl) , TQseg(Q,hd,tl,NULL)

As defined above,a queue segment consists of several Q.(H Core(_,)Top) nodes modeled by QNode.The routines in the CTL may (R,H,pc) traverse,search,add a TCB node or delete one in the queue, (R',H',pc) .VA,Q,o,Tcb.3o whose structure should be preserved. (H Core(o,Tcb,Q)*A) When a thread is created,the scheduler will allocate a (H Core(Gx:(pc',R',ready,_),O)*A) heap block from the free block list.If a thread is joined by where another one.the scheduler will free its TCB.The definition (pc'R,ready,-)=(QU{(R(ra),R.ready,-)})(c) of free block-list GoodL follows the work by Yu et al.[25] a=(QU{c(R(ra),成，ready,-))八{ox(pc,',ready,-)} and Xiang et al.[23],and it can be ported to our framework directly. ctl_yield()mainly performs context switching.Its precondition py requires that the memory space of CTL should be well-formed,specified by the predicate Core. gy is a condition which specifies the actions performed Implementation of yielding.The yielding routine is used by the whole ctl_yield()routine.We assume that the to schedule threads and perform the context switching.The control flow is transferred to thread ox.whose TCB is code body of the ctl_yield()are presented in Figure 6. Tcb,=(pc,R,ready,-).Then gy specifies the postcondi- The first phase of yielding (from YIELD to APPENDTCB) tions which ctl_yield()must satisfies that:(i)at the exit- consists in loading address of the current TCB to ko,saving ing point of ctl_yield(),the old machine context is added the machine context to the current TCB and loading other into Q;(ii)a ready control block Tcb,which contains the global pointers.The code address of the next instruction of current register file Rx and the code pointer pc,has been the current thread has already been saved in ra.ra has to fetched out of Q;(iii)the memory space of Core is still be saved into TCB firstly,because ra will be used to call well-formed while the irrelevant heap A is unchanged.Ob- SAVECTX viously,the specification of ctl_yield()is independent of The second phase of yielding is appending the current CTL scheduling algorithm.Core is related to the implemen- TCB (by calling APPENDTCB)to the thread queue,search- tation,which should be hidden from user programs. ing for a ready TCB through the queue,and fetching it out By the SCAP rules presented in Figure 4,it can be (by calling FETCHTCB).Since there is at least one ready TCB proved that the yielding routine satisfies these specifica- (consider the one just appended)in the queue,the routine tions. FETCHTCB never fails to return.The algorithm of searching ready thread depends on the scheduling policy.Here the Certification of CTL.The certification of ctl_spawn(), naive FIFO method is used and then the code of searching ctl_exit()and ctl_join()follows this method of certi- is a loop over the thread queue. fying the ctl_yield()routine.We take CcrL as the code The role of the last switch phase(from SWITCH)of yield- heap of CTL and YerL as the code heap specification.By ing is to switch the machine context from the old context the CDHP rule,we have: to the new context fetched by FETCHTCB.Concretely,it sets ko with the address of the new TCB.then makes a tail call PCTL FSCAP CCT:平cT to LOADCTX.Inside LOADCTX,the registers file are restored including ra.The last step is tricky,and when program re- turns,the control flow is transferred to the new thread. 4.CMAP:a concurrent program logic CMAP is a program logic for certifying multithreaded Certification of yielding.Part of the formal specifica- assembly code with unbounded dynamic thread creation tions of ctl_yield()are also presented in Figure 6.Note and termination.It assumes that the register files are that the guarantees in the middle of code body are not listed thread local,i.e.,saving and loading registers during con- because they are unnecessary for the readers to understand text switching.CMAP is based on an abstract machine with the specification,although indispensable to the certification built-in thread operations,e.g.,yield,spawn and exit are process.For the same reason,the initial state (R,H,pc)and treated as atomic primitives.This approach simplify the cer- the final state (R',H',pc'),playing their roles as parameters tification of user programs.However,the operations are not of p and g,are omitted as well. directly supported by most existing hardwares. The specification of ctl_yield()(p,gy)is defined be- In Figure 7,we present a simplified CMAP system, low: which is adapted to our thread model.Notice that the whole

As defined above, a queue segment consists of several nodes modeled by QNode. The routines in the CTL may traverse, search, add a TCB node or delete one in the queue, whose structure should be preserved. When a thread is created, the scheduler will allocate a heap block from the free block list. If a thread is joined by another one, the scheduler will free its TCB. The definition of free block-list GoodL follows the work by Yu et al. [25] and Xiang et al. [23], and it can be ported to our framework directly. Implementation of yielding. The yielding routine is used to schedule threads and perform the context switching. The code body of the ctl_yield() are presented in Figure 6. The first phase of yielding (from YIELD to APPENDTCB) consists in loading address of the current TCB to k0, saving the machine context to the current TCB and loading other global pointers. The code address of the next instruction of the current thread has already been saved in ra. ra has to be saved into TCB firstly, because ra will be used to call SAVECTX. The second phase of yielding is appending the current TCB (by calling APPENDTCB) to the thread queue, search￾ing for a ready TCB through the queue, and fetching it out (by calling FETCHTCB). Since there is at least one ready TCB (consider the one just appended) in the queue, the routine FETCHTCB never fails to return. The algorithm of searching ready thread depends on the scheduling policy. Here the naive FIFO method is used and then the code of searching is a loop over the thread queue. The role of the last switch phase (from SWITCH) of yield￾ing is to switch the machine context from the old context to the new context fetched by FETCHTCB. Concretely, it sets k0 with the address of the new TCB, then makes a tail call to LOADCTX. Inside LOADCTX, the registers file are restored including ra. The last step is tricky, and when program re￾turns, the control flow is transferred to the new thread. Certification of yielding. Part of the formal specifica￾tions of ctl_yield() are also presented in Figure 6. Note that the guarantees in the middle of code body are not listed because they are unnecessary for the readers to understand the specification, although indispensable to the certification process. For the same reason, the initial state (R,H,pc) and the final state (R ′ ,H′ ,pc′ ), playing their roles as parameters of p and g, are omitted as well. The specification of ctl_yield() (py ,gy ) is defined be￾low: py , ∃Q.(H ° Core( , ,Q) ∗ Top) gy , λ · (R,H,pc) (R ′ ,H′ ,pc′ ) ¸ .∀A,Q,σ,Tcb.∃σx . · (H ° Core(σ,Tcb,Q) ∗ A) (H′ ° Core(σx,(pc′ ,R˜ ′ ,ready, ),Q ′ ) ∗ A) ¸ where (pc′ ,R˜ ′ ,ready, ) = (Q ∪ {σ ❀ (R(ra),R,ready, )})(σx) Q ′ = (Q ∪ {σ ❀ (R(ra),R˜ ,ready, )}) \ {σx ❀ (pc′ ,R˜ ′ ,ready, )} ctl_yield() mainly performs context switching. Its precondition py requires that the memory space of CTL should be well-formed, specified by the predicate Core. gy is a condition which specifies the actions performed by the whole ctl_yield() routine. We assume that the control flow is transferred to thread σx, whose TCB is Tcbx = (pcx ,R˜ x,ready, ). Then gy specifies the postcondi￾tions which ctl_yield() must satisfies that: (i) at the exit￾ing point of ctl_yield(), the old machine context is added into Q; (ii) a ready control block Tcbx, which contains the current register file Rx and the code pointer pcx , has been fetched out of Q; (iii) the memory space of Core is still well-formed while the irrelevant heap A is unchanged. Ob￾viously, the specification of ctl_yield() is independent of CTL scheduling algorithm. Core is related to the implemen￾tation, which should be hidden from user programs. By the SCAP rules presented in Figure 4, it can be proved that the yielding routine satisfies these specifica￾tions. Certification of CTL. The certification of ctl_spawn(), ctl_exit() and ctl_join() follows this method of certi￾fying the ctl_yield() routine. We take CCTL as the code heap of CTL and ΨCTL as the code heap specification. By the CDHP rule, we have: ΨCTL ⊢SCAP CCTL : ΨCTL 4. CMAP: a concurrent program logic CMAP is a program logic for certifying multithreaded assembly code with unbounded dynamic thread creation and termination. It assumes that the register files are thread local, i.e., saving and loading registers during con￾text switching. CMAP is based on an abstract machine with built-in thread operations, e.g., yield, spawn and exit are treated as atomic primitives. This approach simplify the cer￾tification of user programs. However, the operations are not directly supported by most existing hardwares. In Figure 7, we present a simplified CMAP system, which is adapted to our thread model. Notice that the whole

{P8)} P,=3p.c,Tcb.R(k0)=p+4AHICth(p,G.Tcb)*True g.=VA.p.c,pcx.tsz.H Cth(p,c,(pcx.-,tsx.-))*A YIELD: lw ko cth ro →R(ra)=R'(ra)A sw ra 1 ko Cth(p,c,(pc.R.ts,))*A sw r0 2 k0 SAVECTX: addiu koko 4 SW r1 0 ko sw r2 1 k0 jal SAVECTX 44▣ p=3Q.gbl,o.Tcb.Tcb.ts=ready A Tcb=(R(ra),R,ready,-)A sw r25 24 k0 Hgblp,hd,tl,_*Cth(p,G,Tcb)*TQ(Q.hd,tl)*True sw r28 25 k0 LOAD: jal LOADPTR p=3Q.gbl.o,Tcb.R(t0,t1,t2)=(p,hd.t/)A sw r30 27 k0 Hgblp.hd,tl,*Cth(p.c,Tcb)TQ(Q.hd,l)*True jr ra APPEND: beq t1 ro SWITCH P:=3p,c.Tcb.R(k0)=p+4 HCth(p,c,Tcb)+True jal APPENDTCB gy=VA.p,G.pc.Rx.H Cth(p.G,Tcb)*A -R'(ra)=Tcb.pc AR'=Tcb.RA p=30.gbl.R(t1.t2)=(hd,tl)A Cth(p,c,Tcb)*A Hgbl一.，--，-*TQ(Q,hd,0*True LOADCTX: 1w r1 0 ko FETCH: jal FETCHTCB lw r2 1 k0 p=3Q.gbl,o.Tcb.R(t0.t1.t2)=(p.hd.rl)A Hgbl一，-，-+-*Cth(p,o,Tcb)*TQ(Q,hd,l)*True 1wr2524k0 SAVE: jal SAVEPTR 1wr2825k0 p=3Q,gbl,c,Tcb. 1Wr3027k0 HIgbl p.hd.tl,_+Cth(p,G,Tcb)+TQ(Q.hd,tl)*True subiu ko ko 3 SWITCH: move ko to lw ra 0 ko addiu ko ko 4 jr ra j LOADCTX APPENDTCB: SAVEPTR: FETCHTCB: LOADPTR: 。 Figure 6.Code and specification of yield(part) system is unchanged except for the primitives of yield, jal yield,when pc points to f.In order to ensure the yield- spawn and exit are replaced with function calls in CTL. ing safety,the premises of YIELD rule are:(i)the precon- The code specification 0cMAP is a quadruple (p,g,A,G). dition and assumption at the address f+1 are the same in The predicate p and the local guarantee g describe the states each thread;(ii)the local guarantee gat the address f+1 is and transitions of the program.When checking concurrent equal to the guarantee G;the state of yielding thread always properties during the interleaving execution,we rely on the satisfies the current precondition if it would satisfy the as- A-G method,in which the assumption A and the gurantee sumption A after any state transition;(iii)the current thread G are used.In one thread,the assumption A gives informa- completes the required state transition specified by the guar- tion of what atomic transitions may be performed by other antee G. threads,while the guarantee G holds on every atomic tran- sition performed by the thread itself.So long as the en- vironment (i.e..the collection of all the rest of the threads) Example.We give an example to explain how to cer- satisfies A,the thread's behavior to the environment will sat- tify user multithreaded programs.The example adapted isfy its G.Furthermore,every thread should be verified to from [7]is a program for unbounded dynamic thread cre- ensure that the guarantee of any other thread satisfies its as- ation as shown in Figure 8.When running,the main thread initialize 100 pieces of data with 0 to 99 respectively,and sumption. By this method we could then certify each thread sep- distributes them to 100 child threads.These child threads arately without worrying about the rest of the threads. add their own data by one in parallel.To ensure the safety That is how we achieve thread-modular reasoning.And if property of the program,each child thread assumes that no all threads satisfy their specifications,the following non- other threads will touch its own working data and guaran- interference property results in correct collaboration be- tees that it will not change other threads'data.The assump- tions and guarantees of the main thread and its child threads. tween threads. defined in Figure 8,reflect these ideas. NI ([(A1.G1.1.R)...(An.G)]) Suppose the example code is Cx and its specification is i≠j.c≠ojAH,.(G:成：HH一A,成，H) ex,we have the safety of the code heap Cex with CMAP Suppose the program will yield its control by executing inference rules

{(py ,gy )} YIELD: lw k0 cth r0 sw ra 1 k0 sw r0 2 k0 addiu k0 k0 4 jal SAVECTX p = ∃Q,gbl,σ,Tcb.Tcb.ts = ready ∧ Tcb = (R(ra),R˜ ,ready, ) ∧ H ° gbl 7→ p,hd,tl, ∗ Cth(p,σ,Tcb) ∗ TQ(Q,hd,tl) ∗ True LOAD: jal LOADPTR p = ∃Q,gbl,σ,Tcb.R(t0,t1,t2) = (p,hd,tl) ∧ H ° gbl 7→ p,hd,tl, ∗ Cth(p,σ,Tcb) ∗ TQ(Q,hd,tl) ∗ True APPEND: beq t1 r0 SWITCH jal APPENDTCB p = ∃Q,gbl .R(t1,t2) = (hd,tl) ∧ H ° gbl 7→ , , , ∗ TQ(Q,hd,tl) ∗ True FETCH: jal FETCHTCB p = ∃Q,gbl,σ,Tcb.R(t0,t1,t2) = (p,hd,tl) ∧ H ° gbl 7→ , , , ∗ Cth(p,σ,Tcb) ∗ TQ(Q,hd,tl) ∗ True SAVE: jal SAVEPTR p = ∃Q,gbl,σ,Tcb. H ° gbl 7→ p,hd,tl, ∗ Cth(p,σ,Tcb) ∗ TQ(Q,hd,tl) ∗ True SWITCH: move k0 t0 addiu k0 k0 4 j LOADCTX APPENDTCB: ... FETCHTCB: ... ps = ∃p,σ,Tcb.R(k0)=p+4 ∧ H ° Cth(p,σ,Tcb) ∗ True gs = ∀A, p,σ,pcx ,tsx .H ° Cth(p,σ,(pcx , ,tsx, )) ∗ A → R(ra) = R ′ (ra) ∧ H ° Cth(p,σ,(pcx ,R˜ ,tsx, )) ∗ A SAVECTX: sw r1 0 k0 sw r2 1 k0 ... sw r25 24 k0 sw r28 25 k0 ... sw r30 27 k0 jr ra pl = ∃p,σ,Tcb.R(k0)=p+4 ∧ H ° Cth(p,σ,Tcb) ∗ True gl = ∀A, p,σ,pcx ,Rx .H ° Cth(p,σ,Tcb) ∗ A → R ′ (ra) = Tcb.pc ∧ R˜ ′ = Tcb.R˜ ∧ H ° Cth(p,σ,Tcb) ∗ A LOADCTX: lw r1 0 k0 lw r2 1 k0 ... lw r25 24 k0 lw r28 25 k0 ... lw r30 27 k0 subiu k0 k0 3 lw ra 0 k0 jr ra SAVEPTR: ... LOADPTR: ... Figure 6. Code and specification of yield(part) system is unchanged except for the primitives of yield, spawn and exit are replaced with function calls in CTL. The code specification θCMAP is a quadruple (p,gˇ,A,G), The predicate p and the local guarantee ˇg describe the states and transitions of the program. When checking concurrent properties during the interleaving execution, we rely on the A-G method, in which the assumption A and the gurantee G are used. In one thread, the assumption A gives informa￾tion of what atomic transitions may be performed by other threads, while the guarantee G holds on every atomic tran￾sition performed by the thread itself. So long as the en￾vironment (i.e., the collection of all the rest of the threads) satisfies A, the thread’s behavior to the environment will sat￾isfy its G. Furthermore, every thread should be verified to ensure that the guarantee of any other thread satisfies its as￾sumption. By this method we could then certify each thread sep￾arately without worrying about the rest of the threads. That is how we achieve thread-modular reasoning. And if all threads satisfy their specifications, the following non￾interference property results in correct collaboration be￾tween threads. NI ([(A1,G1,σ1,R˜ 1),...,(An,Gn,σn,R˜ n)]) , ∀i 6= j.σi 6= σj ∧ ∀H,H′ .(Gi R˜ i H H′ → Aj R˜ j H H′ ) Suppose the program will yield its control by executing jal yield, when pc points to f. In order to ensure the yield￾ing safety, the premises of YIELD rule are: (i) the precon￾dition and assumption at the address f+1 are the same in each thread; (ii) the local guarantee gˇ at the address f+1 is equal to the guarantee G; the state of yielding thread always satisfies the current precondition if it would satisfy the as￾sumption A after any state transition; (iii) the current thread completes the required state transition specified by the guar￾antee G. Example. We give an example to explain how to cer￾tify user multithreaded programs. The example adapted from [7] is a program for unbounded dynamic thread cre￾ation as shown in Figure 8. When running, the main thread initialize 100 pieces of data with 0 to 99 respectively, and distributes them to 100 child threads. These child threads add their own data by one in parallel. To ensure the safety property of the program, each child thread assumes that no other threads will touch its own working data and guaran￾tees that it will not change other threads’ data. The assump￾tions and guarantees of the main thread and its child threads, defined in Figure 8, reflect these ideas. Suppose the example code is CEX and its specification is ΨEX, we have the safety of the code heap CEX with CMAP inference rules

(StPred) =RegFileX→Heap→Prop MAIN: (True,A1.GI) A1≌i.0≤i[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 [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

V:= Specification Constructs P Well-formed program (CdSpec）e:=6seAr|θcAe grC:Ψ(aΨS)Ca)pe:Cpd(PRoa) (CHSpec）Ψ：={fo}* Ψk(C,S,pc) (Assert)a∈CHSpec→State→Prop (nep)【-】∈CdSpec一Assert C:Well-formed code heap for all f∈dom(Ψ)：a=(Ψ'(E)I)wc卜{ai:C(E) [0scx SCAP Interpretation (CDHP) Ψ卜C:Ψ I(p,g)]≌入Ψ，Sp3A3n.WFST(m,S,） Ca:Well-formed instruction sequence wFST(0,q,)≌S.qS 一→3 0CMAP.(S.R(ra)=0 CMAP A 0CMAP]YS a→入Ψ.S.S.pc=f WFST(n+1,q,≌3.g8 →38.Ψ(E=6ΛI61Ψ8a1f -(JAL) 一p,g.ΨR(ra)=(p,g) CH(alf:jalf' Ap'S'A WFST(n,gS,Ψ) 10CMAP】≌ a→Ψ，S38ΨSR,》=6N]Ψ8：上UR CMAP Interpretation CHalf:jrrs I(p,总，A,G)1≌入平，(RH,pc).3H1,H2,c,Q Efaddu,addiu,subu,subiu.move,li.Iw,sw} H=H,出H2ApRH1 a→入Ψ，S.(f+1∈dom( A HCore(o,Tcb,Q) A WFTQ(Ψ，Q,(危成H1),A,Go,) →8.Ψ(E+1)-6AI61ΨS) A(E+1主dom( WFTQ(Q.q.A.G.o,R) →3a'.aΨS∧(Ck{af+1:C(f+1)) d,pc,'.Q(o)=(pc,,-) (SEO) CHfa)f:1 一p,A',c.Ψpc)=(p,c,A',c) where ANI([(A.G.R)(A'.G').) AR,H,H.p'成H→A'成HH→p京H) (agΨ，s.ΨΨΛaΨs A(H.gH一pR'H) a÷a' Ψ，S.aΨs→aΨs Figure 9.OCAP-light call,while the return action is performed by jr ra.The in- describes the well-formedness of the thread queue.Upon variant of the abstract control stack is captured by the pred- a well-formed thread queue,the thread library can run the icate (WFST),which tells us what is a well-form abstract scheduling routine safely.The well-formedness of thread control stack.Certainly,a safe function call jal won't break queue is specified by the following invariants: the well-formedness of the abstract control stack. We define the interpretation function of SCAP accord- each Tcb in the thread queue contains a valid code ing to these intuitive ideas in Figure 9.Through the inter- pointer with code specification(p.A,G): pretation function,we can build SCAP instruction rules as assumptions and guarantees of all the threads are non- lemmas in OCAP-light.With these lemmas,safety proof interference; can be constructed directly at OCAP-light level,while still reasoning at the SCAP level.Furthermore,we can prove the precondiction of a waiting thread still holds af- the soundness of SCAP semantically by this interpretation ter any state transitions satisfying the assumption,i.e., function. 成，H,Hp成H一A成H→p成H': Theorem 2(SCAP-Soundness). If平HSCAP C:Ψ，then平LC:平. when calling the routines in CTL,the state satisfies preconditions of all the waiting thread. 5.3.Embedding CMAP in OCAP-light Next,we prove the soundness theorem of CMAP to com- plete the embedding process.Firstly,we prove that the pro- Like SCAP,an interpretation function of CMAP is also grams certified by CMAP logic system call the yield routine defined in Figure 9.Through the interpretation function,we of CTL safely.Informally,the safety proof of ctl_yield() know that the whole data heap H is separated into two parts, is divided into two subgoals.One subgoal is to prove that H and H2.H is for user programs,while H2 is for thread the well-formed state before yielding satisfies the precon- library CTL.R is a registers file excluding the registers ro, dition of ctl_yield()p.The alternative is to prove that ko,k1 and ra.The remainder of the interpretation function the state after the program returns from ctl_yield()is still is a complicated predicate WFTQ.Similar to WFST,WFTQ well-formed.The difficulties of proving this subgoal come

V ::= Specification Constructs (CdSpec) θ ::= θSCAP | θCMAP (CHSpec) Ψ ::= {f ❀ θ} ∗ (Assert) a ∈ CHSpec → State → Prop (Interp) [[ ]] ∈ CdSpec → Assert [[θSCAP ]] , SCAP Interpretation [[(p,g)]] , λΨ,S.p S ∧ ∃n.WFST(n, gˇ S,Ψ) WFST(0,q,Ψ) , ∀S ′ .q S ′ → ∃θCMAP .Ψ(S ′ .R(ra)) = θCMAP ∧ [[θCMAP ]] Ψ S WFST(n+1,q,Ψ) , ∀S ′ .q S ′ → ∃p ′ ,g ′ .Ψ(S ′ .R(ra)) = (p ′ ,g ′ ) ∧ p ′ S ′ ∧ WFST(n,g ′ S ′ ,Ψ) [[θCMAP ]] , CMAP Interpretation [[(p,gˇ,A,G)]] , λΨ,(R,H,pc).∃H1,H2,σ,Q. H = H1 ⊎H2 ∧ p R H˜ 1 ∧ H2 ° Core(σ,Tcb,Q) ∧ WFTQ(Ψ,Q,(gˇ R H˜ 1),A,G,σ,R˜) WFTQ(Q,q,A,G,σ,R˜ ) , ∀σ ′ ,pc′ ,R˜ ′ .Q(σ ′ ) = (pc′ ,R˜ ′ , ) → ∃p ′ ,A ′ ,G ′ .Ψ(pc′ ) = (p ′ ,G ′ ,A ′ ,G ′ ) ∧ NI ([(A,G,σ,R˜),...,(A ′ ,G ′ ,σ ′ ,R˜ ′ ),...]) ∧ (∀R˜ ,H,H′ .p ′ R H˜ → A ′ R H H ˜ ′ → p ′ R H˜ ′ ) ∧ (∀H.q H → p ′ R˜ ′ H) Ψ ⊢ P Well-formed program Ψ ⊢ C:Ψ (a Ψ S) C ⊢ {a}pc : C(pc) Ψ ⊢ (C,S,pc) (PROG) Ψ ⊢ C:Ψ′ Well-formed code heap for all f ∈ dom(Ψ′ ): a = h[[Ψ′ (f)]]iΨ C ⊢ {a}f : C(f) Ψ ⊢ C:Ψ′ (CDHP) C ⊢ {a}f : ι Well-formed instruction sequence a ⇒ λΨ,S.S.pc = f → ∃θ ′ .Ψ(f ′ ) = θ ′ ∧ [[θ ′ ]] Ψ Sˆ jal f ′ C ⊢ {a}f : jal f′ (JAL) a ⇒ λΨ,S. ∃θ ′ .Ψ(S.R(rs)) = θ ∧ [[θ]] Ψ Sˆ jr rs C ⊢ {a}f : jr rs (JR) ι∈{addu,addiu,subu,subiu,move,li,lw,sw} a ⇒ λΨ,S.(f+1 ∈ dom(Ψ) → ∃θ ′ .Ψ(f+1) = θ ′ ∧ [[θ ′ ]] Ψ Sˆ ι) ∧ (f+1 6∈ dom(Ψ) → ∃a ′ .a ′ Ψ Sˆ ι ∧ (C ⊢ {a ′}f+1 : C(f+1))) C ⊢ {a}f : ι (SEQ) where haiΨ , λΨ,S.Ψ ⊆ Ψ′ ∧ a Ψ′ S a ⇒ a ′ , λΨ,S.a Ψ S ⇒ a ′ Ψ S Figure 9. OCAP-light call, while the return action is performed by jr ra. The in￾variant of the abstract control stack is captured by the pred￾icate (WFST), which tells us what is a well-form abstract control stack. Certainly, a safe function call jal won’t break the well-formedness of the abstract control stack. We define the interpretation function of SCAP accord￾ing to these intuitive ideas in Figure 9. Through the inter￾pretation function, we can build SCAP instruction rules as lemmas in OCAP-light. With these lemmas, safety proof can be constructed directly at OCAP-light level, while still reasoning at the SCAP level. Furthermore, we can prove the soundness of SCAP semantically by this interpretation function. Theorem 2 (SCAP - Soundness). If Ψ ⊢SCAP C : Ψ′ , then Ψ ⊢ C : Ψ′ . 5.3. Embedding CMAP in OCAP-light Like SCAP, an interpretation function of CMAP is also defined in Figure 9. Through the interpretation function, we know that the whole data heap H is separated into two parts, H1 and H2. H1 is for user programs, while H2 is for thread library CTL. R˜ is a registers file excluding the registers r0, k0, k1 and ra. The remainder of the interpretation function is a complicated predicate WFTQ. Similar to WFST, WFTQ describes the well-formedness of the thread queue. Upon a well-formed thread queue, the thread library can run the scheduling routine safely. The well-formedness of thread queue is specified by the following invariants: • each Tcb in the thread queue contains a valid code pointer with code specification (p,gˇ,A,G); • assumptions and guarantees of all the threads are non￾interference; • the precondiction of a waiting thread still holds af￾ter any state transitions satisfying the assumption, i.e., ∀R˜ ,H,H′ .p R H˜ → A R H H ˜ ′ → p R H˜ ′ ; • when calling the routines in CTL, the state satisfies preconditions of all the waiting thread. Next, we prove the soundness theorem of CMAP to com￾plete the embedding process. Firstly, we prove that the pro￾grams certified by CMAP logic system call the yield routine of CTL safely. Informally, the safety proof of ctl_yield() is divided into two subgoals. One subgoal is to prove that the well-formed state before yielding satisfies the precon￾dition of ctl_yield() py . The alternative is to prove that the state after the program returns from ctl_yield() is still well-formed. The difficulties of proving this subgoal come

from the indeterminable transfer of control flow.Fortu- CTL is well-formed in OCAP-.light平nF CenL.:平cm·On nately,we could solve these difficulties by knowing that the the other hand,from Section 4,the unbounded thread cre- thread queue satisfies WFTQ.The following lemma speci- ation is well-formed in CMAP,xCMA Cx:Ex.Hence fies the safety of ctl_yield(). by Theorem 3,the example is well-formed in OCAP-light Lemma 1 (Yielding-Safety). 平exu平cIL F CEx:平ex.Finally,CTL and the example are If平：C HCMAP{(p,g,A,G)}f:jal yield,Ψ(f+1)=(p,G,A,G) all well-formed at OCAP-light level.By the CDHP rule of then(Ip,g,A,G)平→(py,g)I》g OCAP-light,we can link CEx with our thread library CerL and have the conclusion that: By the JAL rule presented in Figure 9 and Lemma 1,we can prove the CMAP JAL rule presented in Figure 7 as lem- 平ExU平cT上CEx UCEX:ΨExUΨcT mas at OCAP-light level. Lemma 2 (Yielding-OCAP-light). From this,a complete multithreaded FPCC package can If平：C FCMAP{BCMAP}f:jal yield,.then: be constructed by the PROG rule of OCAP-light easily. YUfyield(Py,g)):C{0CMAP ])f jal yield Following the same pattern of ctl_yield(),we can 6.Related work and conclusion prove that all the routines are safe to call by the user pro- grams.Then,we can have the soundness theorem of CMAP Thread library.Ni et al.have certified a thread library by the CDHP rule in Figure 9 immediately. named Mth [18].whose aim is quite different from our Theorem 3(CMAP-Soundness). CTL,they use a machine model that is a strict subset of x86 If平FCMAP C:平，then平U平cm上C:Ψ to ensure that their certified code is runnable on real CPU without any changes,while we concentrate on the simplic- ity to link our CTL to other certification frameworks with Discussion.Benefiting from the underlying OCAP-light, ease,we take an abstract machine model as our platform. we have bridged the two different program logics,CMAP But still,our code is MIPS-32 compatible.Mth may be ca- and SCAP.It is possible to embed other concurrent program pable of linking to programs certified in other logics,but the logics in OCAP-light with the same method presented in linking has not been done yet.The program logic employed this section.The essential step is to define a corresponding by Ni is a variant of XCAP [17],which makes intensive interpretation function,which expresses the global invari- use of general embedded code pointer to support modular ants of the program logic in another point of view.In the reasoning,and results in larger proof size. original paper [7],the soundness of CMAP is proved by PROG and DTHRDS rules,which is similar to our interpreta- tion function of CMAP actually-all of them do the same FPCC framework.Our work is based on the OCAP job checking whether the thread queue is well-formed.The framework proposed by Feng et al.[6].In the original two rule express the global invariants of the CMAP logic. OCAP paper,an example was shown to bridge a naive yield- As observed,the linkage does not increase the cost of ing routine to the CCAP logic.Compared to our CTL,the proof construction of user program.The safety proof of concurrency model of CCAP is rather simple.For exam- linkage is hidden from the programmer writing and certify- ple.their model lacks machine context switching and thread ing multithreaded applications. management.Our CTL is a big extension to their work,and The thread queue in the original CMAP is abstract and well illustrates the expressiveness and openness of OCAP. similar to our Q,while the interpretation function in our Chang et al.proposed an open verifier for verifying un- framework interprets the abstract queue Q into the concrete trusted code [2].Their framework produces foundational one in real TM memory.Between the concrete queue of verifiers using untrusted extensions to customize the safety CTL and the abstract one of the CMAP logic,there is a enforcement mechanism.However,it is unclear whether one-to-one map which makes the bridging possible. their extensions support concurrent verification. We believe that CTL can be linked with other concurrent certification logics,such as AGL,CSL,etc.Because their Concurrency verification.SAGL [5]and concurrent thread model is similar to ours,they can also be embedded separation logic(CSL)[19]improve the modularity of A-G in OCAP-light by the similar techniques we used. reasoning method and make the definition of assumptions and guarantees easier.In their machine models.the hold- 5.4.Example ing and releasing of locks are primitive operations.So it would be safe to link the programs certified in SAGL or In Section 3.3,we have proved that CTL is well-formed CSL framework with our library just like linking CMAP in SCAP,Yen.HsCAP Cen:Yen.By Theorem 2,we have programs,as long as embedded in OCAP

from the indeterminable transfer of control flow. Fortu￾nately, we could solve these difficulties by knowing that the thread queue satisfies WFTQ. The following lemma speci- fies the safety of ctl_yield(). Lemma 1 (Yielding - Safety). If Ψ;C ⊢CMAP {(p,gˇ,A,G)}f :jal yield, Ψ(f+1) = (p,G,A,G) then h[[(p,gˇ,A,G)]]iΨ ⇒ h[[(py ,gy )]]iΨ By the JAL rule presented in Figure 9 and Lemma 1, we can prove the CMAP JAL rule presented in Figure 7 as lem￾mas at OCAP-light level. Lemma 2 (Yielding - OCAP-light). If Ψ;C ⊢CMAP {θCMAP}f :jal yield, then: Ψ ∪ {yield ❀ (py ,gy )};C ⊢ {[[θCMAP ]]}f : jal yield Following the same pattern of ctl_yield(), we can prove that all the routines are safe to call by the user pro￾grams. Then, we can have the soundness theorem of CMAP by the CDHP rule in Figure 9 immediately. Theorem 3 (CMAP - Soundness). If Ψ ⊢CMAP C : Ψ, then Ψ ∪ ΨCTL ⊢ C : Ψ . Discussion. Benefiting from the underlying OCAP-light, we have bridged the two different program logics, CMAP and SCAP. It is possible to embed other concurrent program logics in OCAP-light with the same method presented in this section. The essential step is to define a corresponding interpretation function, which expresses the global invari￾ants of the program logic in another point of view. In the original paper [7], the soundness of CMAP is proved by PROG and DTHRDS rules, which is similar to our interpreta￾tion function of CMAP actually — all of them do the same job checking whether the thread queue is well-formed. The two rule express the global invariants of the CMAP logic. As observed, the linkage does not increase the cost of proof construction of user program. The safety proof of linkage is hidden from the programmer writing and certify￾ing multithreaded applications. The thread queue in the original CMAP is abstract and similar to our Q, while the interpretation function in our framework interprets the abstract queue Q into the concrete one in real TM memory. Between the concrete queue of CTL and the abstract one of the CMAP logic, there is a one-to-one map which makes the bridging possible. We believe that CTL can be linked with other concurrent certification logics, such as AGL, CSL, etc. Because their thread model is similar to ours, they can also be embedded in OCAP-light by the similar techniques we used. 5.4. Example In Section 3.3, we have proved that CTL is well-formed in SCAP, ΨCTL ⊢SCAP CCTL : ΨCTL. By Theorem 2, we have CTL is well-formed in OCAP-light ΨCTL ⊢ CCTL : ΨCTL. On the other hand, from Section 4, the unbounded thread cre￾ation is well-formed in CMAP, ΨEX ⊢CMAP CEX : ΨEX. Hence by Theorem 3, the example is well-formed in OCAP-light ΨEX ∪ ΨCTL ⊢ CEX : ΨEX. Finally, CTL and the example are all well-formed at OCAP-light level. By the CDHP rule of OCAP-light, we can link CEX with our thread library CCTL and have the conclusion that: ΨEX ∪ ΨCTL ⊢ CEX ∪ CEX : ΨEX ∪ ΨCTL From this, a complete multithreaded FPCC package can be constructed by the PROG rule of OCAP-light easily. 6. Related work and conclusion Thread library. Ni et al. have certified a thread library named Mth [18], whose aim is quite different from our CTL, they use a machine model that is a strict subset of x86 to ensure that their certified code is runnable on real CPU without any changes, while we concentrate on the simplic￾ity to link our CTL to other certification frameworks with ease, we take an abstract machine model as our platform. But still, our code is MIPS-32 compatible. Mth may be ca￾pable of linking to programs certified in other logics, but the linking has not been done yet. The program logic employed by Ni is a variant of XCAP [17], which makes intensive use of general embedded code pointer to support modular reasoning, and results in larger proof size. FPCC framework. Our work is based on the OCAP framework proposed by Feng et al. [6]. In the original OCAP paper, an example was shown to bridge a naive yield￾ing routine to the CCAP logic. Compared to our CTL, the concurrency model of CCAP is rather simple. For exam￾ple, their model lacks machine context switching and thread management. Our CTL is a big extension to their work, and well illustrates the expressiveness and openness of OCAP. Chang et al. proposed an open verifier for verifying un￾trusted code [2]. Their framework produces foundational verifiers using untrusted extensions to customize the safety enforcement mechanism. However, it is unclear whether their extensions support concurrent verification. Concurrency verification. SAGL [5] and concurrent separation logic (CSL) [19] improve the modularity of A-G reasoning method and make the definition of assumptions and guarantees easier. In their machine models, the hold￾ing and releasing of locks are primitive operations. So it would be safe to link the programs certified in SAGL or CSL framework with our library just like linking CMAP programs, as long as embedded in OCAP

Conclusion.We introduce in this paper the design,inter- [8]X.Feng.Z.Shao.A.Vaynberg.S.Xiang.and Z.Ni.Mod- faces and implementation of a certified thread library,which ular verification of assembly code with stack-based control is implemented at assembly level and strictly proved.Dy- abstractions.In Proc.2006 ACM Conf.on Prog.Lang.De- namic thread management,thread scheduling and synchro- sign and Impl..June 2006. [9]C.Flanagan and S.Qadeer.Thread modular model check- nization mechanics are also covered.what is more.the mod. ing.In Proc.of the SPIN Workshop on Software Verification. ularity of the library endows it with high scalability. 2003. In the open framework OCAP,we show that the thread [10]C.Flanangan,S.N.Freund,and S.Qadeer.Thread- library can be linked to safe user programs certified in the modular verification for shared-memory programs.In Proc. concurrent certification logic CMAP to form complete mul- ES0P'02.pages262-277,2002. tithreaded FPCC packages. [11]Y.Guo,X.Jiang,Y.Chen,and C.Lin.A certified thread Our long-term goals include the building of a mature library for multithreaded user programs.http://ssg. thread library with applicative perspectives,as well as the ustcsz.edu.cn/~guoyu/thlib/,Jan.2007. [12]N.A.Hamid,Z.Shao,V.Trifonov.S.Monnier.and Z.Ni.A certification of a tiny operating system kernel,whose con- syntactic approach to foundational proof-carrying code.In currency model resembles CTL. Proc.LICS'02,pages 89-100,July 2002. [13]C.Jones.Tentative steps toward a development method for Acknowledgments interfering programs.In ACM Trans.on Programming Lan- guages and Systems,pages 596-619.1983. [14]L.Lamport.The temporal logic of actions.ACM Transac- We would like to thank Zhong Shao and Xinyu Feng tions on Programming Languages and Systems,16(3),May for their many inspirational suggestions and comments on 1994. ealier drafts of this paper.We would also like to thank [15]MIPS Technologies,Inc.MIPS32TM Architecture For Pro- Zhaozhong Ni and Hai Fang for help using Coq.Cheng Liu, grammers Volume II:The MIPS32TM Instruction Set,v2.50 [16]F.Mueller.A library implementation of POSIX threads un- Yan Guo,Wei Hu and the anonymous reviewers provided der unix.In Proc.of 1993 USEMIX Technical Conf.and many useful suggestions of areas where the paper could be Exhib.,pages 29-41.San Diego.CA.USA.Jan.1993. improved. [17]Z.Ni and Z.Shao.Certified assembly programming with This work is supported by the National Natural Science embedded code pointers.In Proc.33nd ACM Symposium on Foundation of China under Grant No.60673126.Any opin- Principles of Programming Languages,pages 320-333.Jan. ions,findings,and conclusions contained in this document 2006. [18]Z.Ni.D.Yu,and Z.Shao.Technical report for modular are those of the authors and do not reflect the views of this verification of machine level thread implementation.http: agency. //flint.cs.yale.edu/publications/mth.html,Nov. 2006. References [19]P.W.O'Hearn.Resources,concurrency and local reasoning. In Proc.CONCUR'04.pages 49-67.2004. [20]D.A.Patterson and J.L.Hennessy.Computer Organiza- [1]A.W.Appel.Foundational proof-carrying code.In Proc. tion and Design:The Hardware/Software Interface,chapter 16th Annual IEEE Symposium on Logic in Computer Sci- Appendix A:Assemblers,Linkers,and the SPIM Simulator. ence,pages 247-258,June 2001. Morgan Kaufmann,Aug.2004. [2]B.-Y.Chang,A.Chlipala,G.Necula,and R.Schneck.The [21]C.Paulin-Mohring.Inductive definitions in the system open verifier framework for foundational verifiers.In Proc. Coq-rules and properties.In Proc.TLCA.volume 664 of TLD/'05,pages 1-12,Jan.2005. LNCS.Springer-Verlag,1993. [3]Coq Development Team,INRIA.The Coq proof assistant [22]J.Reynolds.Separation logic:a logic for shared mutable reference manual.Cog release v8.0.Oct.2005 data structures.In Proc.17th IEEE Symposium on Logic in [4]R.S.Engelschall.GNU Pth-the GNU portable threads Computer Science,2002 http://www.gnu.org/software/pth/,1999-2003. [23]S.Xiang,Y.Chen,C.Lin,and L.Li.Molularly certified dy- [5]X.Feng.R.Ferreira,and Z.Shao.On the relationship namic storage allocation in scap.In Proc.6th International between concurrent separation logic and assume-guarantee Conference on Quality Software (QSIC'06),pages 321-328. reasoning.In Proc.ESOP'07,pages 173-188,Braga,Por- IEEE CS press,Oct.2006. tugal,Mar.2007.Springer-Verlag. [24]Q.Xu,W.P.de Roever,and J.He.The rely-guarantee [6]X.Feng,Z.Ni,Z.Shao,and Y.Guo.An open framework to method for verifying shared variable concurrent programs. foundational proof-carrying code.In Proc.2007 ACM S/G- Formal Aspects of Computing,9(2):149-174.1997. [25]D.Yu,N.A.Hamid,and Z.Shao.Building certified libraries PLAN International Workshop on Types in Language Design for PCC:Dynamic storage allocation.Science of Computer and Implementation,Jan.2007. Programming,50(1-3):101-127,Mar.2004. [7]X.Feng and Z.Shao.Modular verification of concurrent [26]D.Yu andZ.Shao.Verification of safety properties for con- assembly code with dynamic thread creation and termina- current assembly code.In Proc.ICFP'04,pages 175-188. tion.In Proc.2005 International Conference on Functional September 2004. Programming (ICFP'04),September 2005

Conclusion. We introduce in this paper the design, inter￾faces and implementation of a certified thread library, which is implemented at assembly level and strictly proved. Dy￾namic thread management, thread scheduling and synchro￾nization mechanics are also covered, what is more, the mod￾ularity of the library endows it with high scalability. In the open framework OCAP, we show that the thread library can be linked to safe user programs certified in the concurrent certification logic CMAP to form complete mul￾tithreaded FPCC packages. Our long-term goals include the building of a mature thread library with applicative perspectives, as well as the certification of a tiny operating system kernel, whose con￾currency model resembles CTL. Acknowledgments We would like to thank Zhong Shao and Xinyu Feng for their many inspirational suggestions and comments on ealier drafts of this paper. We would also like to thank Zhaozhong Ni and Hai Fang for help using Coq. Cheng Liu, Yan Guo, Wei Hu and the anonymous reviewers provided many useful suggestions of areas where the paper could be improved. This work is supported by the National Natural Science Foundation of China under Grant No. 60673126. Any opin￾ions, findings, and conclusions contained in this document are those of the authors and do not reflect the views of this agency. References [1] A. W. Appel. Foundational proof-carrying code. In Proc. 16th Annual IEEE Symposium on Logic in Computer Sci￾ence, pages 247–258, June 2001. [2] B.-Y. Chang, A. Chlipala, G. Necula, and R. Schneck. The open verifier framework for foundational verifiers. In Proc. TLDI’05, pages 1–12, Jan. 2005. [3] Coq Development Team, INRIA. The Coq proof assistant reference manual. Coq release v8.0, Oct. 2005. [4] R. S. Engelschall. GNU Pth - the GNU portable threads. http://www.gnu.org/software/pth/, 1999-2003. [5] X. Feng, R. Ferreira, and Z. Shao. On the relationship between concurrent separation logic and assume-guarantee reasoning. In Proc. ESOP’07, pages 173–188, Braga, Por￾tugal, Mar. 2007. Springer-Verlag. [6] X. Feng, Z. Ni, Z. Shao, and Y. Guo. An open framework to foundational proof-carrying code. In Proc. 2007 ACM SIG￾PLAN International Workshop on Types in Language Design and Implementation, Jan. 2007. [7] X. Feng and Z. Shao. Modular verification of concurrent assembly code with dynamic thread creation and termina￾tion. In Proc. 2005 International Conference on Functional Programming (ICFP’04), September 2005. [8] X. Feng, Z. Shao, A. Vaynberg, S. Xiang, and Z. Ni. Mod￾ular verification of assembly code with stack-based control abstractions. In Proc. 2006 ACM Conf. on Prog. Lang. De￾sign and Impl., June 2006. [9] C. Flanagan and S. Qadeer. Thread modular model check￾ing. In Proc. of the SPIN Workshop on Software Verification, 2003. [10] C. Flanangan, S. N. Freund, and S. Qadeer. Thread￾modular verification for shared-memory programs. In Proc. ESOP’02, pages 262–277, 2002. [11] Y. Guo, X. Jiang, Y. Chen, and C. Lin. A certified thread library for multithreaded user programs. http://ssg. ustcsz.edu.cn/∼guoyu/thlib/, Jan. 2007. [12] N. A. Hamid, Z. Shao, V. Trifonov, S. Monnier, and Z. Ni. A syntactic approach to foundational proof-carrying code. In Proc. LICS’02, pages 89–100, July 2002. [13] C. Jones. Tentative steps toward a development method for interfering programs. In ACM Trans. on Programming Lan￾guages and Systems, pages 596–619, 1983. [14] L. Lamport. The temporal logic of actions. ACM Transac￾tions on Programming Languages and Systems, 16(3), May 1994. [15] MIPS Technologies, Inc. MIPS32TM Architecture For Pro￾grammers Volume II: The MIPS32TM Instruction Set, v2.50. [16] F. Mueller. A library implementation of POSIX threads un￾der unix. In Proc. of 1993 USEMIX Technical Conf. and Exhib., pages 29–41, San Diego, CA, USA, Jan. 1993. [17] Z. Ni and Z. Shao. Certified assembly programming with embedded code pointers. In Proc. 33nd ACM Symposium on Principles of Programming Languages, pages 320–333, Jan. 2006. [18] Z. Ni, D. Yu, and Z. Shao. Technical report for modular verification of machine level thread implementation. http: //flint.cs.yale.edu/publications/mth.html, Nov. 2006. [19] P. W. O’Hearn. Resources, concurrency and local reasoning. In Proc. CONCUR’04, pages 49–67, 2004. [20] D. A. Patterson and J. L. Hennessy. Computer Organiza￾tion and Design: The Hardware/Software Interface, chapter Appendix A: Assemblers, Linkers, and the SPIM Simulator. Morgan Kaufmann, Aug. 2004. [21] C. Paulin-Mohring. Inductive definitions in the system Coq—rules and properties. In Proc. TLCA, volume 664 of LNCS. Springer-Verlag, 1993. [22] J. Reynolds. Separation logic: a logic for shared mutable data structures. In Proc. 17th IEEE Symposium on Logic in Computer Science, 2002. [23] S. Xiang, Y. Chen, C. Lin, and L. Li. Molularly certified dy￾namic storage allocation in scap. In Proc. 6th International Conference on Quality Software (QSIC’06), pages 321–328. IEEE CS press, Oct. 2006. [24] Q. Xu, W. P. de Roever, and J. He. The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing, 9(2):149–174, 1997. [25] 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, Mar. 2004. [26] D. Yu and Z. Shao. Verification of safety properties for con￾current assembly code. In Proc. ICFP’04, pages 175–188, September 2004