Introduction

Transactional memory mechanism has recently received significant attention as a way to dramatically simplify memory-sharing concurrent programming, in which mutual exclusion and synchronization can be constructed without using any locks [1]. For convenience,a concurrent programming model based on transactional memory mechanism is called a transactional concurrent programming model in this paper.

In existing user-level transactional concurrent programming models, there are two major solutions. One of them is to use directly some API's for transactional memory mechanism, which may be implemented by hardware, software or hybrid. For example, programmers can write transactional concurrent programs in Java together with the library DSTM2 [2], or in C together with the library TL2-x86 [3]. The advantage of this solution is that one can use existing common languages without changing their compilers, but programmers have to use non-structural library functions carefully.

Another solution is to extend conventional programming languages with some transactional features, such as atomic statement-blocks, as in some new languages Fortress [4], X10 [5], Chapel [6], etc. In this solution, it is easier for programmers to write correct transactional concurrent programs, however, an appropriate compiler must be provided.

To develop a user-level transactional concurrent programming mechanisms, one dilemma is how to make a balance between the performance and correctness of a program. On the one hand, to write an efficient program in the transactional programming paradigm, it still needs programmers' wisdom to build the explicit parallelism among cooperative transactions, in order to decrease the rate of conflicts. On the other hand, however, explicit parallelism is harmful to the correctness of a program, while one of the initial intents of the transactional memory mechanism is to alleviate the burden for a programmer to write concurrent programs.

There have been some contributions in the literature to introduce transactions into existing concurrent programming model. For example, a CCR-based transactional concurrent programming model was proposed by T. Harris and K. Fraser [7], and Baek et al extend the API's of OpenMP [8] to OpenTM [9]. Unfortunately, these approaches still have the usual drawbacks of concurrent programs, that is, not easy to write and not easy to verify.

As well known, Petri nets [10] are useful tools in the specification and verification of concurrent applications. With true concurrency dynamical semantics, a Petri net system has a good opportunity to become a realistic part of a concurrent program for multi-core or multi-thread architecture. In this paper, we present informally a transactional concurrent programming mechanism based on a Petri net, in order to specify concurrency among transactions explicitly while not to aggravate programmers remarkably in writing correct concurrent programs.

Fig. 1 shows a simple example described in a typical transactional concurrent program structure, where an atomic statement-block declares a transactional region, and fork 1, fork 2, fork 3 and cake_c are shared objects among cooperative transactions.

In the Petri net system shown in Fig. 2, to be explained in more details, each of the transitions declares a transactional region, and fork 1, fork 2, fork 3 and cake_c are shared objects among three cooperative transactions. Since the accesses of fork 1, fork 2 , and fork 3 will never conflict, the rate of access conflicts among transactions is decreased, compared to the program in Fig. 1.

Extremely, we can protect all shared objects by the Petri net system, corresponding to the so-called conservative concurrency control. However, if the number of shared objects increases dramatically, the net system may get too big in size. Fortunately, we can leave some shared objects to be protected by the int fork1 = 0, fork2 = 0, fork3 = 0; int cake_c = transactional memory mechanism, if the probability of access conflicts for those shared objects is not that big. For example, we have not made the accesses to cake_c protected by the net system in Fig. 2.

We call a shared object to be critical or non-critical according to its probability of access conflicts. So in the transactional concurrent programming approach suggested in this paper, programmers are encouraged to implement the protection of critical shared objects through Petri net systems, and to leave the non-critical shared objects to be protected automatically by the transactional memory system. In the example shown in Fig. 1 and Fig. 2, the shared object cake_c is less frequently accessed than fork i's, hence, it is assumed that fork i's be critical shared objects among phi's, and cake_c be the non-critical shared object among them.

The Petri net model we use is a special colored Petri net model [11], called resource nets, which guarantee the access consistency for shared objects. The semantics for a transactional memory mechanism is inspired by the implementation of DSTM2 [2].

The rest of the paper is organized as follows. In Section 2, we make some informal interpretation to the Petri net model, resource nets. Further in Section 3, the behavior simulation of a resource net system is discussed. Then in Section 4, the program model is briefly presented. Section 5 shows a sample user-level transactional concurrent programming tool, where the concept resource nets is applied. Finally, Section 6 gives some remarks and the future work.

The Net Model

As stated above, a transactional concurrent program can access two classes of shared objects, critical or non-critical ones. We use resource variables to access critical shared objects, and global variables to access non-critical shared objects. In the following, the set of resource variables is denoted by V R , and the set of global variables is denoted by V T .

A resource net system is a special colored Petri net system N = (P, T, A, W, m 0 , M F ), where ¡1:

••••• •••••• fork1 fork2 fork3 •••••• cake_c : 12-A = (P × T) ∪ (T × P) is the set of arcs. -W : A → {S | S ⊆ V R } is the inscription function. -m 0 ∈ Marking is the initial marking, where Marking = {m | m : (P ∪ T) → {S | S ⊆ V R }}. -M F ⊆ Marking is the set of final markings.

A resource net system N = (P, T, A, W, m 0 , M F ) has the following features:

-For each transition (τ k , I k ) ∈ T, a command sequence I k is attached. When a transition (τ k , I k

) is fired, it starts a transaction for the command sequence I k . A command in I k can access shared variables in V R ∪V T , and the variables local to τ k . -A transition can hold a token while its transaction is executing, and the token does not return to the net system until the computation is committed or aborted. So we extend the definition of marking with transition markings.

-It is possible that M F is empty, which is the usual case in conventional Petri net systems..

It is worth to noting that variables in V R should be disjoined in locations with each other, which are usually implemented by the compiler.

An Example

Example 1 Fig. 2 shows a transactional concurrent program with V R = { fork 1, fork 2,fork 3} and V T = { cake_c }. The resource net system N = (P, T, A, W, m 0 , M F ), where

-P = {f k1, f k2, f k3}. -T = {tr1, tr2, tr3}

, where tr1 = (ph1, I 1 ), tr2 = (ph2, I 2 ), and tr3 = (ph3, I 3 ), where I 1 , I 2 and I 3 are command sequences attached to transitions ph1, ph2, and ph3 respectively, as is illustrated in Fig. 2.

-A = {(tr1,f k1), (tr1,f k2), (tr2,f k2), (tr2,f k3), (tr3,f k3), (tr3,f k1), (f k1,tr1), (f k1, tr3), (f k2, tr2), (f k2, tr1), (f k3, tr3), (f k3, tr2)}.

-W is defined by:

W (f k1, tr1) = W (tr1, f k1) = W (f k1, tr3) = W (tr3, f k1) = {fork1}, W (f k2, tr2) = W (tr2, f k2) = W (f k2, tr1) = W (tr1, f k2) = {fork2}, W (f k3, tr2) = W (tr2, f k3) = W (f k3, tr3) = W (tr3, f k3) = {fork3}. -m 0 ∈ Marking is defined by: m 0 (f k1) = {fork1}, m 0 (f k2) = {fork2}, m 0 (f k3) = {fork3}, and m 0 (τ ) = ∅ for τ = tr1, tr2, tr3. -M F = ∅.

Well-Formed Resource Net Systems

A resource net system N = (P, T, A, W, m 0 , M F ) is well-formed, if

-P ∩ T = ∅. -∀ρ ∈ P.∀v 1 , v 2 ∈ m 0 (ρ).(v 1 = v 2 )

, that is, at the initial marking, all tokens owned by a place are corresponding to different resource variables.

-∀ρ 1 , ρ 2 ∈ P.∀v 1 ∀v 2 .(ρ 1 = ρ 2 ∧ v 1 ∈ m 0 (ρ 1 ) ∧ v 2 ∈ m 0 (ρ 2 ) → v 1 = v 2 ), that is,

at the initial marking, tokens owned by different places have disjoint resource variables.

-∀τ ∈ T.(m 0 (τ ) = ∅), that is, at the initial marking, every transition contains no tokens. -∀m ∈ M F .∀τ ∈ T.(m(τ ) = ∅), that is, at each of final markings, every transition will not contain any tokens.

-∀τ ∈ T.∀ρ 1 , ρ 2 ∈ •τ.∀v 1 ∀v 2 .(ρ 1 = ρ 2 ∧ v 1 ∈ W (τ, ρ 1 ) ∧ v 2 ∈ W (τ, ρ 2 ) → v 1 = v 2 )

, that is, all sets of resource variables on the incoming arcs of the same transition are disjoined with each other.

-

∀τ ∈ T.∀ρ 1 , ρ 2 ∈ τ • .∀v 1 ∀v 2 .(ρ 1 = ρ 2 ∧ v 1 ∈ W (ρ 1 , τ ) ∧ v 2 ∈ W (ρ 2 , τ ) → v 1 = v 2 )

, that is, all sets of memory blocks on the outgoing arcs of the same transition are disjoined with each other.

-∀τ ∈ T.∀ρ ∈ τ • .(W (τ, ρ) ⊆ ρ ′ ∈•τ (W ((ρ ′ , τ )))

, that is, no extra shared objects be produced within a transaction associated to each of transitions.

For simplification,in this paper, we don't consider the dynamic memory allocation for a shared object within a transaction.

In the above,the pre-set and post-set of a transition τ ∈ T or a place ρ ∈ P are used, which are defined as usual:

•τ = {ρ | (ρ, τ ) ∈ A}, τ • = {ρ | (τ, ρ) ∈ A}, •ρ = {τ | (τ, ρ) ∈ A}, and ρ• = {τ | (ρ, τ ) ∈ A}.

Example 2 It is easy to show that the resource net system in Example 1 is well-formed.

Execution Semantics

To show the execution semantics of a resource net system, we define TranState = {blocked, active, aborted, committed }, consisting of 4 transaction states of a transition. At the initial marking, every transition has the state blocked.

Entering a Transition Whenever a transition τ in the resource net system is in state blocked, and the firing condition for τ is satisfied under the current marking m, that is, ∀ρ ∈ •τ.(m(ρ) ⊇ W (ρ, τ )), and in the same time, the current marking is not a final state, that is, m / ∈ MF , the system can enter the transition such that a transaction is started and the transition gets to hold tokens. When it occurs, the state of the τ will be active.

Execution of a Command Sequence Whenever a transition τ in the resource net system is in state active, and the next command in its remained command sequence is c, the transition can make a progress by executing the command c. We need several separate rules respectively for several cases:

(1) If c reads or writes to a global variable which has been written most recently by some other transition but τ , a read/write confliction occurs, and τ will be in the state aborted.

(2) If the execution of c has no read/write confliction and c has no write operation to any global variables, the transition will keep in state active.

(3) If the execution of c has no read/write confliction and c has a write operation to some global variable x, the transition will keep in state active, while the system will record τ to be the transition that most recently written to x.

Ready to Commit a Transaction Whenever a transition τ in the resource net system is in state active, and there is no next command in its remained command sequence, the system can make a progress to change the state of τ from active to committed, meaning that the transaction associated to τ is ready to commit.

Committing a Transaction Whenever a transition τ in the resource net system is in state committed, the system can make a progress to commit the transaction associated to τ , changing the state of τ from committed to blocked.

Aborting a Transaction Whenever a transition τ in the resource net system is in state aborted, the system can make a progress to return tokens to places in the pre-set of τ , changing the state of τ from aborted to blocked.

Let N = (P, T, A, W, m0, MF ) be a well-formed resource net system, it is easy to show that for any reachable marking m from the initial marking m0, the following two properties are satisfied -∀x ∈ P ∪ T.∀v1, v2 ∈ m(x).(v1 = v2),that is, at the marking m, all tokens owned by a place or a transition are corresponding to different resource variables.

-∀x1, x2 ∈ P ∪ T.∀v1∀v2.(x1 = x2 ∧ v1 ∈ m(x1) ∧ v2 ∈ m(x2) → v1 = v2), that is,

at the marking m, all tokens owned by different places or transitions have disjoint resource variables.

Example 3 Since the resource net system N = (P, T, A, W, m0, MF ) in Example 1 is well-formed. So the above two properties will keep in a well-formed program state during its execution.

Behavior Simulation of a Resource Net System

In this section, it will be shown that a well-formed resource net system N can be reduced to an usual colored Petri net system desugar(N ) so that the behavior of N can be simulated by desugar(N ), which can be analyzed and verified by using existing approaches in the Petri net community. The transformation from N to desugar(N ) is called desugaring. Before and after desugaring, the change of net structure can be illustrated by Fig. 3.

-P ′ = {f k1, f k2, f k3, ρ ph1 , ρ ph2 , ρ ph3 }.

-T ′ = {ph1enter, ph2enter, ph3enter, ..., ph3commit} -A ′ = {(ph1enter, ρ ph1 ), (ph2enter, ρ ph2 ), (ph3enter, ρ ph3 ), ..., (f k1, ph1enter), (f k1, ph3enter), ..., (ph1 rollback , f k1), (ph3 rollback , f k1), ..., (ph1commit, f k1), (ph3commit, f k1), ..., ..., (ph3commit, f k3)}. -The definition of W ′ is illustrated in Table 1

(partly). -m ′ 0 is defined by m ′ 0 (ρ ph1 ) = m ′ 0 (ρ ph2 ) = m ′ 0 (ρ ph3 ) = ∅, m ′ 0 (f k1) = {{fork1}}, m ′ 0 (f k2) = {{fork2}}, and m ′ 0 (f k3) = {{fork3}}. -M ′ F = ∅.

It is not difficult to establish a behavior simulation relation between N and desugar(N ), and show that many behavior properties, including deadlock-freeness, for N can be verified indirectly by verifying those for desugar(N ). For example, it is easy to verify that the usual Petri net system desugar(N ) in Example 4 is deadlock-free, so we can conclude that the resource net system N is also deadlock-free.

It is worth to noting that the execution semantics can guarantee behaviour consistence between N and desugar(N ). For every transition τ in N and ρτ in desugar(N ) as illustrated in Fig. 3, we have -If τ is in state blocked, there no token in ρτ , and τenter is enabled. If τenter fires, τ will be in state active at the same time.

-If τ is in state active, nether τcommit or τ rollback will fire though there exist tokens in ρτ .

-If τ is in state committed, τcommit is enabled. -If τ is in state aborted, τ rollback is enabled.

τ is in state active, committed, or aborted, iff there no token in ρτ .

Table 1. W′ : A ′ → {L | L ⊆ 2 Label } if a = then W ′ (a) = (ph1enter, ρ ph1 ) {{fork1}, {fork2}} (ph2enter, ρ ph2 ) {{fork2}, {fork3}} (ph3enter, ρ ph3 ) {{fork3}, {fork1}} ... ... (f k1, ph1enter) {{fork1}} (f k1, ph3enter) {{fork1}} ... ... (ph1 rollback , f k1) {{fork1}} (ph3 rollback , f k1) {{fork1}} ... ... (ph1commit, f k1) {{fork1}} (ph3commit, f k1) {{fork1}} ... ... (ph3commit, f k3) {{fork3}}

For the sake of limited space, in this paper, we have not formally defined the desugaring and the behavior simulation relation.

The Program Model

In the transactional concurrent programming approach of this paper, a program consists of a set of Petri net systems, which are protected parts in the system, and a set of unprotected threads which contains an initial thread identified root and other unprotected threads. Resource variables can only be accessed within protected parts. At the beginning, the thread root is initialized to execute at the level which we call top level.

A set of Petri net systems can spawn outside a Petri net system, initialized with new allocated resource variables or their references. When a transition in a Petri net system is fired, it becomes a (transactional) transition thread, which will eventually commit, or rollback due to conflicts to access the shared memory.

An unprotected thread except for the thread root can be spawned outside a Petri net system.

The program ends if all the Petri net systems achieve one of their final states, and in the same time all the unprotected threads execute to the end.

A sample user-level transactional concurrent programming tool

A sample user-level transactional concurrent programming tool has been developing in our lab, based on available software sources, DSTM2 [2], PNK [13] and GJC [14]. In the programming model of this sample programming tool, a program consists of a set of Petri net systems, corresponding to resource net systems in this paper, and other part written in Java Language.

A simple visual IDE for this programming model has been developing.

Fig. 5. A basic editing view

Editors In the IDE, each of the elements of a program can be visually edited. Fig. 5 shows a basic editing view. A editor for a Petri net system is similar to that provided in PNK source, but some modifications to add code editing area, to make the code editing to be the main input area, and to integrate with associate compilation operations.

Fig. 6. A visual Petri net system

A visually edited Petri net system will be automatically translated to some code to be fed to the compiler. It actually completes a class inherited from a class PetriNet for the programmer, where PetriNet is the class encapsulated for a special Petri net virtual machine. For example, for the Petri net system in Fig. 6, the result class will be the one in Fig. 7.

package base_directory.pnml.compile; public class PNTest extends PetriNet{ public PNTest(Object objectSource) { super(objectSource); this.AddTransition("t1","code", "f1"); this.AddTransition("t2","code", "f2"); this.AddTransition("t3","code", "f3"); this.AddPlace("p1", "a,b", "marking"); this.AddPlace("p2", "", "marking"); this.AddArc("p1", "t1", "a", "inscription"); this.AddArc("t1", "p2", "a", "inscription"); this.AddArc("p1", "t2", "b", "inscription"); this.AddArc("t2", "p2", "b", "inscription"); this.AddArc("p2", "t3", "a,b", "inscription"); } } Fig. 7. Class for a Petri net system Associate Compilation The associate compilation makes the static check of a Petri net system, then associates its code with all other parts of opened codes and compiles them together with each other. At the early time of the compilation, the Petri net system is translated into its internal form as the Petri net virtual machine instructions, which then is added to its specific class.

Variables corresponding to transaction memory blocks and resource memory blocks are declared with the modifiers global and resource respectively. Besides, the code for each transition of a Petri net system is defined by a specific member function with the modifier petrinet. In the associate compilation, the lexical, syntactical, and semantical analysis associate to the modifiers global, resource and petrinet has been processed carefully.

The compiler has been implemented based on GJC [14], a open Java compiler released by Sun, and kept the original logic of GJC unchanged.

The statical semantic check for a Petri net system is corresponding to the definition of a well-formed resource net system in Section 2.2.

STM Integration

The transactional memory support is based on DSTM2 [2], with each piece of transition code automatically trisected by invoking provided STM APIs. Hence the variable with modifier Global can be protected by the transactional memory system.

In order to integrate DSTM2's API, we need to make some modification to GJC. We need to change the type of every variable with modifier Global to a wrapper class with a factory. Also we need to change every reference of those variables and every left-value consisted of those variables to corresponding DSTM2's APIs. where AddTransition, AddPlace, and AddArc are used to construct a Petri net system, and Start and Join used for scheduling the execution of a Petri net system.

Fig. 9 shows an example to start the Petri net system defined in Fig. 6 or Fig. 7. One possible execution result will be "a=1 a=1 b=3", and another possible result is "a=0 a=1 b=3", as is illustrated in Fig. 10. Fig. 11 and Fig. 12 illustrate the integration of a simple Petri net transition simulator and DSTM routine. The left routine in Fig. 11 simulate a Petri net transition to do something, and the right part is the DSTM routine to do the same task. Fig. 12 integrates the functions of two routines in Fig. 11, getting a so-called PNTM routine.

The Petri net virtual machine can be implemented on any architecture you like, especially, it will be helpful if the target architecture can efficiently support concurrent programming, such as a CMP system. Until now, we have just implemented the Petri net virtual machine based on JVM.

The latest stable version of source code, in which the invoking of STM API's in DSTM2 has not been packaged, can be downloaded at the URL: http://soft.cs.tsinghua.edu.cn/~wang/projects/NSFC90818019/software/pntm.rar

We are making a research plan to extend the virtual machine and its implementation based on some reconfigurable simulator for multi-core architectures such that some basic performance analysis could be made. The paper presents an approach to integrate a Petri net system with a transitional memory mechanism, which has currently been applied to the implementation of a userlevel transactional concurrent programming tool in our lab. There is few formalism to play such a role as we have known so far. There exist researches based on Petri nets to model atomic or transactional threads, however the net system is not a part of the program. For example, an approach to check causal atomicity is proposed by modeling programs using Petri Nets [12]. At some extent, concurrent programming models based on Petri nets, such as OPN [15], CLOWN [16], COO [17], CO-OPN/2 [18], and Elementary Object Nets [19] may be extended to support various transaction semantics with the conservative concurrency control.

We observed that the integration of Petri nets with transactional memory can bring benefits to both side, which is the motivation of the paper. On the one hand, with whose access policy is driven by a transactional memory model, with possible conflicts, resolved by a commit-rollback protocol.

That is, our approach advocates the methodology that critical objects shared among concurrent transactions will be protected through a resource net system, while noncritical shared objects be left protected automatically by the transactional memory system. Thus the net system can be designed flexibly to keep a moderate size and in a finer granularity than usual net system.

It is shown that the behavior of a well-formed resource net system can be simulated by its desugar net system, which can be analyzed and verified by using existing approaches in the Petri net community. Behavior properties for a well-formed resource net system, such as deadlock-freeness, can be verified indirectly by verifying those for its desugaring net system. For example, INA tool [20] can be directly integrated into our programming tool being developed, as has been done in PNK.

A practical user-level transactional concurrent programming tool, based on DSTM2 [2], PNK [13] and GJC [14], has been developing in our lab. The version so far is not suitable to make a performance analysis because the target virtual machine on which a program with Petri net structures runs is implemented simply based on JVM. We are making a plan to extend the virtual machine and its implementation such that some basic performance analysis could be made.

Certainly, the approach could be extended to other formalisms as well. Furthermore, how to decide critical or non-critical shared objects, we believe, would become an interesting area in software design methodology.