{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