Safe, Flexible Aliasing with Deferred Borrows

Author Chris Fallin



PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2020.30.pdf
  • Filesize: 0.55 MB
  • 26 pages

Document Identifiers

Author Details

Chris Fallin
  • Mozilla, Mountain View, CA, USA

Cite AsGet BibTex

Chris Fallin. Safe, Flexible Aliasing with Deferred Borrows. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 30:1-30:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ECOOP.2020.30

Abstract

In recent years, programming-language support for static memory safety has developed significantly. In particular, borrowing and ownership systems, such as the one pioneered by the Rust language, require the programmer to abide by certain aliasing restrictions but in return guarantee that no unsafe aliasing can ever occur. This allows parallel code to be written, or existing code to be parallelized, safely and easily, and the aliasing restrictions also statically prevent a whole class of bugs such as iterator invalidation. Borrowing is easy to reason about because it matches the intuitive ownership-passing conventions often used in systems languages. Unfortunately, a borrowing-based system can sometimes be too restrictive. Because borrows enforce aliasing rules for their entire lifetimes, they cannot be used to implement some common patterns that pointers would allow. Programs often use pseudo-pointers, such as indices into an array of nodes or objects, instead, which can be error-prone: the program is still memory-safe by construction, but it is not logically memory-safe, because an object access may reach the wrong object. In this work, we propose deferred borrows, which provide the type-safety benefits of borrows without the constraints on usage patterns that they otherwise impose. Deferred borrows work by encapsulating enough state at creation time to perform the actual borrow later, while statically guaranteeing that the eventual borrow will reach the same object it would have otherwise. The static guarantee is made with a path-dependent type tying the deferred borrow to the container (struct, vector, etc.) of the borrowed object. This combines the type-safety of borrowing with the flexibility of traditional pointers, while retaining logical memory-safety.

Subject Classification

ACM Subject Classification
  • Software and its engineering → General programming languages
Keywords
  • Rust
  • type systems
  • ownership types
  • borrowing

Metrics

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

References

  1. J Aldrich and C Chambers. Ownership domains: Separating aliasing policy from mechanism. ECOOP, 2004. Google Scholar
  2. N Amin, T Rompf, and M Odersky. Foundations of path-dependent types. OOPSLA, 2014. Google Scholar
  3. C Boyapati, A Sălcianu, W Beebee Jr., and M Rinard. Ownership types for safe region-based memory management in real-time Java. PLDI, 2003. Google Scholar
  4. D Clarke and S Drossopoulou. Ownership, encapsulation and the disjointness of type and effect. OOPSLA, 2002. Google Scholar
  5. D G Clarke, J M Potter, and J Noble. Ownership types for flexible alias protection. OOPSLA, 1998. Google Scholar
  6. W Dietl, S Drossopoulou, and P Müller. Generic universe types. ECOOP, 2007. Google Scholar
  7. E Ernst. Family polymorphism. ECOOP, 2001. Google Scholar
  8. D Grossman, G Morrisett, T Jim, M Hicks, Y Wang, and J Cheney. Region-based memory management in Cyclone. PLDI, 2002. Google Scholar
  9. R L Bocchino Jr., V S Adve, D Dig, S V Adve, S Heumann, R Komuravelli, J Overbey, P Simmons, H Sung, and M Vakilian. A type and effect system for Deterministic Parallel Java. OOPSLA, 2009. Google Scholar
  10. G. Kastrinis, G. Balatsouras, K. Ferles, N. Prokopaki-Kostopoulou, and Y. Smaragdakis. An efficient data structure for must-alias analysis. CC, 2018. Google Scholar
  11. K R M Leino, A Poetzsch-Heffter, and Y Zhou. Using data groups to specify and check side effects. PLDI, 2002. Google Scholar
  12. K Naden, R Bocchino, J Aldrich, and K Bierhoff. A type system for borrowing permissions. POPL, 2011. Google Scholar
  13. N Nystrom, V Saraswat, J Palsberg, and C Grothoff. Constrained types for object-oriented languages. OOPSLA, 2008. Google Scholar
  14. M Odersky, V Cremet, C Röckl, and M Zenger. A nominal theory of objects with dependent types. ECOOP, 2003. Google Scholar
  15. J Östlund and T Wrigstad. Multiple aggregate entry points for ownership types. ECOOP, 2012. Google Scholar
  16. A Potanin, M Damitio, and J Noble. Are your incoming aliases really necessary? counting the cost of object ownership. ICSE, 2013. Google Scholar
  17. A Potanin, J Noble, D Clarke, and R Biddle. Generic ownership for generic java. OOPSLA, 2006. Google Scholar
  18. Rust community. The Rust programming language. URL: https://www.rust-lang.org/.
  19. Rust community. Rust survey 2018 results. URL: https://blog.rust-lang.org/2018/11/27/Rust-survey-2018.html.
  20. S Stork, K Naden, J Sunshine, M Mohr, A Fonseca, P Marques, and J Aldrich. Aeminium: A permission-based concurrent-by-default programming language approach. ACM Trans. Prog. Lang. Sys., 36, March 2014. Google Scholar
  21. A Weiss, D Patterson, ND Matsakis, and A Ahmed. Oxide: the essence of Rust, 2019. URL: http://arxiv.org/abs/1903.00982.
  22. E Westbrook, J Zhao, Z Budimlić, and V Sarkar. Practical permissions for race-free parallelism. ECOOP, 2012. Google Scholar
  23. Hongwei Xi and Frank Pfenning. Dependent types in practical programming. POPL, 1999. 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