UNDIP Prototype
Introduction
UNDIP stands for Unbounded Distributed Parameterized systems. UNDIP is a prototype for the verification of safety properties on distributed or non-distributed parameterized systems with potentially unbounded data domain. The prototype performs backward reachability on an over-approximation of the induced transition system. Difference bound matrices are used to define and manipulate the constraints on integer variables.
A parameterized system consists of an arbitrary number of identical state machines running in parallel. Each state machine operates on a finite number of unbounded variables, and communicate with each other machine through shared variables or channels. Such systems have therefore two sources of infinity: the number of processes and the domain of the manipulated data.
UNDIP can be regarded as an extension of PFS to the case where the data domain of the manipulated variables is unbounded, and where the atomic global transition can be replaced by refined non-atomic protocols. Many interesting mutual exclusion algorithms fit into this modeling framework.
Download
UNDIP is free and open source. You can download the source code for free from below. Distribution is under the GNU General Public License (GPL). We run UNDIP on Linux fc6(2.6) undip.tar.gz.Instructions
In a Linux console, extract the file, cd to the directory, type ./configure, then type make. Check the "README" and the examples to get inspired.Case studies
This is a (non exhaustive) list of the mutual exclusion algorithms we verified with UNDIP. Assuming we start from a set of constraints "B" where all constraints have the same cardinal "Card" (i.e. number of processes constrained by the constraints). We insert new processes to the generated constraints only once we reach a fixpoint within the set of constraints with the same cardinal "Card". The number of iterations corresponds to the sum of the aggregation of the number iterations for each cardinal.Models | Iterations | Constraints | Time (sec) |
---|---|---|---|
Burns alg. | 16 | 40 | < 0.05 |
Szymanski alg. | 61 | 5085 | 85 |
Dijkstra alg. | 18 | 89 | < 0.05 |
Java Meta-Lock alg. | 22 | 376 | 3.2 |
Illinois cache prot. | 10 | 46 | < 0.05 |
Firefly cache prot. | 14 | 31 | 0.1 |
Futurebus cache prot. | 10 | 46 | 0.1 |
German cache prot. | 34 | 10492 | 232 |
Bakery alg. | 11 | 29 | < 0.05 |
Bakery (buggy(*)) alg. | 7 | 67 | < 0.05 |
Bakery (all interleavings) alg. | 13 | 42 | 0.1 |
Distr. Lamport alg. | 30 | 4676 | 85 |
Distr. Ricart & Agrawala alg. | 32 | 1205 | 13 |
Related Publications
Main papers: Parameterized Verification of Infinite-state Processes with Global Conditions. Parosh Aziz Abdulla, Giorgio Delzanno, and Ahmed Rezine. In Proc. CAV 2007, 19th International Conference on Computer Aided Verification.PDF, PS.
Handling Parameterized Systems with Non-Atomic Global Conditions. Parosh Aziz Abdulla, Noomene Ben Henda, Giorgio Delzanno, and Ahmed Rezine. In Proc. VMCAI 2008, Verification, Model Checking and Abstract Interpretation.PDF, PS.
Technical report: Parameterized Verification of Infinite-state Processes with Global Conditions. Parosh Aziz Abdulla, Giorgio Delzanno, and Ahmed Rezine. IT-database 2007 Link .