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