 |
| the SDA project |
| home |
| news |
| download |
| documentation |
| FAQ |
| references |
| tools for deadlock analysis |
|
Typical
DECO |
| contact: |
| Cosimo Laneve |
| January 2013 |
The SDA tool can be downloaded at SDA_tool.zip site. Once the file SDA_tool.zip site has been downloaded (approx. 40 MB), uncompress it. A folder SDA_tool has been created. Go in the folder SDA_tool and run
> ant dist
In order to compile a (core) ABS file, use the command:
> bin/bash/generateJava file.abs
The executable Java code will appear in the default folder /gen. To compile an ABS file and store the executable Java code in a particular PATH, run the command:
> bin/bash/generateJava -d PATH file.abs
The SDA_tool verifies at static time the presence of deadlocks and livelocks in (core) ABS programs. The output it gives is
### OUTPUT OF THE ANALYSIS ### Saturation: [true / false] Deadlock in Main: [true / false] Livelock in Main: [true / false]
which states whether deadlocks and/or livelocks are present in the code. The answer true for deadlocks means that deadlocks may be present in the code (false positives are admitted); false means that the code will never manifest a deadlock. Similarly, the answer true for livelocks means that livelocks may be present in the code (false positives are admitted); false means that the code will never manifest a livelock.
To guarantee the termination of the analysis, the compiler uses a fixed number of iterations that can be chosen by the user running:
> bin/bash/generateJava file.abs -iter=num
where "num" is the number of iteration that the user wants to perform. The Saturation flag informs the user if this number of iteration has been reached by the compiler (in this case the analysis is less precise and can output false positives) If the "Deadlock" and "Livelock" flags are false, then (independently by the Saturation flag) the analyzed program is Deadlock/Livelock free.
For additional informations on the compilation and the run of ABS programs, see USAGE.txt in the SDA_tool folder.
A lot of examples of ABS programs, with/without deadlocks and/or livelocks, can be found in the folder /examples.