Document Open Access Logo

Relaxed Linear References for Lock-free Data Structures

Authors Elias Castegren, Tobias Wrigstad

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2017.6.pdf
  • Filesize: 1.64 MB
  • 32 pages

Document Identifiers

Author Details

Elias Castegren
Tobias Wrigstad

Cite As Get BibTex

Elias Castegren and Tobias Wrigstad. Relaxed Linear References for Lock-free Data Structures. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 6:1-6:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.ECOOP.2017.6

Abstract

Linear references are guaranteed to be free from aliases. This is a strong property that simplifies reasoning about programs and enables powerful optimisations, but it is also a property that is too strong for many applications. Notably, lock-free algorithms, which implement protocols that ensure safe, non-blocking concurrent access to data structures, are generally not typable with linear references because they rely on aliasing to achieve lock-freedom.

This paper presents LOLCAT, a type system with a relaxed notion of linearity that allows an unbounded number of aliases to an object as long as at most one alias at a time owns the right to access the contents of the object. This ownership can be transferred between aliases, but can never be duplicated. types are powerful enough to type several lock-free data structures and give a compile-time guarantee of absence of data-races when accessing owned data. In particular, LOLCAT is able to assign types to the CAS (compare and swap) primitive that precisely describe how ownership is transferred across aliases, possibly across different threads.

The paper introduces LOLCAT through a sound core procedural calculus, and shows how LOLCAT can be applied to three fundamental lock-free data structures. It also discusses a prototype implementation which integrates LOLCAT with an object-oriented programming language.

Subject Classification

Keywords
  • Type systems
  • Concurrency
  • Lock-free programming

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Jonathan Aldrich, Valentin Kostadinov, and Craig Chambers. Alias annotations for program understanding. In ACM SIGPLAN Notices, volume 37, pages 311-330. ACM, 2002. Google Scholar
  2. Shekhar Borkar and Andrew A Chien. The future of microprocessors. Communications of the ACM, 54(5):67-77, 2011. Google Scholar
  3. Chandrasekhar Boyapati and Martin Rinard. A parameterized type system for race-free java programs. In ACM SIGPLAN Notices, volume 36, pages 56-69. ACM, 2001. Google Scholar
  4. John Boyland. Alias burying: Unique variables without destructive reads. Softw., Pract. Exper., 31(6):533-553, 2001. Google Scholar
  5. John Boyland. The interdependence of effects and uniqueness. In Workshop on Formal Techs. for Java Programs, 2001. Google Scholar
  6. John Boyland. Checking interference with fractional permissions. In Static Analysis, pages 55-72. Springer, 2003. Google Scholar
  7. John Boyland, James Noble, and William Retert. Capabilities for sharing. In ECOOP 2001—Object-Oriented Programming, pages 2-27. Springer, 2001. Google Scholar
  8. John Tang Boyland and William Retert. Connecting effects and uniqueness with adoption. ACM SIGPLAN Notices, 40(1):283-295, 2005. Google Scholar
  9. Stephan Brandauer, Elias Castegren, Dave Clarke, Kiko Fernandez-Reyes, EinarBroch Johnsen, KaI. Pun, S.LizethTapia Tarifa, Tobias Wrigstad, and AlbertMingkun Yang. Parallel Objects for Multicores: A Glimpse at the Parallel Language Encore. In Formal Methods for Multicore Programming, volume 9104 of LNCS, pages 1-56. Springer International Publishing, 2015. URL: http://dx.doi.org/10.1007/978-3-319-18941-3_1.
  10. E. Castegren and T. Wrigstad. Lolcat: Relaxed linear references for lock-free programming. Technical Report 2016-013, 2016. Uppsala University. URL: http://www.it.uu.se/research/publications/reports/2016-013/.
  11. Dave Clarke and Sophia Drossopoulou. Ownership, encapsulation and the disjointness of type and effect. In ACM SIGPLAN Notices, volume 37, pages 292-310. ACM, 2002. Google Scholar
  12. Dave Clarke and Tobias Wrigstad. External uniqueness is unique enough. ECOOP 2003, pages 59-67, 2003. Google Scholar
  13. Dave Clarke, Tobias Wrigstad, Johan Östlund, and Einar Johnsen. Minimal ownership for active objects. Programming Languages and Systems, pages 139-154, 2008. Google Scholar
  14. Sylvan Clebsch, Sophia Drossopoulou, Sebastian Blessing, and Andy McNeil. Deny capabilities for safe, fast actors. In AGERE, 2015. Google Scholar
  15. Sophia Drossopoulou, Ferruccio Damiani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. Fickle: Dynamic object re-classification. In ECOOP 2001—Object-Oriented Programming, pages 130-149. Springer, 2001. Google Scholar
  16. Faith Ellen, Panagiota Fatourou, Eric Ruppert, and Franck van Breugel. Non-blocking binary search trees. In Proceedings of the 29th ACM SIGACT-SIGOPS symposium on Principles of distributed computing, pages 131-140. ACM, 2010. Google Scholar
  17. Robert Ennals, Richard Sharp, and Alan Mycroft. Linear types for packet processing. In Programming Languages and Systems, pages 204-218. Springer, 2004. Google Scholar
  18. Manuel Fahndrich and Robert DeLine. Adoption and focus: Practical linear types for imperative programming. In ACM SIGPLAN Notices, volume 37, pages 13-24. ACM, 2002. Google Scholar
  19. Mikhail Fomitchev and Eric Ruppert. Lock-free linked lists and skip lists. In Proceedings of the twenty-third annual ACM symposium on Principles of distributed computing, pages 50-59. ACM, 2004. Google Scholar
  20. Anwar Ghuloum. Face the inevitable, embrace parallelism. Communications of the ACM, 52(9):36-38, 2009. Google Scholar
  21. Colin S Gordon. Verifying Concurrent Programs by Controlling Alias Interference. PhD thesis, University of Washington, 2014. Google Scholar
  22. Colin S Gordon, Matthew J Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy. Uniqueness and reference immutability for safe parallelism. In ACM SIGPLAN Notices, volume 47, pages 21-40. ACM, 2012. Google Scholar
  23. Alexey Gotsman, Byron Cook, Matthew Parkinson, and Viktor Vafeiadis. Proving that non-blocking algorithms don't block. In ACM SIGPLAN Notices, volume 44, pages 16-28. ACM, 2009. Google Scholar
  24. Aaron Greenhouse and John Boyland. An object-oriented effects system. In ECOOP’99—Object-Oriented Programming, pages 205-229. Springer, 1999. Google Scholar
  25. Philipp Haller and Martin Odersky. Capabilities for uniqueness and borrowing. In ECOOP 2010-Object-Oriented Programming, pages 354-378. Springer, 2010. Google Scholar
  26. Tim Harris, Simon Marlow, Simon Peyton-Jones, and Maurice Herlihy. Composable memory transactions. In Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, pages 48-60. ACM, 2005. Google Scholar
  27. Timothy L Harris. A pragmatic implementation of non-blocking linked-lists. In DISC, volume 1, pages 300-314. Springer, 2001. Google Scholar
  28. Frédéric Haziza, Lukáš Holík, Roland Meyer, and Sebastian Wolff. Pointer Race Freedom, pages 393-412. Springer Berlin Heidelberg, Berlin, Heidelberg, 2016. URL: http://dx.doi.org/10.1007/978-3-662-49122-5_19.
  29. Steve Heller, Maurice Herlihy, Victor Luchangco, Mark Moir, William N Scherer III, and Nir Shavit. A lazy concurrent list-based set algorithm. In International Conference On Principles Of Distributed Systems, pages 3-16. Springer, 2005. Google Scholar
  30. Maurice Herlihy. A methodology for implementing highly concurrent data structures. In ACM SIGPLAN Notices, volume 25, pages 197-206. ACM, 1990. Google Scholar
  31. Maurice P Herlihy and Jeannette M Wing. Linearizability: A correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems (TOPLAS), 12(3):463-492, 1990. Google Scholar
  32. John Hogg. Islands: Aliasing protection in object-oriented languages. In ACM SIGPLAN Notices, volume 26, pages 271-285. ACM, 1991. Google Scholar
  33. IBM. Ibm system/370 extended architecture, principles of operation, 1983. publication no. SA22-7085. Google Scholar
  34. Cliff B Jones. Specification and design of (parallel) programs. In IFIP congress, volume 83, pages 321-332, 1983. Google Scholar
  35. Naoki Kobayashi. Quasi-linear types. In Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 29-42. ACM, 1999. Google Scholar
  36. Maged M Michael and Michael L Scott. Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In Proceedings of the fifteenth annual ACM symposium on Principles of distributed computing, pages 267-275. ACM, 1996. Google Scholar
  37. Filipe Militão. Rely-Guarantee Protocols for Safe Interference over Shared Memory. PhD thesis, Carnegie Mellon University &Universidade de Lisboa, 2015. Google Scholar
  38. Filipe Militão, Jonathan Aldrich, and Luís Caires. Aliasing control with view-based typestate. In Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs, page 7. ACM, 2010. Google Scholar
  39. Naftaly H Minsky. Towards alias-free pointers. In ECOOP’96—Object-Oriented Programming, pages 189-209. Springer, 1996. Google Scholar
  40. Mark Moir and Nir Shavit. Concurrent data structures. Handbook of Data Structures and Applications, pages 47-14, 2007. Google Scholar
  41. Peter Müller. Modular Specification and Verification of Object-oriented Programs. Springer-Verlag, Berlin, Heidelberg, 2002. Google Scholar
  42. Peter Müller and Arsenii Rudich. Ownership transfer in universe types. In ACM SIGPLAN Notices, volume 42, pages 461-478. ACM, 2007. Google Scholar
  43. Johan Östlund. Language Constructs for Safe Parallel Programming on Multi-cores. PhD thesis, Department of Information Technology, Uppsala University, Jan 2016. Google Scholar
  44. Amir Pnueli. In transition from global to modular temporal reasoning about programs. In Logics and models of concurrent systems, pages 123-144. Springer, 1985. Google Scholar
  45. François Pottier and Jonathan Protzenko. Programming with permissions in Mezzo. In Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming (ICFP'13), pages 173-184, September 2013. Google Scholar
  46. Herb Sutter. The free lunch is over: A fundamental turn toward concurrency in software. Dr. Dobb’s journal, 30(3):202-210, 2005. Google Scholar
  47. Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. Information and computation, 111(2):245-296, 1994. Google Scholar
  48. R Kent Treiber. Systems programming: Coping with parallelism. International Business Machines Incorporated, Thomas J. Watson Research Center, 1986. Google Scholar
  49. Aaron Turon. Reagents: expressing and composing fine-grained concurrency. In ACM SIGPLAN Notices, volume 47, pages 157-168. ACM, 2012. Google Scholar
  50. Jan Vitek and Boris Bokowski. Confined types in java. Software: Practice and Experience, 31(6):507-532, 2001. Google Scholar
  51. Philip Wadler. Linear types can change the world. In IFIP TC, volume 2, pages 347-359. Citeseer, 1990. Google Scholar
  52. Edwin Westbrook, Jisheng Zhao, Zoran Budimli, and Vivek Sarkar. Practical permissions for race-free parallelism. In James Noble, editor, ECOOP 2012, volume 7313 of LNCS, pages 614-639. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-31057-7_27.
  53. Albert Mingkun Yang and Tobias Wrigstad. Type-assisted automatic garbage collection for lock-free data structures. In International Symposium on Memory Management, 2017. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact