Abstract
An important property of concurrent objects is whether they support progress – a special case of liveness – guarantees, which ensure the termination of individual method calls under system fairness assumptions. Liveness properties have been proposed for concurrent objects. Typical liveness properties include lock-freedom, wait-freedom, deadlock-freedom, starvation-freedom and obstruction-freedom. It is known that the five liveness properties above are decidable on the Sequential Consistency (SC) memory model for a bounded number of processes. However, the problem of decidability of liveness for finite state concurrent programs running on relaxed memory models remains open. In this paper we address this problem for the Total Store Order (TSO) memory model, as found in the x86 architecture. We prove that lock-freedom, wait-freedom, deadlock-freedom and starvation-freedom are undecidable on TSO for a bounded number of processes, while obstruction-freedom is decidable.
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
Similar content being viewed by others
References
Abdulla, P.A., Atig, M.F., Bouajjani, A., Derevenetc, E., Leonardsson, C., Meyer, R.: On the state reachability problem for concurrent programs under power. In: Georgiou, C., Majumdar, R. (eds.) NETYS 2020. LNCS, vol. 12129, pp. 47–59. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-67087-0_4
Abdulla, P.A., Jonsson, B.: Undecidable verification problems for programs with unreliable channels. Inf. Comput. 130(1), 71–90 (1996)
Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: Manuel, V., Hermenegildo., Palsberg, J. (eds.) Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, 17–23 January 2010, pp. 7–18. ACM (2010)
Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: Ball, T., Sagiv, M. (eds.) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, 26–28 January 2011, pp. 55–66. ACM (2011)
Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 533–553. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_29
Burckhardt, S., Gotsman, A., Musuvathi, M., Yang, H.: Concurrent library correctness on the TSO memory model. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 87–107. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28869-2_5
Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer (2018). https://doi.org/10.1007/978-3-319-10575-8
Intel Corporation. Intel 64 and IA-32 Architectures Software Developer’s Manual (2021)
Derrick, J., Smith, G., Dongol, B.: Verifying linearizability on TSO architectures. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 341–356. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10181-1_21
Gotsman, A., Musuvathi, M., Yang, H.: Show no weakness: sequentially consistent specifications of TSO libraries. In: Aguilera, M.K. (ed.) DISC 2012. LNCS, vol. 7611, pp. 31–45. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33651-5_3
Herlihy, M., Shavit, N.: The art of multiprocessor programming. Morgan Kaufmann (2008)
Lahav, O., Namakonov, E., Oberhauser, J., Podkopaev, A., Viktor, V.: Making weak memory models fair. CoRR, arXiv preprint arXiv2012.01067 (2020)
Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690–691 (1979)
Leijen, D., Schulte, W., Sebastian, B.: The design of a task parallel library. In: Arora, Shail., Leavens, G.T. (eds.) Proceedings of the 24th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2009, 25–29 October 2009, Orlando, Florida, USA, pp. 227–242. ACM (2009)
Liang, H., Hoffmann, J., Feng, X., Shao, Z.: Characterizing progress properties of concurrent objects via contextual refinements. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 227–241. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40184-8_17
ARM Limited. ARM Architecture Reference Manual ARMv8 (2013)
Manson, J., Pugh, W., Adve, S.V.: The java memory model. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, 12–14 January 2005, pp. 378–391. ACM (2005)
Michael, M.M., Vechev, M.T., Saraswat, V.A.: Idempotent work stealing. In: Reed, D.A., Sarkar, V. (eds.) Proceedings of the 14th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2009, Raleigh, NC, USA, 14–18 February 2009, pp. 45–54. ACM (2009)
Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 391–407. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_27
Petrank, E., Musuvathi, M., Steensgaard, B.: Progress guarantee for parallel programs via bounded lock-freedom. In: Hind, M., Diwan, A. (eds.) Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, Dublin, Ireland, 15–21 June 2009, pp. 144–154. ACM (2009)
Post, E.L.: A variant of a recursively unsolvable problem. Bull. Am. Math. Soc. 52(1946), 264–268 (1946)
Ruohonen, K.: On some variants of post’s correspondence problem. Acta Inf. 19, 357–367 (1983)
Wang, C., Lv, Y., Wu, P.: TSO-to-TSO linearizability is undecidable. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 309–325. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24953-7_24
Wang, C., Lv, Y., Wu, P., Jia., Q.: Decidability of bounded linearizability on TSO memory model. Technical Report ISCAS-SKLCS-21-01, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences (2021). http://lcs.ios.ac.cn/~lvyi/files/ISCAS-SKLCS-21-01.pdf
Wang, C., Petri, G., Lv, Y., Long, T., Liu., Z.: Decidability of liveness for concurrent objects on the TSO memory model. Technical Report ISCAS-SKLCS-22-02, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences (2021). http://lcs.ios.ac.cn/~lvyi/files/ISCAS-SKLCS-22-02.pdf
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Wang, C., Petri, G., Lv, Y., Long, T., Liu, Z. (2022). Decidability of Liveness for Concurrent Objects on the TSO Memory Model. In: Dong, W., Talpin, JP. (eds) Dependable Software Engineering. Theories, Tools, and Applications. SETTA 2022. Lecture Notes in Computer Science, vol 13649. Springer, Cham. https://doi.org/10.1007/978-3-031-21213-0_10
Download citation
DOI: https://doi.org/10.1007/978-3-031-21213-0_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-21212-3
Online ISBN: 978-3-031-21213-0
eBook Packages: Computer ScienceComputer Science (R0)