Process Partitioning

This case study come from Performance Evaluation of Process Partitioning using Probabilistic Model Checking [c6]. The aim is to evaluate the efficiency of several process partition.

The model describes a chain of nodes that sorts values through a propagation mechanism. A value enter through the left side of the chain. Each node compares the incoming value on its left with its current value, keeps the smaller one and propagate the greater one to the right.
The propagation of a value from node i to i+1 is modeled by the transition Τi. On the following figures, partitions are represented by the blue and red areas. The basic rules are

• Two transitions Τi and Τi+1 cannot execute simultaneously since both access node i+1.
• A partition can only execute one transition at a time.

The model evaluate the execution time of three partitions, concentric pair, distant pair and neighbor pair.

A PLASMA Lab project file containing sorting models and the properties used for this experiment can be downloaded here.

We estimated the probability for a partition to reach a given Speedup. This property can be expressed in B-LTL as:

F<=#(3*k) (c=k) & (“_pisteps” = N)

k is the number of operation that must be executed. The condition c=k indicates that all operation have been executed. “_pisteps” is a label containing the length of the execution for the partition i. N is the execution time and represents the speedup. Since the process have been partitioned in two parts, N is comprised between k/2 and k. Thus the speedup is equal to k/N.