Abstract
Even if multicore architectures are nowadays extremely wide-spread, the exploitation of this easily available degree of parallelism is not always straightforward. In this paper we describe the experience gained in our ongoing effort to parallelise the model checking engine of a family of model checkers (KandISTI) developed at ISTI. The main focus of our experimentation is the evaluation of the minimal efforts needed to take advantage of our everyday multicore hardware for model checking purposes. Our early results relative to an initial fragment of the logic show a speedup factor of about 2.5 when 4 physical cores are available. This result, however, can only be achieved by complementing the initial high level Ada design with a second round of code fine-tuning which exploits nonstandard low level features in the implementation of the needed thread-safe data structures.
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
Notes
- 1.
- 2.
In our case we use the GNAT run-time component System.Atomic_Primitives.
- 3.
For all reachable nodes it is true that either the node has no outgoing {b} transitions, or the node and all its successors have at least one outgoing {a} transition.
- 4.
The data in the following tables are taken on a MacBook Pro early 2013, with a quad-core Intel Core i7-3740QM @ 2.70 GHz CPU, 16 GB RAM, running OS X El Capitan Version 10.11.3. The code has been compiled with GNAT GPL 2015 (20150428-49). Execution times computed by performing calls to Calendar.Time at the beginning/end of each evaluation. Sources, executables, models and test data are available from http://fmt.isti.cnr.it/WEBPAPER/AE2016-data.zip.
- 5.
Test executed on a eight-core workstation with a Intel(R) Xeon(R) E5-2630 v3 @ 2.40 GHz CPU, 64G RAM, running Ubuntu 14.04.4 LTS (GNULinux 3.13.0-83-generic x86_64), GNAT GPL 2015 Compiler.
References
Barnat, J., Brim, L., Leucker, M.: Parallel model checking and the FMICS-jETI platform. In: 12th International Conference on Engineering of Complex Computer Systems, ICECCS 2007, pp. 330–338. IEEE Computer Society (2007)
Barnat, J., Rockai, P.: Shared hash tables in parallel model checking. Electron. Notes Theor. Comput. Sci. 198(1), 79–91 (2008). Elseiver
Barnat, J., Ročkai, P., Štill, V., Weiser, J.: Fast, dynamically-sized concurrent hash table. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 49–65. Springer, Heidelberg (2015)
ter Beek, M.H., Gnesi, S., Mazzanti, F.: From EU projects to a family of model checkers. In: De Nicola, R., Hennicker, R. (eds.) Wirsing Festschrift. LNCS, vol. 8950, pp. 312–328. Springer, Heidelberg (2015)
ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state/event-based model- checking approach for the analysis of abstract system properties. Sci. Comput. Program. 76(2), 119–135 (2011). Elseiver
Bollig, B., Leucker, M., Weber, M.: Local parallel model checking for the alternation-free \(\mu \)-calculus. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, p. 128. Springer, Heidelberg (2002)
De Nicola, R., Vaandrager, F.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) Semantics of Systems of Concurrent Processes. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990)
Fantechi, A., Gnesi, S., Lapadula, A., Mazzanti, F., Pugliese, R., Tiezzi, F.: A logical verification methodology for service-oriented computing. ACM Trans. Softw. Eng. Methodol. 21(3), 16:1–16:45 (2012)
Gnesi, S., Mazzanti, F.: An abstract, on the fly framework for the verification of service-oriented systems. In: Wirsing, M., Hölzl, M. (eds.) SENSORIA. LNCS, vol. 6582, pp. 390–407. Springer, Heidelberg (2011)
Laarman, A, van de Pol, J, Weber, M.: Boosting multi-core reachability performance with shared hash tables. In: Formal Methods in Computer-Aided Design, Lugano, Switzerland. IEEE Computer Society (2010)
Laarman, A.: Scalable multi-core model checking. CTIT Ph.D. thesis, Formal Methods and Tools, University of Twente (2014). http://dx.doi.org/10.3990/1.9789036536561
Mazzanti, F., Spagnolo, G.O., Della Longa, S., Ferrari, A.: Deadlock avoidance in train scheduling: a model checking approach. In: Lang, F., Flammini, F. (eds.) FMICS 2014. LNCS, vol. 8718, pp. 109–123. Springer, Heidelberg (2014)
Mazzanti, F., Spagnolo, G.O., Ferrari, A.: Designing a deadlock-free train scheduler: a model checking approach. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 264–269. Springer, Heidelberg (2014)
Saad, R.T., Zilio, S.D., Berthomieu, B.: A general lock-free algorithm for parallel state space construction. In: 9th International Workshop on Parallel and Distributed Methods in Verification (PDMC 2010). IEEE (2010)
Saad, R.T., Dal Zilio, S., Berthomieu, B.: An experiment on parallel model checking of a CTL fragment. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 284–299. Springer, Heidelberg (2012)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Mazzanti, F. (2016). An Experience in Ada Multicore Programming: Parallelisation of a Model Checking Engine. In: Bertogna, M., Pinho, L., Quiñones, E. (eds) Reliable Software Technologies – Ada-Europe 2016. Ada-Europe 2016. Lecture Notes in Computer Science(), vol 9695. Springer, Cham. https://doi.org/10.1007/978-3-319-39083-3_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-39083-3_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-39082-6
Online ISBN: 978-3-319-39083-3
eBook Packages: Computer ScienceComputer Science (R0)