Abstract
TSO-to-SC linearizability is a variant of linearizability for concurrent libraries on the Total Store Order (TSO) memory model. In this paper we propose the notion of k-bounded TSO-to-SC linearizability, a subclass of TSO-to-SC linearizability that concerns only bounded histories. This subclass is non-trivial in that it does not restrict the number of write, flush and cas (compare-and-swap) actions, nor the size of a store buffer, to be bounded. We prove that the decision problem of k-bounded TSO-to-SC linearizability is decidable for a bounded number of processes. We first reduce this decision problem to a marked violation problem of k-bounded TSO-to-SC linearizability, where specific \(\textit{cas}\) actions are introduced to mark call and return actions. Then, we further reduce the marked violation problem to a control state reachability problem of a lossy channel machine, which is already known to be decidable. Moreover, we can show that the decision problem of k-bounded TSO-to-SC linearizability has non-primitive recursive complexity.
This work is partially supported by the National Natural Science Foundation of China under Grants No. 60721061, No. 60833001, No. 61272135, No. 61572478, No. 61700073, No. 61100069, No. 61472405, and No. 61161130530.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Alur, R., McMillan, K., Peled, D.: Model-checking of correctness conditions for concurrent objects. In: LICS 1996, pp. 219–228. IEEE Computer Society (1996)
Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. In: Hermenegildo, M., et al. (eds.) POPL 2010, pp. 7–18. ACM (2010)
Batty, M., Dodds, M., Gotsman, A.: Library abstraction for C/C++ concurrency. In: Giacobazzi, R., Cousot, R. (eds.) POPL 2013, pp. 235–248. ACM (2013)
Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Verifying concurrent programs against sequential specifications. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 290–309. Springer, Heidelberg (2013)
Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: On reducing linearizability to state reachability. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 95–107. Springer, Heidelberg (2015)
Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Tractable refinement checking for concurrent objects. In: Rajamani, S.K., et al. (eds.) POPL 2015, pp. 651–662. ACM (2015)
Burckhardt, S., Gotsman, A., Musuvathi, M., Yang, H.: Concurrent library correctness on the TSO memory model. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 87–107. Springer, Heidelberg (2012)
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)
Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463–492 (1990)
Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess program. IEEE Trans. Comput. 28(9), 690–691 (1979)
Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: Palsberg, J., Abadi, M. (eds.) POPL 2005, pp. 378–391. ACM (2005)
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)
Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: Hall, M.W., Padua, D.A. (eds.) PLDI 2011, pp. 175–186. ACM (2011)
Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity. Inf. Process. Lett. 83(5), 251–261 (2002)
Wang, C., Lv, Y., Wu, P.: Bounded TSO-to-SC linearizability is decidable. Technical report ISCAS-SKLCS-15-11, State Key Laboratory of Computer Science, ISCAS, CAS (2015). http://lcs.ios.ac.cn/~lvyi/files/ISCAS-SKLCS-15-11.pdf
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, Heidelberg (2015)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wang, C., Lv, Y., Wu, P. (2016). Bounded TSO-to-SC Linearizability Is Decidable. In: Freivalds, R., Engels, G., Catania, B. (eds) SOFSEM 2016: Theory and Practice of Computer Science. SOFSEM 2016. Lecture Notes in Computer Science(), vol 9587. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-49192-8_33
Download citation
DOI: https://doi.org/10.1007/978-3-662-49192-8_33
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-49191-1
Online ISBN: 978-3-662-49192-8
eBook Packages: Computer ScienceComputer Science (R0)