×

Verifying linearizability with hindsight. (English) Zbl 1315.68068

Proceedings of the 29th annual ACM SIGACT-SIGOPS symposium on principles of distributed computing, PODC ’10, Zurich, Switzerland, July 25–28, 2010. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-60558-888-9). 85-94 (2010).

MSC:

68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68W10 Parallel algorithms in computer science

Software:

CCSTM
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] J. Bobba, K. E. Moore, H. Volos, L. Yen, M. D. Hill, M. M. Swift, and D. A. Wood. Performance pathologies in hardware transactional memory. In ISCA 07: Pro­ceedings of the 34th Annual International Symposium on Computer Architecture, pages 81 91, New York, NY, USA, 2007. ACM.
[2] N. G. Bronson, J. Casper, H. Cha., and K. Olukotun. A practical concurrent binary search tree. In PPoPP 10: Proceedings of the 15th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pages 257 268, New York, NY, USA, January 2010. ACM.
[3] N. G. Bronson, H. Cha., and K. Olukotun. CCSTM: A library-based STM for Scala. In The First Annual Scala Workshop at Scala Days 2010, April 2010.
[4] B. D. Carlstrom, A. McDonald, M. Carbin, C. Kozyrakis, and K. Olukotun. Transactional collection classes. In PPoPP 07: Proceedings of the 12th ACM SIGPLAN Sym­posium on Principles and Practice of Parallel Program­ming, pages 56 67, New York, NY, USA, 2007. ACM.
[5] C. Cascaval, C. Blundell, M. Michael, H. W. Cain, P. Wu, S. Chiras, and S. Chatterjee. Software transactional mem­ory: Why is it only a research toy? Queue, 6(5):46 58, 2008.
[6] D. Dice, O. Shalev, and N. Shavit. Transactional locking II. In DISC 06: Proceedings of the 20th International Symposium on Distributed Computing, pages 194 208. Springer, March 2006.
[7] A. Dragojevi\'{}c, R. Guerraoui, and M. Kapalka. Stretching transactional memory. In PLDI 09: Proceedings of the 2009 ACM SIGPLAN conference on Programming lan­guage design and implementation, pages 155 165, New York, NY, USA, 2009. ACM.
[8] P. Felber, V. Gramoli, and R. Guerraoui. Elastic trans­actions. In DISC 09: Proceedings of the 23rd Interna­tional Symposium on Distributed Computing, pages 93 107. Springer, 2009. · Zbl 1261.68024
[9] R. Guerraoui, M. Herlihy, and B. Pochon. Toward a the­ory of transactional contention managers. In PODC 05: Proceedings of the 24th Annual ACM Symposium on Prin­ciples of Distributed Computing, pages 258 264, New York, NY, USA, 2005. ACM. · Zbl 1314.68088
[10] R. Guerraoui and M. Kapalka. On the correctness of trans­actional memory. In PPoPP 08: Proceedings of the 13th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pages 175 184, New York, NY, USA, 2008. ACM.
[11] T. Harris, S. Marlow, S. Peyton-Jones, and M. Herlihy. Composable memory transactions. In PPoPP 05: Proceed­ings of the tenth ACM SIGPLAN Symposium on Princi­ples and Practice of Parallel Programming, pages 48 60, New York, NY, USA, 2005. ACM.
[12] T. Harris and S. Stipic. Abstract nested transactions. In TRANSACT 07: 2nd Workshop on Transactional Com­puting, August 2007.
[13] M. Herlihy and E. Koskinen. Transactional Boosting: A methodology for highly-concurrent transactional objects. In PPoPP 08: Proceedings of the 13th ACM SIGPLAN Sym­posium on Principles and Practice of Parallel Program­ming, pages 207 216, New York, NY, USA, 2008. ACM.
[14] M. Herlihy, Y. Lev, V. Luchangco, and N. Shavit. A prov­ably correct scalable concurrent skip list. In OPODIS 06: Proceedings of the 10th International Conference On Prin­ciples Of Distributed Systems, December 2006.
[15] M. Herlihy, V. Luchangco, M. Moir, and W. N. Scherer, III. Software transactional memory for dynamic-sized data structures. In PODC 03: Proceedings of the 22nd Annual Symposium on Principles of Distributed Computing, pages 92 101, New York, NY, USA, 2003. ACM.
[16] M. Herlihy and N. Shavit. The Art of Multiprocessor Pro­gramming. Morgan Kaufmann, San Francisco, CA, USA, 2008.
[17] B. Hindman and D. Grossman. Atomicity via source-to­source translation. In MSPC 06: Proceedings of the 2006 Workshop on Memory System Performance and Correct­ness, pages 82 91, New York, NY, USA, 2006. ACM.
[18] M. Kulkarni, K. Pingali, B. Walter, G. Ramanarayanan, K. Bala, and L. P. Chew. Optimistic parallelism requires abstractions. In PLDI 07: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 211 222, New York, NY, USA, 2007. ACM.
[19] D. Lea. Concurrent hash map in JSR 166 concurrency util­ ities. http://gee.cs.oswego.edu/dl/ concurrency-interest/index.html, December 2007.
[20] M. M. Michael. Hazard Pointers: Safe memory reclama­tion for lock-free objects. IEEE Transactions on Parallel Distributed Systems, 15(6):491 504, 2004.
[21] J. E. B. Moss. Open nested transactions: Semantics and support. In Poster at the 4th Workshop on Memory Per­formance Issues (WMPI-2006). February 2006.
[22] Y. Ni, V. S. Menon, A.-R. Adl-Tabatabai, A. L. Hosking, R. L. Hudson, J. E. B. Moss, B. Saha, and T. Shpeisman. Open nesting in software transactional memory. In PPoPP 07: Proceedings of the 12th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pages 68 78, New York, NY, USA, 2007. ACM Press.
[23] B. Saha, A.-R. Adl-Tabatabai, R. L. Hudson, C. Cao Minh, and B. Hertzberg. McRT STM: A high performance software transactional memory system for a multi-core runtime. In PPoPP 06: Proceedings of the 11th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pages 187 197, New York, NY, USA, March 2006. ACM Press.
[24] N. Shavit and D. Touitou. Software transactional mem­ory. In PODC 95: Proceedings of the 14th Annual ACM Symposium on Principles of Distributed Computing, pages 204 213, New York, NY, USA, 1995. ACM. · Zbl 1373.68178
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.