B(PN)² is a structured parallel programming language. Its syntax is easily structured and offers many of the constructs used in concurrent programming languages, among others iteration, guarded commands, parallel composition, loops, blocks, procedures and communication via channels, stacks or shared variables. For full details of B(PN)² see here. It is also one of the input languages of the PEP-tool.

We show the main concepts of B(PN)² by showing how Dekker's mutex algorithm can be specified in B(PN)².

In [RAY86] Dekker's mutex algorithm is described as follows:

     var flag: array[0..1] of boolean;
     var turn: 0..1;

flag is initialized to false, and turn has the value 0 or 1.

The protocol for process i then becomes:

     flag[i] := true;
     while flag[j] do if turn = j then
                         begin
                              flag[i] := false;
                              while turn = j do nothing enddo;
                              flag[i] := true;
                         end;
                       endif;
                    enddo;
     [critical section];
     turn := j;
     flag[i] := false;

Now we give a stepwise explanation how one can directly derive a correct B(PN)² program from this algorithm:

• The program must be surrounded by the keywords begin and end.
   
• Then the global variables must be defined. This can be done by typing:

  var flag1, flag2:{0..1} init 0;
var turn:{1..2} init 1;

  flag1 and flag2 are variables with values of 0 and 1, initially set to 0. turn is a shared variable with values of 1 and 2, initially 1.
   

• Now we can code the different processes (for example process 1):
  • Value assignment flag1:=true will be denoted with <flag1'=1>.
     
  • The while flag2 construct can be expressed in the following way:

    do
    

    <flag2=0>; exit
    []
    <flag2=1>; ...; repeat

    od

    This means that the loop will be repeated until the value of flag2 is 0.
     

  • A choice of actions will be denoted by [].
  • An if-construct can be expressed in the following way:

    do
    

    ...; exit
    []
    ...; exit
    

    od

    All alternatives are finished with exit. So the loop will be executed only once.
     

• The concurrency of the processes will be denoted by ||.

With this knowledge we are able to specify Dekker's mutex algorithm in an easy way. The corresponding B(PN)² notation looks like:

begin

var flag1, flag2:{0..1} init 0;
var turn:{1,2} init 1;


begin
do


<flag1'=1>
do

<flag2=0>;
exit
[]
<flag2=1>;
do

<turn=1>;
exit
[]
<turn=2>;
<flag1'=0>;
do

<turn=1>;
exit
[]
<turn=2>;
repeat

od;
<flag1'=1>;
exit

od;
repeat

od;
<turn'=2>;
<flag1'=0>;
repeat

od
end

||

begin
do


<flag2'=1>;
do

<flag1=0>;
exit
[]
<flag1=1>;
do

<turn=2>;
exit
[]
<turn=1>;
<flag2'=0>;
do

<turn=2>;
exit
[]
<turn=1>;
repeat

od;
<flag2'=1>;
exit

od;
repeat

od;
<turn'=1>;
<flag2'=0>;
repeat

od
end

end


Types of communication

In B(PN)² communication between processes can be realized in several ways, and one can jointly use all different kinds of communication together.

• Communication via global variables

Processes can communicate via globally defined variables. For example, in the algorithm mentioned above the processes communicate via the global variable turn.

• Communication via channels

Processes can communicate via channels acting as FIFO (First In First Out) buffers. Each channel has a fixed capacity indicating how many values can be held by the channel at any time. Channels can be defined in the following way:

var ch: chan 3 of {0..5};

This means that the channel ch has a capacity of three values ranging from 0 to 5. Actions on channels like reading and writing of values are denoted like this:

• x'=ch?
  This means that the variable x reads a value from the channel ch if the channel is not empty. Afterwards the value is deleted from the channel.
• x=ch!
  This means that the variable x writes its value to the channel ch if the capacity value allows it.
• ch??
  This expression tests if the channel ch is not empty.
• ch!!
  This expression tests if the channel ch is not already full.

• Communication via stacks

Processes can communicate via stacks which act as LIFO buffers (Last In First Out). Similarly to channels, stacks have a capacity limit which indicates how many values can be pushed onto the stack. A stack can be defined in the following way:

var st: stack 3 of {0..5};

It means that the stack st has a capacity of three values ranging from 0 to 5. Actions like putting values onto and taking values from the stack can be realized in the following way:

• x'=st?
  It means that the variable x pops a value from the stack st if the stack is not empty. Afterwards the value is deleted from the stack.
• x=st!
  It means that the variable x pushes its value to the stack st if the capacity value allows it.
• st??
  This expression tests if the stack st is not empty.
• st!!
  This expression tests if the stack st is not using its full capacity.

Setting labels

Unlike the other modelling languages B(PN)² only treats actions and abstracts from states or places and transitions. But sometimes it is desirable to denote a special control point in a program. For example, in Dekker's mutex algorithm we are interested in the question if both processes can enter their critical regions at the same time. Therefore, a notation is needed to express that the control of a process has arrived between two actions. The Kit uses an extension to the usual B(PN)² compiler which allows the user to place labels to denote special control points. These labels can then be used in formulae. Labels can be placed where actions are allowed. A label consists of a string followed by a colon.

Dekker's mutex algorithm in B(PN)² using labels can be seen here. The critical regions are labelled incs1: and incs2:, respectively.

Now one can check the mutex property like this:

check bpn2:pep-reach dekker_critlab.bpn2 mutex.form

The following output should be printed on your screen:



This is the expected result. There exists no execution sequence so that the program control stays at the labelled control points at the same time.

Atomic propositions in formulae

Atomic propositions can consist of ...

• Labels
• Expressions

of the form "x=val", "x#val", "x<val", "x>val", "x<=val", "x>=val" (# denotes inequality).
For a channel ch or a stack st one can type "ch[1]=val", "ch[2]=val", "st[3]=val", .... The number in square brackets denotes the stack position of the channel or the stack. It must not be greater than the capacity defined for the channel or the stack.

Expressions need to be typed in quotes.