116 J.Comput.Sci.Technol.,Jan.2009,Vol.24.No.1 chine is established following the syntactic approach which multiple threads cooperate on are checked.The to proving type soundness.From the "progress"and expressiveness and the application to high-level pro- "preservation"lemmas,we can guarantee that given a grams of such invariance proof method have been well- well-formed program under compatible preconditions, known.It is the atomicity and isolation properties of the current instruction sequence will be able to exe- transactional memory that make the requirement of in- cute without getting "stuck".Furthermore,any safety variant on shared memory reasonable. property derivable from the global invariant will hold In this section,we use examples to demonstrate the throughout the execution.The soundness of our system effectiveness of our reasoning system.And we present is formally stated as Theorem 1. examples in high-level programs and their assembly Lemma1(Progress).Φ=(Inw,[i,,乎n]).f counterparts,showing that reasoning about programs there exist p1,,pn,such that重，p,,pnJ卜P,then using TM in assembly level is essentially the same as in there exists a program P such that PP. high-level under such reasoning. Lemma2(Preservation).Φ=(Inv,[i,…, 亚nl).f重，p1,,Pnl上P and P-一P,then there 4.1 Dining Philosopher Algorithm erist p,,p such that重，p,.,pn]上P. Theorem 1 (Soundness).=(Inv,[1,..., A simplified example of dining philosophers in trans- 乎n]).If there erist p1,,pn,such that重，p1,· actional program style is shown in Fig.7,where two Pn]P,then for any n≥0，there erist a programP philosophers (Threadi and Thread2)share two forks andp,…,p such that P-→nP'and重，pi,,pn]H (represented by memory locations forki and fork2). A philosopher picks up a fork by writing the thread id (1 or 2)into the memory location representing the fork, 3.5 Separation Logic and puts down a fork by writing 0. We describe heaps using separation logicl271.Ex- Variables: Invariant: cept for implication,separation logic is similar to lin- nat fork1,fork2: fork1 fork2 ear logic,where register and heap bindings are treated as intuitionistic and linear resources,respectively,ex- Thread1: Thread2: tended with an axiom restricting each heap address to while (TRUE){ while (TRUE){ a single binding.We write A and B for heap predicates. starttrans; starttrans; We write HA if the heap predicate A holds on heap if (fork1){ if (fork2){ H.The syntax for the fragment of separation logic we forki =1; fork2 =2; use is given in Fig.6. fork2 =1; fork =2; commit; commit; A,B ::nm|emp A*B AA B AV B } |3x:P.B|廿x∈S.A else else commit; commit Fig.6.Separation logic. continue; continue; Now we describe these predicates informally.nm holds if the heap consists entirely of the binding of n to /eat /eat m.emp holds only on the empty heap.A*B holds if starttrans; starttrans; the heap can be split into two disjoint parts such that A fork1 =0; fork1=0; holds on one and B on the other.AA B holds if both A fork2 =0; fork2 =0; and B hold on the entire heap.AV B holds if either A commit; commit; or B holds on the heap.3x:P.B holds if there exists /think //think an z of type P such that Bz holds on the heap.P will be omitted when it is clear from the context.Vx E S.A Fig.7.Simplified example of dining philosopher algorithm. holds on a heap that satisfies Ax for all x in the finite set S. The invariant on the shared memory can be ex- pressed as(fork1=fork2),indicating that both forks 4 Examples are free(when they are all equal to 0)or a philosopher is holding them both.In the more general case of three or In our system,not only the invariant on each thread more philosophers,the invariant on the shared memory of a program but also the invariant on the global heap can be expressed as (V i.forki=0Vforki=forki+1=116 J. Comput. Sci. & Technol., Jan. 2009, Vol.24, No.1 chine is established following the syntactic approach to proving type soundness. From the “progress” and “preservation” lemmas, we can guarantee that given a well-formed program under compatible preconditions, the current instruction sequence will be able to exe￾cute without getting “stuck”. Furthermore, any safety property derivable from the global invariant will hold throughout the execution. The soundness of our system is formally stated as Theorem 1. Lemma 1 (Progress). Φ = (Inv, [Ψ1, . . . , Ψn]). If there exist p1, . . . , pn, such that Φ, [p1, . . . , pn] ` P, then there exists a program P 0 such that P 7−→ P 0 . Lemma 2 (Preservation). Φ = (Inv, [Ψ1, . . ., Ψn]). If Φ, [p1, . . . , pn] ` P and P 7−→ P 0 , then there exist p 0 1 , . . . , p0 n such that Φ, [p 0 1 , . . . , p0 n ] ` P 0 . Theorem 1 (Soundness). Φ = (Inv, [Ψ1, . . ., Ψn]). If there exist p1, . . . , pn, such that Φ, [p1, . . ., pn] ` P, then for any n > 0, there exist a program P 0 and p 0 1 , . . . , p0 n such that P 7−→n P 0 and Φ, [p 0 1 , . . . , p0 n ] ` P 0 . 3.5 Separation Logic We describe heaps using separation logic[27]. Ex￾cept for implication, separation logic is similar to lin￾ear logic, where register and heap bindings are treated as intuitionistic and linear resources, respectively, ex￾tended with an axiom restricting each heap address to a single binding. We write A and B for heap predicates. We write H ° A if the heap predicate A holds on heap H. The syntax for the fragment of separation logic we use is given in Fig.6. A, B ::= n 7→ m | emp | A ∗ B | A ∧ B | A ∨ B | ∃ x : P.B | ∀ x ∈ S.A Fig.6. Separation logic. Now we describe these predicates informally. n 7→ m holds if the heap consists entirely of the binding of n to m. emp holds only on the empty heap. A ∗ B holds if the heap can be split into two disjoint parts such that A holds on one and B on the other. A∧B holds if both A and B hold on the entire heap. A ∨ B holds if either A or B holds on the heap. ∃ x : P.B holds if there exists an x of type P such that Bx holds on the heap. P will be omitted when it is clear from the context. ∀ x ∈ S.A holds on a heap that satisfies Ax for all x in the finite set S. 4 Examples In our system, not only the invariant on each thread of a program but also the invariant on the global heap which multiple threads cooperate on are checked. The expressiveness and the application to high-level pro￾grams of such invariance proof method have been well￾known. It is the atomicity and isolation properties of transactional memory that make the requirement of in￾variant on shared memory reasonable. In this section, we use examples to demonstrate the effectiveness of our reasoning system. And we present examples in high-level programs and their assembly counterparts, showing that reasoning about programs using TM in assembly level is essentially the same as in high-level under such reasoning. 4.1 Dining Philosopher Algorithm A simplified example of dining philosophers in trans￾actional program style is shown in Fig.7, where two philosophers (Thread1 and Thread2) share two forks (represented by memory locations fork1 and fork2). A philosopher picks up a fork by writing the thread id (1 or 2) into the memory location representing the fork, and puts down a fork by writing 0. Variables: Invariant: nat fork1, fork2; fork1 = fork2 Thread1 : Thread2 : while (TRUE) { while (TRUE) { starttrans; starttrans; if (! fork1){ if (! fork2){ fork1 = 1; fork2 = 2; fork2 = 1; fork1 = 2; commit; commit; } } else { else { commit; commit; continue; continue; } } // eat // eat starttrans; starttrans; fork1 = 0; fork1 = 0; fork2 = 0; fork2 = 0; commit; commit; // think // think } } Fig.7. Simplified example of dining philosopher algorithm. The invariant on the shared memory can be ex￾pressed as (fork1 = fork2), indicating that both forks are free (when they are all equal to 0) or a philosopher is holding them both. In the more general case of three or more philosophers, the invariant on the shared memory can be expressed as (∀ i.forki = 0∨forki = forki+1 =