article

Measuring and Evaluating Parallel State-Space Exploration Algorithms

Authors:

Jonathan Ezekiel,

Gerald LüttgenAuthors Info & Claims

Electronic Notes in Theoretical Computer Science (ENTCS), Volume 198, Issue 1

Pages 47 - 61

https://doi.org/10.1016/j.entcs.2007.10.020

Published: 01 February 2008 Publication History

Abstract

We argue in this paper that benchmarking should be complemented by direct measurement of parallelisation overheads when evaluating parallel state-space exploration algorithms. This poses several challenges that so far have not been addressed in the literature: what exactly are those overheads, how can and cannot they be measured, and how should system models be selected in order to expose the causes of parallelisation (in)efficiencies? We discuss and answer these questions based on our experience with parallelising Saturation - a symbolic algorithm for generating state-spaces of asynchronous system models - on a shared-memory architecture. Doing so will hopefully spare newcomers to the growing PDMC community from having to learn these lessons the hard way, as we did over a painful period of almost three years.

References

[1]

Baker, M. and Buyya, R., Cluster computing: The commodity supercomputer. SPE. v29. 551-576.

Digital Library

[2]

Behrmann, G., Hune, T. and Vaandrager, F.W., Distributing timed model checking -- How the search order matters. In: LNCS, 1855. pp. 216-231.

Digital Library

[3]

Bollig, B., Leucker, M. and Weber, M., Local parallel model checking for the alternation-free μ-calculus. In: LNCS, 2318. pp. 128-147.

Digital Library

[4]

Brim, L., Černá, I., Krčál, P. and Pelánek, R., Distributed LTL model checking based on negative cycle detection. In: LNCS, 2245. pp. 96-107.

Digital Library

[5]

Butenhof, D.R., Programming with POSIX Threads. 1997. Addison-Wesley.

Digital Library

[6]

Chung, M.-Y. and G. Ciardo, Saturation NOW, in: QEST (2004), pp. 272--281

Digital Library

[7]

Ciardo, G., Lüttgen, G. and Siminiceanu, R., Saturation: An efficient iteration strategy for symbolic state-space generation. In: LNCS, 2031. pp. 328-342.

Digital Library

[8]

Ezekiel, J., G. Lüttgen and G. Ciardo, Parallelising symbolic state-space generators, in: CAV, LNCS, 2007, to appear

Digital Library

[9]

Ezekiel, J., Lüttgen, G. and Siminiceanu, R., Can Saturation be parallelised? On the parallelisation of a symbolic state-space generator. In: LNCS, 4346. pp. 331-346.

Digital Library

[10]

Frigo, M., C.E. Leiserson and K.H. Randall, The implementation of the Cilk-5 multithreaded language, in: SIGPLAN (1998), pp. 212--223

Digital Library

[11]

Garavel, H., Mateescu, R. and Smarandache, I., Parallel state space construction for model-checking. In: LNCS, 2057. pp. 217-234.

Digital Library

[12]

Gautier, T., Roch, J.-L. and Villard, G., . In: LNCS, 980. pp. 1-25.

Digital Library

[13]

Graham, S.L., P.B. Kessler and M.K. McKusick, Gprof: A call graph execution profiler (with retrospective), in: PLDI (1982), pp. 49--57

[14]

Grama, A., Gupta, A., Karypis, G. and Kumar, V., Introduction to Parallel Computing. 2002. Addison-Wesley.

Digital Library

[15]

Achieving speedups in distributed symbolic reachability analysis through asynchronous computation. In: LNCS, 3725. pp. 129-145.

Digital Library

[16]

Grumberg, O., Heyman, T. and Schuster, A., A work-efficient distributed algorithm for reachability analysis. In: LNCS, 2725. pp. 54-66.

[17]

Gupta, A., A. Tucker and S. Urushibara, The impact of operating system scheduling policies and synchronization methods of performance of parallel applications, in: SIGMETRICS (1991), pp. 120--132

Digital Library

[18]

Heyman, T., Geist, D., Grumberg, O. and Schuster, A., Achieving scalability in parallel reachability analysis of very large circuits. In: LNCS, 1855. pp. 20-35.

Digital Library

[19]

Inggs, C.P., “Parallel Model Checking on Shared Memory Architectures,” Ph.D. thesis, University of Manchester, UK (2004)

[20]

Inggs, C.P. and Barringer, H., Effective state exploration for model checking on a shared memory architecture. ENTCS. v68 i4.

[21]

Inggs, C.P. and Barringer, H., CTL* model checking on a shared-memory architecture. FMSD. v29. 135-155.

Digital Library

[22]

Kimura, S. and E.M. Clarke, A parallel algorithm for constructing binary decision diagrams, in: ICCD (1990), pp. 220--223

[23]

Knottenbelt, W.J., Harrison, P.G., Mestern, M.A. and Kritzinger, P.S., A probabilistic dynamic technique for the distributed generation of very large state spaces. Perform. Eval. v39. 127-148.

Digital Library

[24]

Lerda, F. and Sisto, R., Distributed-memory model checking with SPIN. In: LNCS, 1680. pp. 22-39.

Digital Library

[25]

Milvang-Jensen, K. and Hu, A.J., BDDNOW: A parallel BDD package. In: LNCS, 1522. pp. 501-507.

Digital Library

[26]

Stern, U. and Dill, D.L., Parallelizing the Murφ verifier. FMSD. v18. 117-129.

Digital Library

[27]

Stornetta, T. and F. Brewer, Implementation of an efficient parallel BDD package, in: DAC (1996), pp. 641--644

Digital Library

Cited By

Ruman ÁDrašar MSadlek LYang SCeleda P(2024)Adversary Tactic Driven Scenario and Terrain Generation with Partial Infrastructure SpecificationProceedings of the 19th International Conference on Availability, Reliability and Security10.1145/3664476.3664523(1-11)Online publication date: 30-Jul-2024
https://dl.acm.org/doi/10.1145/3664476.3664523
Höfinger SHaunschmid E(2018)Modelling parallel overhead from simple run-time recordsThe Journal of Supercomputing10.1007/s11227-017-2023-973:10(4390-4406)Online publication date: 31-Dec-2018
https://dl.acm.org/doi/10.1007/s11227-017-2023-9
Gava FPommereau FGuedj M(2014)A BSP algorithm for on-the-fly checking CTL* formulas on security protocolsThe Journal of Supercomputing10.1007/s11227-014-1099-869:2(629-672)Online publication date: 1-Aug-2014
https://dl.acm.org/doi/10.1007/s11227-014-1099-8
Show More Cited By

Index Terms

Measuring and Evaluating Parallel State-Space Exploration Algorithms
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Logic
    1. Verification by model checking
  2. Models of computation
    1. Concurrency
      1. Parallel computing models

Recommendations

Metrics for evaluation of parallel efficiency toward highly parallel processing

I studied novel performance metrics of parallel processing efficiency, determined simply by measuring timing data in a parallel process. The metrics, which consider load-imbalance, are called the parallel efficiency, load-balancing, and parallel ...
Abstract state machines capture parallel algorithms: Correction and extension

We consider parallel algorithms working in sequential global time, for example, circuits or parallel random access machines (PRAMs). Parallel abstract state machines (parallel ASMs) are such parallel algorithms, and the parallel ASM thesis asserts that ...
Sequential and Parallel Algorithms for the State Space Exploration

AbstractIn this article, we are interested in the exploration part of model checking which consists in traversing all the possible states of a system. We propose two approaches to exploration, parallel and sequential. We present a comparison between our ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Electronic Notes in Theoretical Computer Science (ENTCS)

Electronic Notes in Theoretical Computer Science (ENTCS) Volume 198, Issue 1

February, 2008

96 pages

ISSN:1571-0661

Issue’s Table of Contents

Copyright © © 2008.

Publisher

Elsevier Science Publishers B. V.

Netherlands

Publication History

Published: 01 February 2008

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 16 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Ruman ÁDrašar MSadlek LYang SCeleda P(2024)Adversary Tactic Driven Scenario and Terrain Generation with Partial Infrastructure SpecificationProceedings of the 19th International Conference on Availability, Reliability and Security10.1145/3664476.3664523(1-11)Online publication date: 30-Jul-2024
https://dl.acm.org/doi/10.1145/3664476.3664523
Höfinger SHaunschmid E(2018)Modelling parallel overhead from simple run-time recordsThe Journal of Supercomputing10.1007/s11227-017-2023-973:10(4390-4406)Online publication date: 31-Dec-2018
https://dl.acm.org/doi/10.1007/s11227-017-2023-9
Gava FPommereau FGuedj M(2014)A BSP algorithm for on-the-fly checking CTL* formulas on security protocolsThe Journal of Supercomputing10.1007/s11227-014-1099-869:2(629-672)Online publication date: 1-Aug-2014
https://dl.acm.org/doi/10.1007/s11227-014-1099-8
Brauer JSchlich BKowalewski S(2009)Parallel and Distributed Invariant Checking of Microcontroller SoftwareElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2009.09.059254(45-63)Online publication date: 1-Oct-2009
https://dl.acm.org/doi/10.1016/j.entcs.2009.09.059

View Options

View options

Figures

Tables

Media

View Issue’s Table of Contents