**Analyzing
parallel applications with Petri Nets. **

The demand for high availability and reliability of computer and
software systems has led to a formal verification of such
systems. There are two principal approaches to formal
verification: model checking and theorem proving.

**I will talk about Petri Nets and
how to model parallel programs and how to exploit verification
tools as Tina to verify the properties such as liveleness of the
system. I will restrict the discussion to so-called
"1-conservative" Petri Nets, in which the capacity of
each place is assumed to be 1, and each edge will remove exactly
one mark from a net if it leads from a place to a transition and
add exactly one when it leads from a transition to a place.**

**First let's look at the following
statement:**

**If P1 is true Then P2 is true**

**Note: Predicat P1 is true means
that there is a marking in P1 and T1 is fired.**

**How to model it in Petri Nets ?**

**This statement looks like this
using Petri Nets:**

**And the following statement:**

**If both P1 AND P2 are true Then P3
is true;**

**How can you model this statement
with Petri Nets ?**

**This statement looks like this
using Petri Nets:**

**And how to model the following
statement:**

**If either P1 OR P2 is true Then P3
is true;**

**This statement looks like this
using Petri Nets:**

**And how to model the folowing
statement:**

**If either P1 OR P2 is true Then
either P4 OR P5 is true**

**Note: Predicate P1 is true means
that there is a marking in P1 ...**

**And this statement looks like this
with Petri Nets:**

**And how to model the following
statement:**

**If both P1 AND P2 are true Then
both P3 and P4 are true;**

**This statement looks like this
using Petri Nets:**

**Now , how to model a
WaitForSingleObject() ?**

**WaitForSingleObject(Object) is like
a statement:**

**If P1 is trueTHEN P2 is true**

**Note: P1 is true means the Object
is signaled **

**And this statement looks like this
using Petri Nets:**

**And how to model a
WaitForMultipleObject() on two objects - waiting on all of them -
?**

**That's easy, it looks like the
following statement:**

**If both P1 AND P2 are true THEN P3
is true, and we have already modeled this statement before..**

**Now how to model a Critical Section
?**

**If we have two threads that are
waiting on the critical section , that means ONE of them will
succeed entering the critical section , the other will wait, and
that looks like the following statement:**

**If either Thread 1 leaves CS1 OR
Thread2 leaves CS1 Then either Thread1 Enters CS1 OR Thread2
Enters CS1**

**This looks like the statement
before:**

**If either P1 OR P2 is true Then
either P4 OR P5 is true**

**And this statement looks like this
using Petri Nets:**

**Now how to model a Semaphore
created with count 4 ?**

**Here it is:**

**Now let us look at a parallel
Object Pascal example and how to model it in Petri Nets:**

**-----------------------------------------------**

**program test;**

**uses
windows,syncobjs,sysutils,classes;**

**var hnd : THandle; **

**cs1,cs2:TCriticalSection;**

**AId:DWORD; **

**function
StartFunc1(InVal:pointer):DWORD;**

**begin **

**while(true)**

**Do**

**begin**

**cs1.Enter; **

**writeln('Thread1 has entered
Critical Section 1 but not 2.'); **

**cs2.enter; **

**writeln('Thread1 has entered
Critical Section 1 and 2!'); **

**cs2.Leave; **

**writeln('Thread1 has left Critical
Section 2 but still owns 1.'); **

**cs1.Leave; **

**writeln('Thread1 has left both
critical sections...'); **

**Sleep(20); **

**end;**

**end;**

**begin**

**cs1:=TCriticalSection.create;**

**cs2:=TCriticalSection.create;**

**hnd:=BeginThread(nil,0,@StartFunc1,pointer(1),0,AId);
**

**closehandle(hnd);**

**while(true)**

**do **

**begin**

**cs2.Enter; **

**writeln('Thread1 has entered
Critical Section 2 but not 1.'); **

**cs1.enter; **

**writeln('Thread1 has entered
Critical Section 1 and 2!'); **

**cs1.Leave; **

**writeln('Thread1 has left Critical
Section 1 but still owns 2.'); **

**cs2.Leave; **

**writeln('Thread1 has left both
critical sections...'); **

**Sleep(20); **

**end;**

**cs1.free;**

**cs2.free;**

**end.**

**-----------------------------------------------------**

**The Petri Net model of the Object
Pascal program above will looks like this:**

**If we analyze the REACHABILITY of
this petri net example, with for example the tool Tina , this
will tell us that the system is bounded but it's NOT LIVE, with a
deadlock at p12 and p22. **

**So, if P12 and P22 are marked, it
means Thread1 owns critical section1 and Thread2 owns critical
section2 and since lcs_1 and lcs_2 are not marked the system is
not live and that means there is a deadlock in the system. **

**And how to avoid this deadlock ?**

**There is a rule that can be stated
as follow:**

**[1] IF two or more processes or
threads use the same critical sections THEN they - the processes
or threads - must take them in the same order to avoid deadlock -
in the system - .**

**So, in our parallel program both
threads have to take the critical sections in the same order.**

**Tina can give you information about
boundedness and place invariants of the system , but what is
place invariants - good for - ?**

**For boundedness and deadlocks...
one of the most important properties, you can use petri nets and
reason about place invariants equations that you extract from the
resolution of the following equation: Transpose(vector) *
Incidence matrix = 0 and find your vectors on wich you wil base
your reasonning... **

**As an example , suppose that you
resolve your equation Transpose(vector) * Incidence matrix = 0
and find the following equations - place invariants -**

**Note: P,Q,S,R are all the places in
the system... **

**Equation1: 2 * M(P) M(Q) +
M(S) = C1 (constant) **

**and **

**Equation2: M(P) + M(R) + M(S) = C2
(constant) **

**Note also that vector f * M0
(initial marking) = 0 **

**So, it follows - from the equations
- that since M(P) + M(R) + M(S) = C1 , it means that M(P) <=
C1 and M(R) <= C1 and M(S) <= C1 , and, from the second
invariant equation , we have that M(Q) <= C2 , this IMPLY that
the system is structuraly bounded. **

**That's the same thing for deadlocks
, you reason about invariants equations to proove that there is
no deadlock in the system... **

**That's all for now.**

**Click here to go to my website:****
http://pages.videotron.com/aminer/**

**Sincerely,
Amine Moulay Ramdane**