As newly developed transactional memory technology has received significant attention as a way to dramatically simplify sharedmemory concurrent programming, user-level transactional concurrent programming models have become a very interesting topic in the programming community. However, the fact is that, in existing transactional concurrent programming models, user-level mechanisms hav e not been well developed. The dilemma is how to make a balance between the performance and correctness of a program. Explicit concurrency among cooperative transactions can undoubtedly decrease the rate of conflicts and improve the performance, but it is harmful to the correctness. In this paper, a transactional concurrent programming approach, based on Petri nets, is presented, which can easily specify concurrency among transactions and do not aggravate programmers remarkably in writing correct transactional concurrent programs. In this approach, a special Petri net system with transition markings is developed. Although such a Petri net system is not defined conventionally, it is shown that its behavior can be simulated through a conventional net, so existing analysis and verification approaches for usual Petri nets can be applied indirectly.
Transactional memory mechanism has recently received significant attention as a
way to dramatically simplify memory-sharing concurrent pr ogramming, in which
mutual exclusion and synchronization can be constructed without using any locks
[
In existing user-level transactional concurrent programm ing 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 [
Another solution is to extend conventional programming languages with some
transactional features, such as atomic statement-blocks, as in some new
languages Fortress [
To develop a user-level transactional concurrent programm ing 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’ w isdom 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 [
As well known, Petri nets [
Fig.1 shows a simple example described in a typical transactional concurrent program structure, where an atomic statement-block declar es 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 cont rol. 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 thread ph1: while ( true ) { atomic { read fork1 ; read fork2 ; write fork1+1 to fork1 ; write fork2+1 to fork2 ; int fork1 = 0, fork2 = 0, fork3 = 0; thread ph2: int cake_c = 12; while ( true ) { atomic { read fork2 ; read fork3 ; write fork2+1 to fork2 ; write fork3+1 to fork3 ; if ( fork2 mod 10 == 0 ) { read cake_c ; write cake_c-1 to cake_c ; } } } } } thread ph3: while ( true ) { atomic { read fork3 ; read fork1 ; write fork3+1 to fork3 ; write fork1+1 to fork1 ; if ( fork1 mod 20 == 0 ) { read cake_c ; write cake_c-1 to 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 is’, hence, it is assumed that fork i’s be critical shared objects among phis’, and cake_c be the non-critical shared object among them.
The Petri net model we use is a special colored Petri net model [
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. 2
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 VR, and the set of global variables is denoted by VT .
A resource net system is a special colored Petri net system N = (P, T, A, W, m0, MF ), where
MT cake_c : 12
MR fork1 : 0 fork2 : 0 fork3 : 0
ph1 1: read fork1 ; read fork2 ; write fork1+1 to fork1 ; write fork2+1 to fork2 fk2 fk1 fk3 – P ⊆ { ρk | k ∈ N} , and T ⊆ { (τk, Ik) | k ∈ N} are the set of places and the set of transitions respectively. – A = (P × T) ∪ (T × P) is the set of arcs. – W : A → { S | S ⊆ VR} is the inscription function. – m0 ∈ Marking is the initial marking, where Marking =
{ m | m : (P ∪ T) → { S | S ⊆ VR} . – MF ⊆ Marking is the set of final markings.
A resource net system N = (P, T, A, W, m0, MF ) has the following features: – For each transition (τk, Ik) ∈ T, a command sequence Ik is attached. When a transition (τk, Ik) is fired, it starts a transaction for the command sequence Ik. A command in Ik can access shared variables in VR ∪VT , 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 MF is empty, which is the usual case in conventional Petri net systems..
It is worth to noting that variables in VR should be disjoined in locations with each other, which are usually implemented by the compiler. 2.1
Example 1 Fig.2 shows a transactional concurrent program with VR = { fork 1, fork 2,fork 3} and VT = { cake_c }. The resource net system N = (P, T, A, W, m0, MF ), where – P = { f k1, f k2, f k3} . – T = { tr1, tr2, tr3} , where tr1 = (ph1, I1), tr2 = (ph2, I2), and tr3 = (ph3, I3), where I1, I2 and I3 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} . – m0 ∈ Marking is defined by: m0(f k1) = { fork1} , m0(f k2) = { fork2} , m0(f k3) = { fork3} , and m0(τ ) = ∅ for τ = tr1, tr2, tr3.
– MF = ∅. 2.2
A resource net system N = (P, T, A, W, m0, MF ) is well-formed , if – P ∩ T = ∅. – ∀ρ ∈ P.∀v1, v2 ∈ m0(ρ).(v1 6= v2), that is, at the initial marking, all tokens owned by a place are corresponding to different resource variables. – ∀ρ1, ρ2 ∈ P.∀v1∀v2.(ρ1 6= ρ2 ∧ v1 ∈ m0(ρ1) ∧ v2 ∈ m0(ρ2) → v1 6= v2), that is, at the initial marking, tokens owned by different places have disjoint resource variables. – ∀τ ∈ T.(m0(τ ) = ∅), that is, at the initial marking, every transition contains no tokens. – ∀m ∈ MF .∀τ ∈ T.(m(τ ) = ∅), that is, at each of final markings, every transition will not contain any tokens. – ∀τ ∈ T.∀ρ1, ρ2 ∈ • τ.∀v1∀v2.(ρ1 6= ρ2 ∧ v1 ∈ W (τ, ρ1) ∧ v2 ∈ W (τ, ρ2) → v1 6= v2), that is, all sets of resource variables on the incoming arcs of the same transition are disjoined with each other. – ∀τ ∈ T.∀ρ1, ρ2 ∈ τ • .∀v1∀v2.(ρ1 6= ρ2 ∧ v1 ∈ W (ρ1, τ ) ∧ v2 ∈ W (ρ2, τ ) → v1 6= v2), that is, all sets of memory blocks on the outgoing arcs of the same transition are disjoined with each other. – ∀τ ∈ T.∀ρ ∈ τ • .(W (τ, ρ) ⊆ Sρ′ ∈• τ (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 dyna mic 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. 2.3
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 6= 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 6= x2 ∧ v1 ∈ m(x1) ∧ v2 ∈ m(x2) → v1 6= 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 wel l-formed program state during its execution. 3
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.
…… m …… m (a) …… m enter
rollback (b)
commit …… m Example 4 Consider the well-formed resource net system N = (P, T, A, W, m0, MF ) in Example 1. desugar(N ) = (P′ , T′ , A′ , W ′ , m′0, M F′ ) can be depicted in Fig.4, where
It is not difficult to establish a behavior simulation relation between N and desugar(N ), and show that many behavior properties, including deadlockf-reeness , 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 ρτ . 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. 5
A sample userl-evel transactional concurrent
programming tool
A sample user-level transactional concurrent programming tool has been developing in
our lab, based on available software sources, DSTM2 [
A simple visual IDE for this programming model has been developing. 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.
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"); } } 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 [
The statical semantic check for a Petri net system is corresponding to the definition of a wellf-ormed resource net system in Section 2.2.
STM Integration The transactional memory support is based on DSTM2 [
In order to integrate DSTM2s’ API, we need to make some modific ation 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 D STM2s’ APIs. Petri Net Virtual Machine As stated above, a Petri net system is finally translated to some class inherited from a class PetriNet, which encapsulates interfaces for a special Petri net virtual machine. The Petri net virtual machine is now simply designed with the following instructions: – AddTransition (name,code) – AddPlace (name,resource) – AddArc (Source, Target, Inscription) – Start () – Join () 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. package base_directory.pnml.compile; public class Test { private resource int a =0; private resource int b =0; public static void main(String[] args) {
Test t= new Test(); new PNTest(t).start(); } public petrinet void f1() {
a=1; } public petrinet void f2() {
System.out.print("a="+a); b=3; } public petrinet void f3() {
System.out.print("a="+a); System.out.print("b="+b); a=4; b=5; }
}
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 [
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
public void run () {
Commit(); } }); Thread.onAbort(new Runnable() { public void run () {
Abort(); } }); Thread.doIt(new Callable<Void>() { public Void call ()
throws Exception {
DoThings(); } });
transactional memory, a finer granularity of concurrency can be achieved in a Petri net system, and the scale of the net model can be controlled flexibly. On the other hand, with a Petri net system, the concurrency among cooperative transactions can be built explicitly, which can undoubtedly decrease the rate of conflicts and improve the performance, while the analysis and verification capability of a Petri net model can be inherited.
The main idea in a resource net system, the net system presented in the paper, is to classify shared resources in two classes: (1) resources such that the access policy is driven by the net structure, so that mutual exclusion is guaranteed; (2) resources 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 sy stem 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 indir ectly by verifying those for
its desugaring net system. For example, INA tool [
A practical user-level transactional concurrent programm ing tool, based on DSTM2
[
Certainly, the approach could be extended to other formalisms as well. Furthermore, how to decide critical or non-critical shared objects, we be lieve, would become an interesting area in software design methodology.