×

zbMATH — the first resource for mathematics

Parameterized model checking on the TSO weak memory model. (English) Zbl 07268904
Summary: We present an extended version of the model checking modulo theories framework for verifying parameterized systems under the TSO weak memory model. Our extension relies on three main ingredients: (1) an axiomatic theory of the TSO memory model based on relations over (read, write) events, (2) a TSO-specific backward reachability algorithm and (3) an SMT solver for reasoning about TSO formulas. One of the main originality of our work is a partial order reduction technique that exploits specificities of the TSO memory model. We have implemented this framework in a new version of the Cubicle model checker called Cubicle-\( \mathscr{W} \). Our experiments show that Cubicle-\( \mathscr{W}\) is expressive and efficient enough to automatically prove safety of concurrent algorithms, for an arbitrary number of processes, ranging from mutual exclusion to synchronization barriers translated from actual x86-TSO implementations.
MSC:
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Software:
Cubicle; Mcmt; Memorax
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: The benefits of duality in verifying concurrent programs under TSO. In: 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada, pp. 5:1-5:15 (2016) · Zbl 1392.68142
[2] Abdulla, P.A., Atig, M.F., Chen, Y., Leonardsson, C., Rezine, A.: Memorax, a precise and sound tool for automatic fence insertion under TSO. In: 19th International Conference Tools and Algorithms for the Construction and Analysis of Systems—TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, pp. 530-536 (2013)
[3] Abdulla, P.A., Delzanno, G., Henda, N.B., Rezine, A.: Regular model checking without transducers (on efficient verification of parameterized systems). In: 13th International Conference Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24-April 1, 2007, Proceedings, pp. 721-736 (2007) · Zbl 1186.68312
[4] Abdulla, P.A., Delzanno, G., Rezine, A.: Parameterized verification of infinite-state processes with global conditions. In: 19th International Conference on Computer Aided Verification, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings, pp. 145-157 (2007) · Zbl 1135.68461
[5] Alglave, J.: A Shared Memory Poetics. Ph.D. thesis, University of Paris 7 - Denis Diderot, Paris, France (2010)
[6] Alglave, J., Fox, A.C.J., Ishtiaq, S., Myreen, M.O., Sarkar, S., Sewell, P., Nardelli, F.Z.: The semantics of power and ARM multiprocessor machine code. In: Proceedings of the POPL 2009 Workshop on Declarative Aspects of Multicore Programming, DAMP 2009, Savannah, GA, USA, January 20, 2009, pp. 13-24 (2009)
[7] Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software verification for weak memory via program transformation. In: Programming Languages and Systems—22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, pp. 512-532 (2013) · Zbl 1381.68143
[8] Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: 25th International Conference on Computer Aided Verification—CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, pp. 141-157 (2013)
[9] Alglave, J.; Maranget, L.; Tautschnig, M., Herding cats: modelling, simulation, testing, and data mining for weak memory, ACM Trans. Program. Lang. Syst., 36, 2, 7:1-7:74 (2014)
[10] Apt, KR; Kozen, D., Limits for automatic verification of finite-state concurrent systems, Inf. Process. Lett., 22, 6, 307-309 (1986)
[11] Bouajjani, A., Calin, G., Derevenetc, E., Meyer, R.: Lazy TSO reachability. In: Fundamental Approaches to Software Engineering—18th International Conference, FASE 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings, pp. 267-282 (2015)
[12] Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Programming Languages and Systems—22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, pp. 533-553 (2013) · Zbl 1381.68039
[13] Clarke, E.M., Grumberg, O., Browne, M.C.: Reasoning about networks with many identical finite-state processes. In: Proceedings of the Fifth Annual ACM Symposium on Principles of Distributed Computing, Calgary, Alberta, Canada, August 11-13, 1986, pp. 240-248 (1986) · Zbl 0709.68610
[14] Conchon, S., Declerck, D., Zaïdi, F.: Cubicle-\( \cal{W} \): parameterized model checking on weak memory. In: 9th International Joint Conference System Descriptions—IJCAR 2018, Oxford, United Kingdom, July 14-17, 2018, Proceedings (2018) · Zbl 06958097
[15] Conchon, S., Goel, A., Krstic, S., Mebsout, A., Zaïdi, F.: Invariants for finite instances and beyond. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013, pp. 61-68 (2013)
[16] Conchon, S., Goel, A., Krstic, S., Mebsout, A., Zaïdi, F.: Cubicle: a parallel SMT-based model checker for parameterized systems—tool paper. In: 24th International Conference on Computer Aided Verification, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, pp. 718-724 (2012)
[17] Conchon, S., Mebsout, A., Zaïdi, F.: Certificates for parameterized model checking. In: FM 2015: Formal Methods in 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings, pp. 126-142 (2015)
[18] Cubicle-\( \cal W\it \). http://cubicle.lri.fr/cubiclew/
[19] German, SM; Sistla, AP, Reasoning about systems with many processes, J. ACM, 39, 3, 675-735 (1992) · Zbl 0799.68078
[20] Ghilardi, S., Ranise, S.: Backward reachability of array-based systems by SMT solving: termination and invariant synthesis. LMCS 6(4) (2010) · Zbl 1213.68379
[21] Ghilardi, S., Ranise, S.: MCMT: a model checker modulo theories. In: 5th International Joint Conference Automated Reasoning, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings, pp. 22-29 (2010) · Zbl 1291.68257
[22] Goeman, HJM, The arbiter: an active system component for implementing synchronizing primitives, Fundam. Inform., 4, 517-530 (1981) · Zbl 0487.68008
[23] Herlihy, M.; Shavit, N., The Art of Multiprocessor Programming (2008), Burlington: Morgan Kaufmann, Burlington
[24] Lamport, L., How to make a multiprocessor computer that correctly executes multiprocess programs, IEEE Trans. Comput., 28, 9, 690-691 (1979) · Zbl 0419.68045
[25] Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: 22nd International Conference Theorem Proving in Higher Order Logics, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 391-407 (2009)
[26] Sewell, P.; Sarkar, S.; Owens, S.; Nardelli, FZ; Myreen, MO, x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors, Commun. ACM, 53, 7, 89-97 (2010)
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.