Coarse-Grained Locking Scheme for Parallel State Space Construction

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

1 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques
2 LAAS-OLC

We propose a new parallel algorithm for state space construction that is well-suited for modern, multiprocessor architectures with non-uniform memory access times. Our algorithm uses a network of distributed hash tables to store the states locally—we use one hash table per processor (or thread)—and a shared entity, suggestively called the dispatcher, to control the distribution of data among all these tables. Conflicts in accessing the same shared memory location simultaneously are resolved by a traditional CREW strategy; we use one lock per hash table to grant write accesses but read accesses are allowed to occur concurrently. With this approach, we combine the simplicity and ease of implementation of distributed hash tables with the dynamic data distribution of concurrent data structures. We evaluate the performance of our algorithm on different benchmarks.

Domaines: Systèmes embarqués; Logique en informatique [cs.LO]

Silvano Dal Zilio, Rodrigo Tacla Saad, Bernard Berthomieu. Coarse-Grained Locking Scheme for Parallel State Space Construction. Rapport LAAS n° 13048. 2013. ⟨hal-01790224⟩