Orchestrating the execution of parallel programs using Discrete Control Theory

Gadara Software

Gadara involves program analysis, control synthesis and code instrumentation. Different research communities have expressed interest in different modules of Gadara software. Unfortunately our original Gadara was monolithic. We have re-architected the tool using a modular design. Different components will be available as the software development progresses. Contact us if you have any special interest.

Figure 1 is the architecture of Gadara used in our papers. At a high level, we divide the software system into three modules, source code analysis for modeling, control synthesis for deadlock-free control logic, and source code instrumentation for deadlock-free binary.

Figure 1. Gadara Architecture






Control synthesis module

Control synthesis module takes as input a Gadara Petri net specified in our text format, and outputs the net with augmented control places. Currently we offer a random Gadara Petri net generator tool with configurable parameters, and a Gadara net verifier tool that checks the Gadara net format and examines whether the net is live or not. The verifier examines the entire state space to find unsafe states. It uses advanced data structure to minimize the memory footprint, and utilizes multithreading for parallel computation. Our experiment shows that the verifier scales to billions of states.

1. Random Gadara net generator tool, ver 0.1.16, jar, src.

Usage: java -j randomgen.jar [options...]

-b N : probability to generate branches over sequences
-h : help information
-l N : number of locks (resource) shared
-n N : number of functions (process subnets)
-r N : probability to acquire a new lock instead of releasing one already held
-s N : seed for random number generator
-t N : max number of acquisition/release steps per function

Example: java -j randomgen.jar -b N -h -l N -n N -r N -s N -t N

2. Multithreaded Gadara net verifier tool, ver 0.1.48, jar, src.

Usage: java -j verify.jar [FILE] [options...]

-c : use Cartesian product index instead of tree index, which is faster but needs more memory
-h : help information
-j N : number of concurrent threads
-o : calculate the state space of the original uncontrolled system, ignoring control places
-p N : progress display interval (sec), no display if it is 0 (default)
-u : calculate the unsafe state space

Example: java -j verify.jar gadara.pn -c -h -j N -o -p N -u

Details of the verifier tool is documented here:

Papers that use these tools for experiments:







Lock/Unlock pairing module

LLVM pass for lock/unlock pairing: src.