Document Open Access Logo

Definite Reference Mutability

Author Ana Milanova

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2018.25.pdf
  • Filesize: 0.73 MB
  • 30 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program analysis
  • Software and its engineering → General programming languages
Keywords
  • reference immutability
  • type inference
  • CFL-reachability
  • precision

Metrics

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

Abstract

Reference immutability type systems such as Javari and ReIm ensure that a given reference cannot be used to mutate the referenced object. These systems are conservative in the sense that a mutable reference may be mutable due to approximation.
In this paper, we present ReM (for definite Re[ference] M[utability]). It separates mutable references into (1) definitely mutable, and (2) maybe mutable, i.e., references whose mutability is due to inherent approximation. In addition, we propose a CFL-reachability system for reference immutability, and prove that it is equivalent to ReIm/ReM, thus building a novel framework for reasoning about correctness of reference immutability type systems. We have implemented ReM and applied it on a large benchmark suite. Our results show that approximately 86.5% of all mutable references are definitely mutable.

Cite As Get BibTex

Ana Milanova. Definite Reference Mutability. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 25:1-25:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.ECOOP.2018.25

Author Details

Ana Milanova
  • Dept. of Computer Science, Rensselaer Polytechnic Institute, 110 8th Street, Troy NY, USA

Funding

  • Milanova, Ana: This work was partially supported by NSF grant 1319384.

Supplementary Materials

References

  1. Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools (2nd Edition). Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2006. Google Scholar
  2. Shay Artzi, Adam Kiezun, David Glasser, and Michael D. Ernst. Combined static and dynamic mutability analysis. In Proceedings of the Twenty-second IEEE/ACM International Conference on Automated Software Engineering, ASE '07, pages 104-113, New York, NY, USA, 2007. ACM. URL: http://dx.doi.org/10.1145/1321631.1321649.
  3. Joseph A. Bank, Andrew C. Myers, and Barbara Liskov. Parameterized types for java. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '97, pages 132-145, New York, NY, USA, 1997. ACM. URL: http://dx.doi.org/10.1145/263699.263714.
  4. Michael Carbin, Sasa Misailovic, and Martin C. Rinard. Verifying quantitative reliability for programs that execute on unreliable hardware. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, part of SPLASH 2013, Indianapolis, IN, USA, October 26-31, 2013, pages 33-52, 2013. Google Scholar
  5. David G. Clarke, John M. Potter, and James Noble. Ownership types for flexible alias protection. In Proceedings of the 13th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications, OOPSLA '98, pages 48-64, New York, NY, USA, 1998. ACM. URL: http://dx.doi.org/10.1145/286936.286947.
  6. Rance Cleaveland and Matthew Hennessy. Testing equivalence as a bisimulation equivalence. In Automatic Verification Methods for Finite State Systems, International Workshop, Grenoble, France, June 12-14, 1989, Proceedings, pages 11-23, 1989. URL: http://dx.doi.org/10.1007/3-540-52148-8_2.
  7. Dave Cunningham, Werner Dietl, Sophia Drossopoulou, Adrian Francalanza, Peter Müller, and Alexander J. Summers. Formal methods for components and objects. In Frank S. Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul Roever, editors, Formal Methods for Components and Objects, 6th International Symposium, FMCO 2007, Amsterdam, The Netherlands, October 24-26, 2007, Revised Lectures, chapter Universe Types for Topology and Encapsulation, pages 72-112. Springer-Verlag, Berlin, Heidelberg, 2008. URL: http://dx.doi.org/10.1007/978-3-540-92188-2_4.
  8. Werner Dietl and Peter Müller. Universes: Lightweight ownership for JML. Journal of Object Technology, 4(8):5-32, 2005. Google Scholar
  9. Werner Dietl and Peter Müller. Runtime universe type inference. In IWACO, pages 72-80, 2007. URL: http://sct.ethz.ch/projects/student_docs/Frank_Lyner/Frank_Lyner_MA_paper.pdf.
  10. Julian Dolby, Christian Hammer, Daniel Marino, Frank Tip, Mandana Vaziri, and Jan Vitek. A data-centric approach to synchronization. ACM Transactions on Programming Languages and Systems, 34(1):1-48, apr 2012. Google Scholar
  11. Manuel Fähndrich, Jakob Rehof, and Manuvir Das. Scalable context-sensitive flow analysis using instantiation constraints. In Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation, PLDI '00, pages 253-263, New York, NY, USA, 2000. ACM. URL: http://dx.doi.org/10.1145/349299.349332.
  12. Robert Fuhrer, Frank Tip, Adam Kieżun, Julian Dolby, and Markus Keller. Efficiently refactoring java applications to use generic libraries. In Proceedings of the 19th European Conference on Object-Oriented Programming, ECOOP'05, pages 71-96, Berlin, Heidelberg, 2005. Springer-Verlag. URL: http://dx.doi.org/10.1007/11531142_4.
  13. Colin S. Gordon, Matthew J. Parkinson, Jared Parsons, Aleks Bromfield, and Joe Duffy. Uniqueness and reference immutability for safe parallelism. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA '12, pages 21-40, New York, NY, USA, 2012. ACM. URL: http://dx.doi.org/10.1145/2384616.2384619.
  14. Neville Grech and Yannis Smaragdakis. P/taint: unified points-to and taint analysis. PACMPL, 1(OOPSLA):102:1-102:28, 2017. URL: http://dx.doi.org/10.1145/3133926.
  15. Christian Haack and Erik Poll. Type-based object immutability with flexible initialization. In Proceedings of the 23rd European Conference on ECOOP 2009 - Object-Oriented Programming, Genoa, pages 520-545, Berlin, Heidelberg, 2009. Springer-Verlag. URL: http://dx.doi.org/10.1007/978-3-642-03013-0_24.
  16. Wei Huang, Werner Dietl, Ana Milanova, and Michael D. Ernst. Inference and checking of object ownership. In Proceedings of the 26th European Conference on Object-Oriented Programming, ECOOP'12, pages 181-206, Berlin, Heidelberg, 2012. Springer-Verlag. URL: http://dx.doi.org/10.1007/978-3-642-31057-7_9.
  17. Wei Huang, Yao Dong, Ana Milanova, and Julian Dolby. Scalable and precise taint analysis for android. In Proceedings of the 2015 International Symposium on Software Testing and Analysis, ISSTA 2015, pages 106-117, New York, NY, USA, 2015. ACM. URL: http://dx.doi.org/10.1145/2771783.2771803.
  18. Wei Huang, Ana Milanova, Werner Dietl, and Michael D. Ernst. Reim &reiminfer: Checking and inference of reference immutability and method purity. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA '12, pages 879-896, New York, NY, USA, 2012. ACM. URL: http://dx.doi.org/10.1145/2384616.2384680.
  19. Adam Kiezun, Michael D. Ernst, Frank Tip, and Robert M. Fuhrer. Refactoring for parameterizing java classes. In Proceedings of the 29th International Conference on Software Engineering, ICSE '07, pages 437-446, Washington, DC, USA, 2007. IEEE Computer Society. URL: http://dx.doi.org/10.1109/ICSE.2007.70.
  20. Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. Principles of program analysis. Springer-Verlag New York, Inc., 1999. Google Scholar
  21. David J. Pearce. Jpure:: A modular purity system for java. In Proceedings of the 20th International Conference on Compiler Construction: Part of the Joint European Conferences on Theory and Practice of Software, CC'11/ETAPS'11, pages 104-123, Berlin, Heidelberg, 2011. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=1987237.1987247.
  22. Alex Potanin, Johan Östlund, Yoav Zibin, and Michael D. Ernst. Immutability. In Aliasing in Object-Oriented Programming, volume 7850 of LNCS, pages 233-269. Springer-Verlag, apr 2013. Google Scholar
  23. Jaime Quinonez, Matthew S. Tschantz, and Michael D. Ernst. Inference of reference immutability. In Proceedings of the 22Nd European Conference on Object-Oriented Programming, ECOOP '08, pages 616-641, Berlin, Heidelberg, 2008. Springer-Verlag. URL: http://dx.doi.org/10.1007/978-3-540-70592-5_26.
  24. Jakob Rehof and Manuel Fähndrich. Type-base flow analysis: From polymorphic subtyping to cfl-reachability. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '01, pages 54-66, New York, NY, USA, 2001. ACM. URL: http://dx.doi.org/10.1145/360204.360208.
  25. Thomas Reps. Undecidability of context-sensitive data-independence analysis. ACM Transactions on Programming Languages and Systems, 22(1):162 - -186, 2000. Google Scholar
  26. Thomas W. Reps. Program analysis via graph reachability. Information & Software Technology, 40(11-12):701-726, 1998. URL: http://dx.doi.org/10.1016/S0950-5849(98)00093-7.
  27. Thomas W. Reps, Susan Horwitz, and Shmuel Sagiv. Precise interprocedural dataflow analysis via graph reachability. In Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995, pages 49-61, 1995. URL: http://dx.doi.org/10.1145/199448.199462.
  28. Adrian Sampson, Werner Dietl, Emily Fortuna, Danushen Gnanapragasam, Luis Ceze, and Dan Grossman. Enerj: approximate data types for safe and general low-power computation. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011, pages 164-174, 2011. Google Scholar
  29. Umesh Shankar, Kunal Talwar, Jeffrey S. Foster, and David Wagner. Detecting format string vulnerabilities with type qualifiers. In Proceedings of the 10th Conference on USENIX Security Symposium - Volume 10, SSYM'01, pages 16-16, Berkeley, CA, USA, 2001. USENIX Association. URL: http://dl.acm.org/citation.cfm?id=1267612.1267628.
  30. Manu Sridharan and Rastislav Bodík. Refinement-based context-sensitive points-to analysis for java. In Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '06, pages 387-400, New York, NY, USA, 2006. ACM. URL: http://dx.doi.org/10.1145/1133981.1134027.
  31. Alexandru Sălcianu and Martin Rinard. Purity and side effect analysis for java programs. In Proceedings of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI'05, pages 199-215, Berlin, Heidelberg, 2005. Springer-Verlag. URL: http://dx.doi.org/10.1007/978-3-540-30579-8_14.
  32. Rishi Surendran and Vivek Sarkar. Automatic parallelization of pure method calls via conditional future synthesis. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, pages 20-38, New York, NY, USA, 2016. ACM. URL: http://dx.doi.org/10.1145/2983990.2984035.
  33. Frank Tip, Robert M. Fuhrer, Adam Kieżun, Michael D. Ernst, Ittai Balaban, and Bjorn De Sutter. Refactoring using type constraints. ACM Transactions on Programming Languages and Systems, 33(3):1-47, 2011. URL: http://dx.doi.org/10.1145/1961204.1961205.
  34. Matthew S. Tschantz and Michael D. Ernst. Javari: Adding reference immutability to java. In Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications, OOPSLA '05, pages 211-230, New York, NY, USA, 2005. ACM. URL: http://dx.doi.org/10.1145/1094811.1094828.
  35. Mandana Vaziri, Frank Tip, Julian Dolby, Christian Hammer, and Jan Vitek. A type system for data-centric synchronization. In Proceedings of the 24th European Conference on Object-oriented Programming, ECOOP'10, pages 304-328, Berlin, Heidelberg, 2010. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=1883978.1884000.
  36. Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, and William R. Cook. Verifying equivalence of database-driven applications. Proc. ACM Program. Lang., 2(POPL):56:1-56:29, dec 2017. URL: http://dx.doi.org/10.1145/3158144.
  37. Guoqing Xu, Atanas Rountev, and Manu Sridharan. Scaling cfl-reachability-based points-to analysis using context-sensitive must-not-alias analysis. In Proceedings of the 23rd European Conference on ECOOP 2009 - Object-Oriented Programming, Genoa, pages 98-122, Berlin, Heidelberg, 2009. Springer-Verlag. URL: http://dx.doi.org/10.1007/978-3-642-03013-0_6.
  38. Qirun Zhang and Zhendong Su. Context-sensitive data-dependence analysis via linear conjunctive language reachability. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pages 344-358, New York, NY, USA, 2017. ACM. URL: http://dx.doi.org/10.1145/3009837.3009848.
  39. Yoav Zibin, Alex Potanin, Mahmood Ali, Shay Artzi, Adam Kie, un, and Michael D. Ernst. Object and reference immutability using java generics. In Proceedings of the the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, ESEC-FSE '07, pages 75-84, New York, NY, USA, 2007. ACM. URL: http://dx.doi.org/10.1145/1287624.1287637.
  40. Yoav Zibin, Alex Potanin, Paley Li, Mahmood Ali, and Michael D. Ernst. Ownership and immutability in generic java. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA '10, pages 598-617, New York, NY, USA, 2010. ACM. URL: http://dx.doi.org/10.1145/1869459.1869509.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact