(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)