Document Open Access Logo

Composing Interfering Abstract Protocols

Authors Filipe Militão, Jonathan Aldrich, Luís Caires

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2016.16.pdf
  • Filesize: 0.75 MB
  • 26 pages

Document Identifiers

Subject Classification

Keywords
  • shared memory interference
  • protocol composition
  • aliasing
  • linearity

Metrics

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

Abstract

The undisciplined use of shared mutable state can be a source of program errors when aliases unsafely interfere with each other.
While protocol-based techniques to reason about interference abound, they do not address two practical concerns: the decidability of protocol composition and its integration with protocol abstraction.
We show that our composition procedure is decidable and that it ensures safe interference even when composing abstract protocols.
To evaluate the expressiveness of our protocol framework for safe shared memory interference, we show how this same protocol framework can be used to model safe, typeful message-passing concurrency idioms.

Cite As Get BibTex

Filipe Militão, Jonathan Aldrich, and Luís Caires. Composing Interfering Abstract Protocols. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 16:1-16:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.ECOOP.2016.16

Author Details

Filipe Militão
Jonathan Aldrich
Luís Caires

References

  1. A. Ahmed, M. Fluet, and G. Morrisett. L3: A linear language with locations. Fundam. Inf., 77(4):397-449, December 2007. Google Scholar
  2. N. E. Beckman, K. Bierhoff, and J. Aldrich. Verifying correct usage of atomic blocks and typestate. In OOPSLA 2008. Google Scholar
  3. K. Bierhoff and J. Aldrich. Modular typestate checking of aliased objects. In OOPSLA 2007. Google Scholar
  4. G. Castagna and B. C. Pierce. Decidable bounded quantification. In POPL 1994. Google Scholar
  5. S. Crafa and L. Padovani. The chemical approach to typestate-oriented programming. In OOPSLA 2015. Google Scholar
  6. T. Dinsdale-Young, L. Birkedal, P. Gardner, M. Parkinson, and H. Yang. Views: compositional reasoning for concurrent programs. In POPL 2013. Google Scholar
  7. T. Dinsdale-Young, M. Dodds, P. Gardner, M. J. Parkinson, and V. Vafeiadis. Concurrent abstract predicates. In ECOOP 2010. Google Scholar
  8. M. Fähndrich and K. Rustan M. Leino. Heap monotonic typestate. In IWACO 2003. Google Scholar
  9. X. Feng. Local rely-guarantee reasoning. In POPL '09. Google Scholar
  10. J.-Y. Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. Google Scholar
  11. C. S. Gordon, M. D. Ernst, and D. Grossman. Rely-guarantee references for refinement types over aliased mutable data. In PLDI 2013. Google Scholar
  12. J. B. Jensen and L. Birkedal. Fictional separation logic. In ESOP 2012. Google Scholar
  13. C. B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 1983. Google Scholar
  14. R. Jung, D. Swasey, F. Sieczkowski, K. Svendsen, A. Turon, L. Birkedal, and D. Dreyer. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In POPL 2015. Google Scholar
  15. N. R. Krishnaswami, P. Pradic, and N. Benton. Integrating linear and dependent types. In POPL 2015. Google Scholar
  16. N. R. Krishnaswami, A. Turon, D. Dreyer, and D. Garg. Superficially substructural types. In ICFP 2012. Google Scholar
  17. K. R. Leino and P. Müller. A basis for verifying multi-threaded programs. In ESOP 2009. Google Scholar
  18. F. Militão. Rely-Guarantee Protocols for Safe Interference over Shared Memory. PhD thesis, Carnegie Mellon University and Universidade Nova de Lisboa, 2015. Google Scholar
  19. F. Militão, J. Aldrich, and L. Caires. Rely-guarantee protocols. In ECOOP 2014. Google Scholar
  20. F. Militão, J. Aldrich, and L. Caires. Substructural typestates. In PLPV 2014. Google Scholar
  21. F. Militão, J. Aldrich, and L. Caires. Composing interfering abstract protocols (technical report). CMU-CS-16-103, 2016. Google Scholar
  22. R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, i. Inf. Comput., September 1992. Google Scholar
  23. A. Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germán Andrés Delbianco. Communicating state transition systems for fine-grained concurrent resources. In ESOP 2014. Google Scholar
  24. S. Peyton Jones, A. Gordon, and S. Finne. Concurrent haskell. In POPL 1996. Google Scholar
  25. A. Pilkiewicz and F. Pottier. The essence of monotonic state. In TLDI 2011. Google Scholar
  26. F. Pottier and J. Protzenko. Programming with permissions in mezzo. In ICFP 2013. Google Scholar
  27. J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proc. Logic in Computer Science, pages 55-74, 2002. Google Scholar
  28. J. Seco and L. Caires. Subtyping first-class polymorphic components. In ESOP 2005. Google Scholar
  29. R. E. Strom. Mechanisms for compile-time enforcement of security. In POPL 1983. Google Scholar
  30. R. E. Strom and S. Yemini. Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Software Eng., 12(1):157-171, 1986. Google Scholar
  31. K. Svendsen and L. Birkedal. Impredicative concurrent abstract predicates. In ESOP 2014. Google Scholar
  32. A. Turon, D. Dreyer, and L. Birkedal. Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In ICFP '13. Google Scholar
  33. R. Wolff, R. Garcia, É. Tanter, and J. Aldrich. Gradual typestate. In ECOOP 2011. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact