Abstract
The use of specialised approximations for reachability, instead of exact reachability, has given rise to scalable methods to verify deadlock freedom in the context of distributed finite-state systems. In this work, we extend these approaches to check static properties. These properties capture the immediate/static behaviour of a system. The static nature of these properties make them a good match for the sort of over-approximations we use. Local-deadlock freedom and mutual exclusion are two commonly desired properties for distributed systems that naturally fit into our framework. Local-deadlock freedom, in particular, specifies that no subsystem can reach a permanently blocked state. We show by a series of experiments that our approximate framework can prove such properties for a number of interesting systems, and it can do so more efficiently compared to complete approaches.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The predicate \(reach_{Pair}\) corresponds to \(pairwise\_reachable\) in [2]. This new name is introduced for uniformity.
- 2.
These predicates correspond to \(reachable^C_{N}\), \(reachable^A_{N}\), \(reachable^C_{S}\), and \(reachable^A_{S}\) in [3], respectively. This renaming is for uniformity.
- 3.
Proofs are given in reports associated to original papers.
- 4.
\(Reach_{Pair}\) corresponds to the formula Reachable in [2] where the pairs in NPR are calculated over sets \(S_i\) and \(S_j\) instead of \(RequireSync_i\) and \(RequireSync_j\). The sets \(RequireSync_i\) represent an optimisation for checking deadlock freedom that is not valid to all static properties. \(Reach_{NC}\), \(Reach_{SC}\), \(Reach_{NA}\) and \(Reach_{SA}\) correspond to formulas \(Reach^C_N\), \(Reach^C_S\), \(Reach^A_N\) and \(Reach^A_S\) in [3], respectively.
References
Antonino, P., Gibson-Robinson, T., Roscoe, A.W.: The automatic detection of token structures and invariants using SAT checking. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 249–265. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54580-5_15
Antonino, P., Gibson-Robinson, T., Roscoe, A.W.: Efficient deadlock-freedom checking using local analysis and SAT solving. In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 345–360. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33693-0_22
Antonino, P., Gibson-Robinson, T., Roscoe, A.W.: Tighter reachability criteria for deadlock-freedom analysis. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 43–59. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48989-6_3
Antonino, P., Gibson-Robinson, T., Roscoe, A.W.: Experiment package (2017). www.cs.ox.ac.uk/people/pedro.antonino/sppkg.zip
Antonino, P.R.G., Oliveira, M.M., Sampaio, A.C.A., Kristensen, K.E., Bryans, J.W.: Leadership election: an industrial SoS application of compositional deadlock verification. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 31–45. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06200-6_3
Antonino, P., Sampaio, A., Woodcock, J.: A refinement based strategy for local deadlock analysis of networks of CSP processes. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 62–77. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06410-9_5
Attie, P.C., Bensalem, S., Bozga, M., Jaber, M., Sifakis, J., Zaraket, F.A.: An abstract framework for deadlock prevention in BIP. In: Beyer, D., Boreale, M. (eds.) FMOODS/FORTE -2013. LNCS, vol. 7892, pp. 161–177. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38592-6_12
Attie, P.C., Chockler, H.: Efficiently verifiable conditions for deadlock-freedom of large concurrent programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 465–481. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30579-8_30
Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: IJCAI 2009, San Francisco, CA, USA, pp. 399–404 (2009)
Bensalem, S., Bozga, M., Legay, A., Nguyen, T.-H., Sifakis, J., Yan, R.: Component-based verification using incremental design and invariants. Softw. Syst. Model. 15(2), 427–451 (2016)
Filho, M.S.C., Oliveira, M.V.M., Sampaio, A., Cavalcanti, A.: Local livelock analysis of component-based models. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 279–295. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47846-3_18
Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 — a modern refinement checker for CSP. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187–201. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_13
Gibson-Robinson, T., Hansen, H., Roscoe, A.W., Wang, X.: Practical partial order reduction for CSP. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 188–203. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17524-9_14
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Lambertz, C., Majster-Cederbaum, M.: Analyzing component-based systems on the basis of architectural constraints. In: Arbab, F., Sirjani, M. (eds.) FSEN 2011. LNCS, vol. 7141, pp. 64–79. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29320-7_5
Martin, J.M.R.: The Design and Construction of Deadlock-Free Concurrent Systems. Ph.D. thesis, University of Buckingham (1996)
Martin, J.M.R., Jassim, S.A.: An efficient technique for deadlock analysis of large scale process networks. In: Fitzgerald, J., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol. 1313, pp. 418–441. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63533-5_22
Oliveira, M.V.M., Antonino, P., Ramos, R., Sampaio, A., Mota, A., Roscoe, A.W.: Rigorous development of component-based systems using component metadata and patterns. Formal Aspects Comput. 28(6), 937–1004 (2016). https://doi.org/10.1007/s00165-016-0375-1. ISSN:1433-299X
Ouaknine, J., Palikareva, H., Roscoe, A.W., Worrell, J.: A static analysis framework for livelock freedom in CSP. Logical Methods Comput. Sci. 9(3) September 2013. https://doi.org/10.2168/LMCS-9(3:24)2013
Raymond, K.: A tree-based algorithm for distributed mutual exclusion. ACM Trans. Comput. Syst. (TOCS) 7(1), 61–77 (1989)
Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical compression for model-checking CSP or how to check 10\(^{\text{20}}\) dining philosophers for deadlock. In: TACAS, pp. 133–152 (1995)
Roscoe, A.W.: Understanding Concurrent Systems. Springer, Heidelberg (2010)
Tarry, G.: Le probleme des labyrinthes. Nouvelles annales de mathématiques, journal des candidats aux écoles polytechnique et normale 14, 187–190 (1895)
Acknowledgements
The first author is a CAPES Foundation scholarship holder (Process no: 13201/13-1). The other authors are partially sponsored by EPSRC under agreement number EP/N022777.
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
Antonino, P., Gibson-Robinson, T., Roscoe, A.W. (2017). Checking Static Properties Using Conservative SAT Approximations for Reachability. In: Cavalheiro, S., Fiadeiro, J. (eds) Formal Methods: Foundations and Applications. SBMF 2017. Lecture Notes in Computer Science(), vol 10623. Springer, Cham. https://doi.org/10.1007/978-3-319-70848-5_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-70848-5_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-70847-8
Online ISBN: 978-3-319-70848-5
eBook Packages: Computer ScienceComputer Science (R0)