A Dynamic, Lock free Data Dictionary for Parallel State Space Construction

Rodrigo Tacla Saad (1) , Bernard Berthomieu (1) , Silvano Dal Zilio (1)

1 LAAS - Laboratoire d'analyse et d'architecture des systèmes

We propose a novel algorithm for parallel state space construction based on an original data structure, called a localization table, that aims at better space and temporal balance. Our proposal is close in spirit to algorithms based on distributed hash tables with the distinction that states are dynamically assigned to processors; we do not rely on an a-priori static partition of the state space. Distribution of the states space and coordination between processes is made through the shared access to a localization table, that is designed to be a highly efficient, thread safe data structure. In our solution, every process keeps a share of the global state space. The localization table is used to dynamically assign newly discovered states and behaves as an associative array that returns the identity of the processor that owns a given state. With this approach, we are able to consolidate a network of local dictionaries into an (abstract) distributed data structure without sacrificing memory affinity – data that are ”logically connected” are physically close to each others – and without incurring performance costs associated to the heavy use of locks to ensure data integrity. We evaluate the performance of our algorithm based on experimental results obtained on different benchmarks and compare these results with other solutions proposed in the literature.

Mots clés: Parallel State Space Construction; Model Checking; Parallel Algorithm; Lock-Free Dictionary

Domaines: Calcul parallèle, distribué et partagé [cs.DC]

Rodrigo Tacla Saad, Bernard Berthomieu, Silvano Dal Zilio. A Dynamic, Lock free Data Dictionary for Parallel State Space Construction. 2010. ⟨hal-00523188v1⟩