×

Vector symmetry reduction. (English) Zbl 1335.68134

Miller, Alice (ed.) et al., Proceedings of the 8th international workshop on automated verification of critical systems (AVoCS 2008), Glasgow, UK, September 30 – October 1, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 250, No. 2, 3-18 (2009).
Summary: Symmetry reduction is an effective state-space reduction technique for model checking, and works by restricting search to equivalence class representatives with respect to a group of symmetries for a model. A major problem with symmetry reduction techniques is the time taken to compute the representative of a state, which can be prohibitive. In efficient implementations of symmetry reduction, a symmetry is applied to a state as a sequence of operations which swap component identities. We show that vector processing technology, common to modern computers, can be used to implement a vectorised swap operation, which can be incorporated into the representative computation algorithm to accelerate symmetry reduction. Via a worked example, we present details of this vector symmetry reduction method. We have implemented our techniques in the TopSpin symmetry reduction package for the Spin model checker, and present experimental results showing the speedups obtained via vectorisation for two case-studies running on a PowerPC vector processor.
For the entire collection see [Zbl 1281.68035].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)

Software:

SPIN; TopSpin; SymmSpin
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bosnacki, D.; Dams, D.; Holenderski, L., Symmetric Spin, STTT, 4, 1, 92-106 (2002)
[2] Calder, M.; Miller, A., Generalising feature interactions in email, (Amyot, D.; Logrippo, L., Proceedings of FIW 2003 (2003), IOS Press), 187-204
[3] Clarke, E. M.; Emerson, E. A.; Jha, S.; Sistla, A. P., Symmetry reductions in model checking, (Hu, A. J.; Vardi, M. Y., Proceedings of CAV 1998. Proceedings of CAV 1998, LNCS, volume 1427 (1998), Springer), 147-158
[4] Clarke, E. M.; Jha, S.; Enders, R.; Filkorn, T., Exploiting symmetry in temporal logic model checking, Formal Methods in System Design, 9, 1/2, 77-104 (1996)
[5] Clarke, E.; Grumberg, O.; Peled, D., Model Checking (1999), The MIT Press
[6] Donaldson, A. F.; Miller, A., Automatic symmetry detection for model checking using computational group theory, (Fitzgerald, J.; Hayes, I. J.; Tarlecki, A., Proceedings of FM 2005. Proceedings of FM 2005, LNCS, volume 3582 (2005), Springer), 481-496 · Zbl 1120.68414
[7] Donaldson, A. F.; Miller, A., A computational group theoretic symmetry reduction package for the SPIN model checker, (Johnson, M.; Vene, V., Proceedings of AMAST 2006. Proceedings of AMAST 2006, LNCS, volume 4019 (2006), Springer), 374-380
[8] Donaldson, A. F.; Miller, A., Exact and approximate strategies for symmetry reduction in model checking, (Misra, J.; Nipkow, T., Proceedings of FM 2006. Proceedings of FM 2006, LNCS, volume 4085 (2006), Springer), 541-556
[9] A.F. Donaldson and A. Miller. Extending symmetry reduction techniques to a realistic model of computation. Electr. Notes Theor. Comput. Sci; A.F. Donaldson and A. Miller. Extending symmetry reduction techniques to a realistic model of computation. Electr. Notes Theor. Comput. Sci · Zbl 1335.68135
[10] Emerson, E. A.; Sistla, A. P., Symmetry and model checking, Formal Methods in System Design, 9, 1/2, 105-131 (1996)
[11] Emerson, E. A.; Trefler, R. J., From asymmetry to full symmetry: New techniques for symmetry reduction in model checking, (Pierre, L.; Kropf, T., Proceedings of CHARME 1999. Proceedings of CHARME 1999, LNCS, volume 1703 (1999), Springer), 142-156 · Zbl 0957.68067
[12] Emerson, E. A.; Wahl, T., On combining symmetry reduction and symbolic representation for efficient model checking, (Geist, D.; Tronci, E., Proceedings of CHARME 2003. Proceedings of CHARME 2003, LNCS, volume 2860 (2003), Springer), 216-230 · Zbl 1179.68082
[13] Emerson, E. A.; Wahl, T., Dynamic symmetry reduction, (Halbwachs, N.; Zuck, L. D., Proceedings of TACAS 2005. Proceedings of TACAS 2005, LNCS, volume 3440 (2005), Springer), 382-396 · Zbl 1087.68587
[14] Freescale Semiconductor. AltiVechttp://www.freescale.com/altivec/; Freescale Semiconductor. AltiVechttp://www.freescale.com/altivec/
[15] Herstein, I., Topics in Algebra (1975), John Wiley & Sons · Zbl 1230.00004
[16] Hofstee, H. P., Power efficient processor architecture and the Cell processor, (Procedings of HPCA 2005 (2005), IEEE Computer Society), 258-262
[17] Holzmann, G. J., The SPIN Model Checker: Primer and Reference Manual (2003), Addison-Wesley
[18] Holzmann, G. J.; Bosnacki, D., The design of a multicore extension of the SPIN model checker, IEEE Trans. Software Eng., 33, 10, 659-674 (2007)
[19] Ip, C. N.; Dill, D. L., Better verification through symmetry, Formal Methods in System Design, 9, 1/2, 41-75 (1996)
[20] Kernighan, B. W.; Ritchie, D., The C Programming Language (1988), Prentice Hall
[21] Miller, A.; Donaldson, A. F.; Calder, M., Symmetry in temporal logic model checking, ACM Comput. Surv., 38, 3 (2006), Article 8
[22] Rangarajan, M.; Dajani-Brown, S.; Schloegel, K.; Cofer, D. D., Analysis of distributed Spin applied to industrial-scale models, (Graf, S.; Mounier, L., Proceedings of SPIN 2004. Proceedings of SPIN 2004, LNCS, volume 2989 (2004), Springer), 267-285 · Zbl 1125.68373
[23] Sistla, A. P.; Gyuris, V.; Emerson, E. A., SMC: a symmetry-based model checker for verification of safety and liveness properties, ACM Trans. Softw. Eng. Methodol., 9, 2, 133-166 (2000)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.