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