118 J.Comput.Sci.Technol.,Jan.2009,Vol.24,No.1 Usually,high-level languages use a programming structure atomicf...}to identify a transaction.Such a InuH≌3t1,2,tg,t4.HIFul1一U1*Empty一2* transaction structure denies the flexibility of construct- In一v3*0ut一U4 ing a transaction,where branches may lead to different A v1 TRUE-2 FALSE components of a same start of a transaction,as shown AU2=TRUE→U1=FALSE in Fig.7.For the same philosopher thread,an auxil- A v3 BFSIZE A v4 BFSIZE iary variable is needed to record the picking attempts L.start: -[pc L.start inside the transaction and used to decide whether to starttrans try for forks again before eating.Fig.9 presents the lw rfull Full zero code fragment using an auxiliary variable for the atomic addiu rtrue zero TRUE bne rfull rtrue Laddin block.We can see that the assembly-level abstraction j L_commit does provide certain convenience. Laddin: -{B.pc =L_start A Hu l emp A了，2,3，v4.Hs IF Fu11一1* while (TRUE){ Empty一2*In→3*0ut一v4 picked FALSE; A U3 BFSIZE A v4 BFSIZE atomicf A R(rtrue)=TRUE Av1 TRUE} if (fork1){ lw rin In zero fork fork2 =1; addiu rin rin 1 picked TRUE: addiu rtemp zero BFSIZE } beq rin rtemp L.subR jLfcheck if (picked)continue; Lfcheck: /eat sw rin In zero lw rout Out zero beq rin rout Lfset jL-setemp Fig.9.Auxiliary variable in atomic block. L_setemp: -{B.pc L.start A31,2,3,U4.Hs I-Fu11一1* 4.2 Producer-Consumer Algorithm Empty一2*In一3*0ut一v4 A v3 BFSIZE A v4 BFSIZE Fig.10 presents the code for the producer-consumer ∧(U1≠TRUE A H In一ts) algorithm where producers keep putting goods into the V(v1=TRUE A Hw I-Ful1→U1*In-v3)} addiu remp zero FALSE Variables: Invariant: sw remp Empty zero bool Full,Empty; ！(Ful1 A Empty) j L_commit int In,Out; 0≤In,Out<BFSIZE L_commit: -[B.pc=L.start A 3 v1:U3;04.Hs IF Fullv1* Producer: Consumer: Empty一FALSE*In一3*Out一v4 while (TRUE){ while (TRUE){ A U3 BFSIZE A v4 BFSIZE starttrans; starttrans; ∧(U1≠TRUE if (Full) if (Empty) AH Empty一FALSE*In一g) V(v1 TRUE In++; 0ut++; ∧(He I Ful1一U1*Empty→FALSE if (In ==BFSIZE) if (Out -BFSIZE) In→3 V H I-emp)} In BFSIZE; Out -BFSIZE; commit if (In =Out) if (Out =In) jL-start Full TRUE; Empty TRUE; L_subR: Empty FALSE; Full FALSE; subu rin rin rtemp } } jL.fcheck commit; commit; L fset: } sw rtrue Full zero j L.setemp Fig.10.Producer-consumer. Fig.11.Producer-consumer in our system.118 J. Comput. Sci. & Technol., Jan. 2009, Vol.24, No.1 Usually, high-level languages use a programming structure atomic{. . . } to identify a transaction. Such a transaction structure denies the flexibility of construct￾ing a transaction, where branches may lead to different components of a same start of a transaction, as shown in Fig.7. For the same philosopher thread, an auxil￾iary variable is needed to record the picking attempts inside the transaction and used to decide whether to try for forks again before eating. Fig.9 presents the code fragment using an auxiliary variable for the atomic block. We can see that the assembly-level abstraction does provide certain convenience. while (TRUE) { picked = FALSE; atomic{ if (! fork1){ fork1 = fork2 = 1; picked = TRUE; } } if (! picked) continue; // eat . . . Fig.9. Auxiliary variable in atomic block. 4.2 Producer-Consumer Algorithm Fig.10 presents the code for the producer-consumer algorithm where producers keep putting goods into the Variables: Invariant: bool Full, Empty; ! (Full ∧ Empty) int In, Out; 0 6 In, Out < BFSIZE Producer : Consumer : while (TRUE) { while (TRUE) { starttrans; starttrans; if (! Full) if (! Empty) { { In+ +; Out+ +; if (In == BFSIZE) if (Out == BFSIZE) In -= BFSIZE; Out -= BFSIZE; if (In == Out) if (Out == In) Full = TRUE; Empty = TRUE; Empty = FALSE; Full = FALSE; } } commit; commit; } } Fig.10. Producer-consumer. Inv H , ∃ v1, v2, v3, v4. H ° Full 7→ v1 ∗ Empty 7→ v2∗ In 7→ v3 ∗ Out 7→ v4 ∧ v1 = TRUE → v2 = FALSE ∧ v2 = TRUE → v1 = FALSE ∧ v3 < BFSIZE ∧ v4 < BFSIZE L start: −{pc = L start} starttrans lw rfull Full zero addiu rtrue zero TRUE bne rfull rtrue L addin j L commit L addin: −{B.pc = L start ∧ Hw ° emp ∧ ∃ v1, v2, v3, v4. Hs ° Full 7→ v1∗ Empty 7→ v2 ∗ In 7→ v3 ∗ Out 7→ v4 ∧ v3 < BFSIZE ∧ v4 < BFSIZE ∧ R(rtrue) = TRUE ∧ v1 6= TRUE} lw rin In zero addiu rin rin 1 addiu rtemp zero BFSIZE beq rin rtemp L subR j L fcheck L fcheck: sw rin In zero lw rout Out zero beq rin rout L fset j L setemp L setemp: −{B.pc = L start ∧ ∃ v1, v2, v3, v4. Hs ° Full 7→ v1∗ Empty 7→ v2 ∗ In 7→ v3 ∗ Out 7→ v4 ∧ v3 < BFSIZE ∧ v4 < BFSIZE ∧ ((v1 6= TRUE ∧ Hw ° In 7→ v3) ∨ (v1 = TRUE ∧ Hw ° Full 7→ v1 ∗ In 7→ v3))} addiu remp zero FALSE sw remp Empty zero j L commit L commit: −{B.pc = L start ∧ ∃ v1, v3, v4. Hs ° Full 7→ v1∗ Empty 7→ FALSE ∗ In 7→ v3 ∗ Out 7→ v4 ∧ v3 < BFSIZE ∧ v4 < BFSIZE ∧ ((v1 6= TRUE ∧ Hw ° Empty 7→ FALSE ∗ In 7→ v3) ∨ (v1 = TRUE ∧ (Hw ° Full 7→ v1 ∗ Empty 7→ FALSE∗ In 7→ v3 ∨ Hw ° emp)))} commit j L start L subR: subu rin rin rtemp j L fcheck L fset: sw rtrue Full zero j L setemp Fig.11. Producer-consumer in our system