Abstract
Symbolic state-space generators are notoriously hard to parallelise. However, the Saturation algorithm implemented in the SMART verification tool differs from other sequential symbolic state-space generators in that it exploits the locality of firing events in asynchronous system models.
This paper explores whether event locality can be utilised to efficiently parallelise Saturation on shared-memory architectures. Conceptually, we propose to parallelise the firing of events within a decision diagram node, which is technically realised via a thread pool. We discuss the challenges involved in our parallel design and conduct experimental studies on its prototypical implementation. On a dual-processor dual-core PC, our studies show speed-ups for several example models, e.g., of up to 50% for a Kanban model, when compared to running our algorithm only on a single core.
Research funding was provided by the EPSRC under grant GR/S86211/01.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Chung, M.-Y., Ciardo, G.: A dynamic firing speculation to speedup distributed symbolic state-space generation. In: IPDPS, IEEE Computer Society Press, Los Alamitos (2006)
Chung, M.-Y., Ciardo, G.: Saturation NOW. In: QEST, pp. 272–281. IEEE Computer Society Press, Los Alamitos (2004)
Ciardo, G., Jones, R., Miner, A., Siminiceanu, R.: SMART: Stochastic model analyzer for reliability and timing. In: Tools of Measurement, Modelling and Evaluation of Computer-Communication Systems, pp. 29–34 (2001)
Ciardo, G., Lüttgen, G., Siminiceanu, R.: Saturation: An efficient iteration strategy for symbolic state-space generation. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, pp. 328–342. Springer, Heidelberg (2001)
Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NUSMV: A new symbolic model checker. STTT 2(4), 410–425 (2000)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Graham, S.L., Kessler, P.B., McKusick, M.K.: gprof: A call graph execution profiler (with retrospective). In: Best of PLDI, pp. 49–57. ACM Press, New York (1982)
Grumberg, O., Heyman, T., Ifergan, N., Schuster, A.: Achieving speedups in distributed symbolic reachability analysis through asynchronous computation. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 129–145. Springer, Heidelberg (2005)
Grumberg, O., Heyman, T., Schuster, A.: A work-efficient distributed algorithm for reachability analysis. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 54–66. Springer, Heidelberg (2003)
Heyman, T., Geist, D., Grumberg, O., Schuster, A.: Achieving scalability in parallel reachability analysis of very large circuits. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 20–35. Springer, Heidelberg (2000)
Inggs, C.P.: Parallel Model Checking On Shared Memory Architectures. PhD thesis, University of Manchester, UK (2004)
Kam, T., Villa, T., Brayton, R., S.-Vincentelli, A.L.: Multi-valued decision diagrams: Theory and applications. Multiple-Valued Logic 4(1-2), 9–62 (1998)
Lewis, B., Berg, D.J.: Multithreaded programming with Pthreads. Prentice-Hall, Englewood Cliffs (1998)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)
Milvang-Jensen, K., Hu, A.J.: BDDNOW: A parallel BDD package. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 501–507. Springer, Heidelberg (1998)
Stornetta, T., Brewer, F.: Implementation of an efficient parallel BDD package. In: DAC, pp. 641–644. ACM Press, New York (1996)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Ezekiel, J., Lüttgen, G., Siminiceanu, R. (2007). Can Saturation Be Parallelised? . In: Brim, L., Haverkort, B., Leucker, M., van de Pol, J. (eds) Formal Methods: Applications and Technology. PDMC 2006. Lecture Notes in Computer Science, vol 4346. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70952-7_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-70952-7_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70951-0
Online ISBN: 978-3-540-70952-7
eBook Packages: Computer ScienceComputer Science (R0)