This Article 
 Bibliographic References 
 Add to: 
The Design of a Multicore Extension of the SPIN Model Checker
October 2007 (vol. 33 no. 10)
pp. 659-674
We describe an extension of the SPIN model checker for use on multi-core shared-memory systems and report on its performance. We show how, with proper load balancing, the time requirements of a verification run can in some cases be reduced close to N-fold when N processing cores are used. We also analyze the types of verification problems for which multi-core algorithms cannot provide relief. The extensions discussed here require only relatively small changes in the SPIN source code, and are compatible with most existing verification modes, such as partial order reduction, the verification of temporal logic formulae, bitstate hashing, and hash-compact compression.

[1] R. Alur, R.K. Brayton, T.A. Henzinger, S. Qadeer, and S.K. Rajamani, “Partial-Order Reduction in Symbolic State-Space Exploration,” Formal Methods in System Design, vol. 18, pp. 97-116, 2001.
[2] J. Barnat, L. Brim, and J. Stribrna, “Distributed LTL Model-Checking in SPIN,” Proc. Eighth Int'l SPIN Workshop Model Checking of Software, May 2001.
[3] J. Barnat, L. Brim, and J. Chaloupka, “Parallel Breadth-First Search LTL Model Checking,” Proc. Automated Software Eng., 2003.
[4] G. Behrmann, T. Hune, and F. Vaandrager, “Distributing Timed Model Checking—How the Search Order Matters,” Proc. 12th Int'l Conf. Computer Aided Verification, pp. 216-231, 2000.
[5] D. Bosnacki and G.J. Holzmann, “Improving SPIN's Partial-Order Reduction for Breadth-First Search,” Proc. 12th Int'l SPIN Workshop, pp. 91-105, 2005.
[6] L. Brim, I. Cerna, P. Moravec, and J. Simsa, “Accepting Predecessors Are Better than Back Edges in Distributed LTL Model Checking,” Formal Methods in Computer Aided Design, pp.266-352, 2004.
[7] L. Brim, I. Cerna, P. Moravec, and J. Simsa, “Distributed Partial Order Reduction of State Spaces,” Electronic Notes in Theoretical Computer Science, vol. 128, pp. 63-74, 2005.
[8] L. Brim, I. Cerna, P. Moravec, and J. Simsa, “How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors,” Electronic Notes in Theoretical Computer Science, vol. 135, pp. 3-18, 2006.
[9] I. Cerna and R. Pelanek, “Distributed Explicit Fair Cycle Detection,” Proc. SPIN Workshop, pp. 49-73, 2003.
[10] S. Chien et al., “Using Autonomy Flight Software to Improve Science Return on Earth Observing One (EO1),” J. Aerospace Computing, Information, and Comm., Apr. 2005.
[11] E.W. Dijkstra, “Shmuel Safra's Version of Termination Detection,” EWD998, Jan. 1987.
[12] S. Edelkamp and S. Jabar, “Large-Scale Directed Model Checking LTL,” Proc. 13th Int'l SPIN Workshop, pp. 1-18, 2006.
[13] P.R. Gluck and G.J. Holzmann, “Using Spin Model Checking for Flight Software Verification,” Proc. 2002 Aerospace Conf., Mar. 2002.
[14] P. Godefroid, Partial Order Methods for the Verification of Concurrent Systems: An Approach to the State Space Explosion. Springer Verlag, 1996.
[15] G.J. Holzmann, Design and Validation of Computer Protocols. Prentice Hall, 1991.
[16] G.J. Holzmann, P. Godefroid, and D. Pirottin, “Coverage Preserving Reduction Strategies for Reachability Analysis,” Proc. 12th Int'l Conf. Protocol Specification Testing and Verification, pp. 349-363, June 1992.
[17] G.J. Holzmann and D. Peled, “An Improvement in Formal Verification,” Proc. Conf. Formal Description Techniques, Oct. 1994.
[18] G.J. Holzmann, D. Peled, and M. Yannakakis, “On Nested Depth-First Search,” The SPIN Verification System, pp. 23-32, Am. Math. Soc., 1996.
[19] G.J. Holzmann and M.H. Smith, “Automating Software Feature Verification,” Bell Labs Technical J., vol. 5, no. 2, pp. 72-87, Apr.-June 2000.
[20] G.J. Holzmann, The SPIN Model Checker—Primer and Reference Manual. Addison-Wesley, 2004.
[21] G.J. Holzmann and R. Joshi, “Model-Driven Software Verification,” Proc. 11th SPIN Workshop, pp. 77-92, Apr. 2004.
[22] G.J. Holzmann, “A Stack-Slicing Algorithm for Multi-Core Model Checking,” Proc. Sixth Int'l Workshop Parallel and Distributed Methods on Verification, July 2007.
[23] C.P. Inggs and H. Barringer, “Effective State Exploration for Model Checking on a Shared Memory Architecture,” Electronic Notes in Theoretical Computer Science, vol. 68, no. 4, 2002.
[24] C.P. Inggs and H. Barringer, “${\rm CTL}^{\ast}$ Model Checking on a Shared-Memory Architecture,” Electronic Notes in Theoretical Computer Science, vol. 128, pp. 107-123, 2005.
[25] S. Jabbar and S. Edelkamp, “Parallel External Directed Model Checker with Linear I/O,” Proc. Seventh Int'l Conf. Verification, Model Checking, and Abstract Interpretation, pp. 237-251, 2006.
[26] R. Joshi and G.J. Holzmann, “A Mini-Challenge: Build a Verifiable Filesystem,” Formal Aspects of Computing, vol. 19, 2007.
[27] R. Kumar and E.G. Mercer, “Load Balancing Parallel Explicit State Model Checking,” Proc. Third Int'l Workshop Parallel and Distributed Model Checking, Aug. 2004.
[28] R.P. Kurshan, V. Levin, M. Minea, D. Peled, and H. Yenigün, “Static Partial Order Reduction,” Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS '98), pp. 345-357, 1998.
[29] A.L. Lafuente, “Simplified Distributed LTL Model Checking by Localizing Cycles,” Technical Report 00176, Institut fur Informatik, Univ. Freiburg, Germany, July 2002.
[30] F. Lerda and R. Sisto, “Distributed-Memory Model Checking in SPIN,” Proc. SPIN Workshop, 1999.
[31] G.E. Moore, “Cramming More Components onto Integrated Circuits,” Electronics, vol. 38, pp. 114-117, 1965.
[32] D. Peled, “Combining Partial Order Reductions with On-the-Fly Model-Checking,” Proc. Conf. Computer Aided Verification (CAV '94), pp. 377-390, 1994.
[33] J. Penix, W. Visser, C. Pasareanu, E. Engstrom, A. Larson, and N. Weininger, “Verifying Time Partitioning in the DEOS Scheduling Kernel,” Formal Methods in Systems Design J., vol. 26, no. 2, Mar. 2005.
[34] G.L. Peterson, “Myths about the Mutual Exclusion Problem,” Information Processing Letters, vol. 12, no. 3, pp. 115-116, June 1981.
[35] R. Pelanek, “Typical Properties of State Spaces,” Proc. 11th SPIN Workshop, pp. 5-22, Apr. 2004.
[36] J.H. Reif, “Depth First Search Is Inherently Sequential,” Information Processing Letters, vol. 20, no. 5, pp. 229-234, June 1985.
[37] U. Stern and D. Dill, “Parallelizing the Mur$\varphi$ Verifier,” Proc. Ninth Int'l Conf. Computer Aided Verification, pp. 256-278, June 1997.
[38] A. Valmari, “The State Explosion Problem,” Lectures on Petri Nets I: Basic Models, Springer, pp. 429-528, 1998.

Index Terms:
Software/Program Verification, Model Checking, Models of Computation, Logics and meanings of Programs, Distributed Programming
Gerard J. Holzmann, Dragan Bosnacki, "The Design of a Multicore Extension of the SPIN Model Checker," IEEE Transactions on Software Engineering, vol. 33, no. 10, pp. 659-674, Oct. 2007, doi:10.1109/TSE.2007.70724
Usage of this product signifies your acceptance of the Terms of Use.