# UNDIP Prototype

## Introduction

**UNDIP** stands for **Un**bounded **Di**stributed **P**arameterized 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 |

^{(*)}A Bug was introduced on purpose. A counter-example (trace) is returned by the prototype.

## 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 .