Abstract
Architectural imperatives due to the slowing of Moore’s Law, the broad acceptance of relaxed semantics and the O(n!) worst case verification complexity of generating sequential histories motivate a new approach to concurrent correctness. Quantifiability is proposed as a novel correctness condition that models a system in vector space to launch a new mathematical analysis of concurrency. Analysis is facilitated with linear algebra, better supported and of much more efficient time complexity than traditional combinatorial methods. In this paper, we design and implement a quantifiable stack (QStack) and queue (QQueue) and present results showing that quantifiable data structures are highly scalable through use of relaxed semantics, an explicit implementation trade-off permitted by quantifiability. We present a technique for proving that a data structure is quantifiable and apply this technique to show that the QStack is quantifiably correct.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Afek, Y., Korland, G., Yanovsky, E.: Quasi-linearizability: relaxed consistency for improved concurrency. In: Lu, C., Masuzawa, T., Mosbah, M. (eds.) OPODIS 2010. LNCS, vol. 6490, pp. 395–410. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17653-1_29
Aspnes, J., Herlihy, M., Shavit, N.: Counting networks. J. ACM (JACM) 41(5), 1020–1048 (1994)
Bar-Nissan, G., Hendler, D., Suissa, A.: A dynamic elimination-combining stack algorithm. In: Fernàndez Anta, A., Lipari, G., Roy, M. (eds.) OPODIS 2011. LNCS, vol. 7109, pp. 544–561. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25873-2_37
Beman Dawes, D.A., Rivera, R.: Boost C++ libraries, December 2018. https://www.boost.org/users/history/version_1_69_0.html. Accessed 15 Jan 2019
Best, E., Randell, B.: A formal model of atomicity in asynchronous systems. Acta Inform. 16(1), 93–124 (1981)
Castañeda, A., Rajsbaum, S., Raynal, M.: Unifying concurrent objects and distributed tasks: interval-linearizability. J. ACM (JACM) 65(6), 1–42 (2018)
Chockler, G., Lynch, N., Mitra, S., Tauber, J.: Proving atomicity: an assertional approach. In: Fraigniaud, P. (ed.) DISC 2005. LNCS, vol. 3724, pp. 152–168. Springer, Heidelberg (2005). https://doi.org/10.1007/11561927_13
Cook, V., Peterson, C., Painter, Z., Dechev, D.: Quantifiability: correctness of concurrent programs in vector space. In: 29th Euromicro International Conference on Parallel, Distributed and Network-Based Processing (2021)
Guttag, J.V., Horowitz, E., Musser, D.R.: Abstract data types and software validation. Commun. ACM 21(12), 1048–1064 (1978)
Haas, A.: Fast concurrent data structures through timestamping. Ph.D. thesis, University of Salzburg, Salzburg, Austria (2015)
Hendler, D., Shavit, N., Yerushalmi, L.: A scalable lock-free stack algorithm. In: Proceedings of the Sixteenth Annual ACM Symposium on Parallelism in Algorithms and Architectures, SPAA 2004, pp. 206–215. ACM, New York (2004)
Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann (2012). Revised Reprint. ISBN 0123973375
Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. (TOPLAS) 12(3), 463–492 (1990)
Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463–492 (1990)
Hoare, C.A.R.: Proof of correctness of data representations. In: Programming Methodology, pp. 269–281. Springer, New York (1978)
Kirsch, C.M., Lippautz, M., Payer, H.: Fast and scalable, lock-free k-FIFO queues. In: Malyshkin, V. (ed.) PaCT 2013. LNCS, vol. 7979, pp. 208–223. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39958-9_18
Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess program. IEEE Trans. Comput. 28(9), 690–691 (1979)
Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18(12), 717–721 (1975)
Michael, M.M., Scott, M.L.: Simple, fast, and practical Non-Blocking and blocking concurrent queue algorithms. Technical Report 600 (1995)
Michael, M.M., Scott, M.L.: Nonblocking algorithms and preemption-safe locking on multiprogrammed shared memory multiprocessors. J. Parallel Distrib. Comput. 51(1), 1–26 (1998)
Morrison, A., Afek, Y.: Fast concurrent queues for x86 processors. In: Proceedings of the 18th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (2013)
Papadimitriou, C.H.: The serializability of concurrent database updates. J. ACM (JACM) 26(4), 631–653 (1979)
Peterson, C., Cook, V., Dechev, D.: Concurrent correctness in vector space. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) VMCAI 2021. LNCS, vol. 12597, pp. 151–173. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-67067-2_8
Rihani, H., Sanders, P., Dementiev, R.: Brief announcement: multiqueues: simple relaxed concurrent priority queues. In: Proceedings of the 27th ACM Symposium on Parallelism in Algorithms and Architectures, SPAA 2015, pp. 80–82. ACM, New York (2015). https://doi.org/10.1145/2755573.2755616. http://doi.acm.org/10.1145/2755573.2755616
Scherer, W.N., Scott, M.L.: Nonblocking concurrent data structures with condition synchronization. In: Guerraoui, R. (ed.) DISC 2004. LNCS, vol. 3274, pp. 174–187. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30186-8_13
Treiber, R.K.: Systems programming: coping with parallelism. International Business Machines Incorporated, Thomas J. Watson Research Center, New York (1986)
Wing, J.M.: Verifying atomic data types. Int. J. Parallel Prog. 18(5), 315–357 (1989)
Yang, C.: Fast wait free queue, October 2018. https://github.com/chaoran/fast-wait-free-queue. Accessed 5 Feb 2019
Yang, C., Mellor-Crummey, J.: A wait-free queue as fast as fetch-and-add. In: Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming - PPoPP 2016, pp. 1–13. ACM Press, New York (2016)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Cook, V., Peterson, C., Painter, Z., Dechev, D. (2021). Design and Implementation of Highly Scalable Quantifiable Data Structures. In: Malyshkin, V. (eds) Parallel Computing Technologies. PaCT 2021. Lecture Notes in Computer Science(), vol 12942. Springer, Cham. https://doi.org/10.1007/978-3-030-86359-3_28
Download citation
DOI: https://doi.org/10.1007/978-3-030-86359-3_28
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-86358-6
Online ISBN: 978-3-030-86359-3
eBook Packages: Computer ScienceComputer Science (R0)