PARallel program DESigner (PARDES)
PARDES is an extensible distributed framework for automated design of the behavioral evolution of shared memory parallel programs. For example, given a program P that already satisfies a set of LTL properties, denoted Spec, and a new leads-to property L raised due to new requirements, PARDES enables developers to automatically determine whether or not there exists a revised version of P that satisfies (Spec
Ù L). If so, PARDES automatically generates a revised version of P that actually satisfies (Spec Ù L). To do so, PARDES enables developers to distribute program actions on a network of machines connected by TCP/IP protocol. Current implementation of PARDES is in C++ and we use symbolic techniques (e.g., BDDs) to represent programs. However, the implementation of each node of PARDES could potentially be different depending on the complexity of program actions. The source of PARDES is not currently available, but we provide the executables of two examples, namely a token passing program and a barrier synchronization protocol, for the addition of leads-to properties. A complete description of these examples and the underlying theory of PARDES is available here. The following Figure illustrates the architecture of PARDES:
For each one of the following examples the file synCoor.exe is the coordinator and an instance of synNode.exe can be instantiated for different program actions. Here is te command line for executing synCoor and synNode:
\> synCoor -p (port no.) -n (number of nodes that should be coordinated
by synCoor)
\> synNode -i (server IP address) -p (server port) -n (process number)
-a (action number)
Token Passing Example:
Case 1: Adding the first leads-to property that guarantees from every initial state the token passing program will reach a state where there is exactly one token (see this for a complete explanation of the Token Passing example). This addition can be done over a network of workstations using the following executables:
Executable for the coordinator
Executable for a node
In this case, you need to run the following on the command line of the machine where the coordinator is located:
synCoor -p (PORT) -n 3 // substitute port with an available PORTnumber
You also need to run the following on the command line of each machine where a node is located:
synNode -i IP ADDRESS -p (PORT) -n %1 -a %2 // substitute IP ADDRESS with the IP address of the coordinator and PORT with the server port number
// The option -n requires the index of the process whose action is being analyzed in this node. The action number is being represented by the option -a
Case 2: Adding the second leads-to property that guarantees
from every state where one token exists, the passing program will reach
a stable state (see
this for a more details). This addition can be done over a network
of workstations using the following executables:
Executable for the coordinator
Executable for a node
Barrier Synchronization Protocol:
Please read this for a complete explanation of the Barrier Synchronization protocol. The executables of a version of Barrier Synchronization protocol with 18 processes follows (each process has 3 actions, thereby creating 54 addition nodes). You may run it similar to the instructions given for the token passing example.
Executable for the coordinator (synCoor -p (PORT) -n 54)
Executable for a node (synNode -i IP ADDRESS -p (PORT) -n %1 -a %2 )
Model Checking the Synthesized Programs:
While the algorithm in this generate programs that are correct-by-construction, we do not have the same confidence in the implementation of our algorithm in PARDES. (In fact, it is a very difficult task to verify our implementation, if not impossible!) For this reason, we model check the code generated by PARDES to gain more confidence in the implementation of PARDES. The Promela models of the synthesized programs are as follows:
Promela Code of the synthesized Token Passing program after adding the first leads-to property is available here.
Promela Code of the synthesized Barrier Synchronization program after adding the first leads-to property is available here.
| Short bio CV Research Teaching |