Abstract
This paper introduces VeriDAG, a verification tool for directed acyclic graphs that represent concurrent programs under memory consistency models. VeriDAG has two novel aspects. First, VeriDAG does not handle concurrent programs directly, but operates on directed acyclic graphs whose edges denote dependencies between instructions in the concurrent programs. This provides software model checking under various memory consistency models by replacing the definitions of edge connections, whereas many model checkers are specific to certain memory consistency models. Second, an engine for exploring execution traces is fully implemented in Haskell with manageable exploration strategies. In contrast, similar model checkers use external engines such as SMT solvers and model checkers that ignore relaxed memory consistency models. Thus, VeriDAG provides a research framework on which we can design new memory consistency models and apply exploration strategies for execution traces under memory consistency models. As evidence, this paper compares VeriDAG with an existing model checker, and implements reordering controls, which are heuristic searches for counterexample detection in directed model checking.
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
Abdulla, P.A., Aronis, S., Atig, M.F., Jonsson, B., Leonardsson, C., Sagonas, K.: Stateless model checking for TSO and PSO. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 353–367. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_28
Abdulla, P.A., Atig, M.F., Bouajjani, A., Ngo, T.P.: Context-bounded analysis for POWER. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 56–74. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54580-5_4
Abdulla, P.A., Atig, M.F., Jonsson, B., Leonardsson, C.: Stateless model checking for POWER. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 134–156. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_8
Abe, T., Maeda, T.: Concurrent program logic for relaxed memory consistency models with dependencies across loop iterations. Journal of Information Processing 25, 244–255 (2017)
Abe, T., Maeda, T.: A general model checking framework for various memory consistency models. International Journal on Software Tools for Technology Transfer 19(5) (2017). https://bitbucket.org/abet/mcspin/
Abe, T., Ugawa, T., Maeda, T.: Reordering control approaches to state explosion in model checking with memory consistency models. In: Proc. of VSTTE (2017)
Abe, T., Ugawa, T., Maeda, T., Matsumoto, K.: Reducing state explosion for software model checking with relaxed memory consistency models. In: Fränzle, M., Kapur, D., Zhan, N. (eds.) SETTA 2016. LNCS, vol. 9984, pp. 118–135. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47677-3_8
Adve, S.V., Gharachorloo, K.: Shared memory consistency models: A tutorial. Computer 29(12), 66–76 (1996)
Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM Transactions on Programming Languages and Systems 36(2) (2014). http://diy.inria.fr/herd/
Aravind, A.A.: Yet another simple solution for the concurrent programming control problem. IEEE Transactions on Parallel and Distributed Systems 22(6), 1056–1063 (2011)
Blom, S., van de Pol, J., Weber, M.: LTSmin: distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 354–359. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_31
Dijkstra, E.W.: Cooperating sequential processes. In: Programming Languages: NATO Advanced Study Institute, pp. 43–112. Academic Press (1968)
Edelkamp, S., Lafuente, A.L.: HSF-SPIN User Manual (2006)
Edelkamp, S., Lafuente, A.L., Leue, S.: Directed explicit model checking with HSF-SPIN. In: Dwyer, M. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 57–79. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45139-0_5
Edelkamp, S., Schuppan, V., Bošnački, D., Wijs, A., Fehnker, A., Aljazzar, H.: Survey on directed model checking. In: Peled, D.A., Wooldridge, M.J. (eds.) MoChArt 2008. LNCS (LNAI), vol. 5348, pp. 65–89. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00431-5_5
Fischer, B., Inverso, O., Parlato, G.: CSeq: A concurrency pre-processor for sequential C verification tools. In: Proc. of ASE, pp. 710–713 (2013)
Holzmann, G.J.: The SPIN Model Checker. Addison-Wesley (2003)
Lamport, L.: A new solution of Dijkstra’s concurrent programming problem. Comm. ACM 17(8), 453–455 (1974)
Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers 9, 690–691 (1979)
Lamport, L.: A fast mutual exclusion algorithm. ACM Transactions on Computer Systems 5(1), 1–11 (1987)
Leijen, D., Palamarchuk, A.: The IntMap module. https://hackage.haskell.org/package/containers-0.5.10.2/docs/Data-IntMap.html
McCloskey, B., Bacon, D.F., Cheng, P., Grove, D.: Staccato: A parallel and concurrent real-time compacting garbage collector for multiprocessors. Research Report RC24504, IBM (2008)
Nidhugg: Nidhugg Manual, Version 0.2 (2016). https://github.com/nidhugg
Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. Technical Report UCAM-CL-TR-745, Computer Laboratory, University of Cambridge (2009)
Peterson, G.L.: Myths about the mutual exclusion problem. Information Processing Letters 12(3), 115–116 (1981)
Pizlo, F., Petrank, E., Steensgaard, B.: A study of concurrent real-time garbage collectors. Proc. of PLDI, pp. 33–44 (2008)
Reffe, F., Edelkamp, S.: Error detection with directed symbolic model checking. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 195–211. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48119-2_13
Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: Proc. of PLDI, pp. 175–186 (2011)
Still, V.: LLVM transformations for model checking. Master’s thesis, Masaryk University (2016)
Štill, V., Ročkai, P., Barnat, J.: Weak memory models as LLVM-to-LLVM transformations. In: Kofroň, J., Vojnar, T. (eds.) MEMICS 2015. LNCS, vol. 9548, pp. 144–155. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-29817-7_13
Tomasco, E., Truc Nguyen Lam, O.I., Fischer, B., Torre, S.L., Parlato, G.: Lazy sequentialization for TSO and PSO via shared memory abstractions. In: Proc. of FMCAD, pp. 193–200 (2016)
Travkin, O., Wehrheim, H.: Verification of concurrent programs on weak memory models. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 3–24. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46750-4_1
Turon, A., Vafeiadis, V., Dreyer, D.: GPS: Navigating weak memory with ghosts, protocols, and separation. In: Proc. of OOPSLA, pp. 691–707 (2014)
Vafeiadis, V., Narayan, C.: Relaxed separation logic: A program logic for C11 concurrency. In: Proc. of OOPSLA, pp. 867–884 (2013)
van der Berg, F.: Model checking LLVM IR using LTSmin: Using relaxed memory model semantics. Master’s thesis. University of Twente (2013)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Abe, T. (2017). A Verifier of Directed Acyclic Graphs for Model Checking with Memory Consistency Models. In: Strichman, O., Tzoref-Brill, R. (eds) Hardware and Software: Verification and Testing. HVC 2017. Lecture Notes in Computer Science(), vol 10629. Springer, Cham. https://doi.org/10.1007/978-3-319-70389-3_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-70389-3_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-70388-6
Online ISBN: 978-3-319-70389-3
eBook Packages: Computer ScienceComputer Science (R0)