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 functionExample: 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 spaceExample: java -j verify.jar gadara.pn -c -h -j N -o -p N -u
Details of the verifier tool is documented here:
- Yin Wang, Jason Stanley, Stéphane Lafortune, "Explicit Storage and Analysis of Billions of States using Commodity Computers", tech report, Workshop on Descrete Event Systems 2012, parameters
Papers that use these tools for experiments:
- Ahmed Nazeem, Spyros Reveliotis, "A practical approach for maximally permissive liveness-enforcing supervision of complex resource allocation systems", IEEE Transactions on Automation Science and Engineering, vol.21, no.4, pp.499-518, 2011
- Hongwei Liao, Jason Stanley, Yin Wang, Stéphane Lafortune, Spyros Reveliotis, and Scott Mahlke, "Deadlock-Avoidance Control of Multithreaded Software: An Efficient Siphon-based Algorithm for Gadara Petri nets", IEEE Conference on Decisions and Control 2011
- Ahmed Nazeem, Spyros Reveliotis, Yin Wang, and Stéphane Lafortune, "Designing Compact and Maximally Permissive Deadlock Avoidance Policies for Complex Resource Allocation Systems Through Classification Theory: the Linear Case", IEEE Transactions on Automatic Control , vol.56, no.8, pp.1818-1833, 2011
- Yin Wang, Terence Kelly, Manjunath Kudlur, Scott Mahlke, and Stéphane Lafortune, "The application of supervisory control to deadlock avoidance in concurrent software", Workshop on Descrete Event Systems 2008
Lock/Unlock pairing module
LLVM pass for lock/unlock pairing: src.