Document Open Access Logo

Reference Capabilities for Concurrency Control

Authors Elias Castegren, Tobias Wrigstad

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2016.5.pdf
  • Filesize: 0.73 MB
  • 26 pages

Document Identifiers

Author Details

Elias Castegren
Tobias Wrigstad

Cite As Get BibTex

Elias Castegren and Tobias Wrigstad. Reference Capabilities for Concurrency Control. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 5:1-5:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.ECOOP.2016.5

Abstract

The proliferation of shared mutable state in object-oriented
programming complicates software development as two seemingly
unrelated operations may interact via an alias and produce
unexpected results. In concurrent programming this manifests itself as data-races. Concurrent object-oriented programming further suffers from the fact that code that warrants synchronisation cannot easily be distinguished from code that does not. The burden is placed solely on the programmer to reason about alias freedom, sharing across threads and side-effects to deduce where and when to apply concurrency control, without inadvertently blocking parallelism.

This paper presents a reference capability approach to concurrent
and parallel object-oriented programming where all uses of
aliases are guaranteed to be data-race free. The static type of
an alias describes its possible sharing without using explicit
ownership or effect annotations. Type information can express
non-interfering deterministic parallelism without dynamic
concurrency control, thread-locality, lock-based schemes, and
guarded-by relations giving multi-object atomicity to nested data
structures. Unification of capabilities and traits allows
trait-based reuse across multiple concurrency scenarios with
minimal code duplication. The resulting system brings together
features from a wide range of prior work in a unified way.

Subject Classification

Keywords
  • Type systems
  • Capabilities
  • Traits
  • Concurrency
  • Object-Oriented

Metrics

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

References

  1. Martin Abadi, Cormac Flanagan, and Stephen N. Freund. Types for safe locking: Static race detection for Java. ACM Trans. Program. Lang. Syst., 28(2):207-255, March 2006. URL: http://dx.doi.org/10.1145/1119479.1119480.
  2. Paulo Sérgio Almeida. Control of Object Sharing in Programming Languages. PhD thesis, Imperial College London, June 1998. Google Scholar
  3. David F. Bacon, Robert E. Strom, and Ashis Tarafdar. Guava: a Dialect of Java Without Data Races. In OOPSLA, pages 382-400, 2000. Google Scholar
  4. Henry G. Baker. 'Use-once' Variables and Linear Objects - Storage Management, Reflection and Multi-Threading. ACM SIGPLAN Notices, 30(1), January 1995. Google Scholar
  5. Robert Bocchino. An Effect System and Language for Deterministic-By-Default Parallel Programming, 2010. PhD thesis, University of Illinois at Urbana-Champaign. Google Scholar
  6. Shekhar Borkar and Andrew A Chien. The future of microprocessors. CACM, 54(5):67-77, 2011. Google Scholar
  7. Chandrasekhar Boyapati, Robert Lee, and Martin C. Rinard. Ownership types for safe programming: preventing data races and deadlocks. In OOPSLA, pages 211-230, 2002. Google Scholar
  8. John Boyland. Alias burying: Unique variables without destructive reads. Software - Practice and Experience, 31(6):533-553, May 2001. Google Scholar
  9. John Boyland. Checking interference with fractional permissions. In SAS, pages 55-72, 2003. Google Scholar
  10. John Boyland, James Noble, and William Retert. Capabilities for Sharing: A Generalisation of Uniqueness and Read-Only. ECOOP. Springer, 2001. Google Scholar
  11. John Tang Boyland. Semantics of fractional permissions with nesting. ACM Trans. Program. Lang. Syst., 32(6):22:1-22:33, August 2010. URL: http://dx.doi.org/10.1145/1749608.1749611.
  12. John Tang Boyland and William Retert. Connecting Effects and Uniqueness with Adoption. In POPL, pages 283-295, 2005. Google Scholar
  13. Luís Caires and João C. Seco. The Type Discipline of Behavioral Separation. POPL, 2013. Google Scholar
  14. Nicholas R. Cameron, Sophia Drossopoulou, James Noble, and Matthew J. Smith. Multiple ownership. In OOPSLA, 2007. Google Scholar
  15. E. Castegren and T. Wrigstad. Reference capabilities for trait based reuse and concurrency control. Technical Report 2016-007, 2016. Uppsala University. Google Scholar
  16. Dave Clarke, Johan Östlund, Ilya Sergey, and Tobias Wrigstad. Ownership Types: A Survey. In Aliasing in Object-Oriented Programming, volume 7850 of LNCS. Springer, 2013. Google Scholar
  17. Dave Clarke and Tobias Wrigstad. External uniqueness is unique enough. In ECOOP, 2003. Google Scholar
  18. Dave Clarke, Tobias Wrigstad, Johan Östlund, and Einar Johnsen. Minimal ownership for active objects. In Programming Languages and Systems, volume 5356 of LNCS. Springer, 2008. Google Scholar
  19. David G. Clarke and Sophia Drossopoulou. Ownership, Encapsulation and the Disjointness of Type and Effect. In OOPSLA, pages 292-310, 2002. Google Scholar
  20. Sylvan Clebsch, Sophia Drossopoulou, Sebastian Blessing, and Andy McNeil. Deny capabilities for safe, fast actors. In AGERE, 2015. Google Scholar
  21. David Cunningham, Sophia Drossopoulou, and Susan Eisenbach. Universe Types for Race Safety. In VAMP, 2007. URL: http://pubs.doc.ic.ac.uk/universes-races/.
  22. Werner M. Dietl. Universe Types: Topology, Encapsulation, Genericity, and Tools. Ph.D., Department of Computer Science, ETH Zurich, December 2009. Google Scholar
  23. M. Fähndrich and R. DeLine. Adoption and Focus: Practical Linear Types for Imperative Programming. In PLDI, pages 13-24, 2002. Google Scholar
  24. Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy. Uniqueness and Reference Immutability for Safe Parallelism. In OOPSLA, pages 21-40, 2012. Google Scholar
  25. Aaron Greenhouse and John Boyland. An object-oriented effects system. ECOOP, 1999. Google Scholar
  26. Philipp Haller and Martin Odersky. Capabilities for uniqueness and borrowing. In ECOOP, 2010. Google Scholar
  27. John Hogg. Islands: Aliasing Protection in Object-Oriented Languages. In OOPSLA, 1991. Google Scholar
  28. John Hogg, Doug Lea, Alan Wills, Dennis de Champeaux, and Richard Holt. The Geneva Convention on the Treatment of Object Aliasing. OOPS Messenger, 3(2), April 1992. Google Scholar
  29. Neelakantan R. Krishnaswami, Aaron Turon, Derek Dreyer, and Deepak Garg. Superficially Substructural Types. ICFP, New York, NY, USA, 2012. ACM. Google Scholar
  30. K Rustan M Leino, Peter Müller, and Jan Smans. Verification of concurrent programs with Chalice. In Foundations of Security Analysis and Design V. 2009. Google Scholar
  31. H. Levy, editor. Capability Based Computer Systems. Digital Press, 1984. Google Scholar
  32. Filipe Militão, Jonathan Aldrich, and Luís Caires. Rely-guarantee protocols. In ECOOP, 2014. Google Scholar
  33. Mark Samuel Miller. Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. PhD thesis, Johns Hopkins University, 2006. Google Scholar
  34. Naftaly Minsky. Towards alias-free pointers. In ECOOP, July 1996. Google Scholar
  35. P. Müller and A. Poetzsch-Heffter. Universes: a type system for controlling representation exposure. Technical Report 263, 1999. Fernuniversität Hagen. Google Scholar
  36. Peter Müller. Modular Specification and Verification of Object-Oriented Programs, volume 2262 of Lecture Notes in Computer Science. Springer, 2002. Google Scholar
  37. Pratibha Permandla, Michael Roberson, and Chandrasekhar Boyapati. A type System for Preventing Data Races and Deadlocks in the Java Virtual Machine Language. In LCTES, pages 1-10, 2007. Google Scholar
  38. François Pottier and Jonathan Protzenko. Programming with Permissions in Mezzo. In ICFP, pages 173-184, September 2013. Google Scholar
  39. Nathanael Schärli, Stéphane Ducasse, Oscar Nierstrasz, and AndrewP. Black. Traits: Composable units of behaviour. In ECOOP, 2003. Google Scholar
  40. Jesse A. Tov. Practical Programming with Substructural Types. PhD thesis, Northeastern University, 2012. Google Scholar
  41. Philip Wadler. Linear Types Can Change the World! In M. Broy and C. Jones, editors, IFIP TC 2 Working Conference on Programming Concepts and Methods. North Holland, 1990. Google Scholar
  42. Edwin Westbrook, Jisheng Zhao, Zoran Budimli, and Vivek Sarkar. Practical permissions for race-free parallelism. In ECOOP, 2012. Google Scholar
  43. Tobias Wrigstad, Filip Pizlo, Fadi Meawad, Lei Zhao, and Jan Vitek. Loci: Simple thread-locality for Java. In ECOOP, 2009. Google Scholar
  44. Yang Zhao. Concurrency Analysis Based On Fractional Permission System. PhD thesis, University of Wisconsin - Milwaukee, 2007. Google Scholar
  45. Yoav Zibin, Alex Potanin, Shay Artzi, et al. Object and reference immutability using Java generics. In ESEC/FSE. 2007. 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