Document Open Access Logo

A Concurrent Specification of POSIX File Systems

Authors Gian Ntzik, Pedro da Rocha Pinto, Julian Sutherland, Philippa Gardner

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2018.4.pdf
  • Filesize: 0.67 MB
  • 28 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
Keywords
  • POSIX
  • concurrency
  • file systems
  • refinement
  • separation logic
  • atomicity

Metrics

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

Abstract

POSIX is a standard for operating systems, with a substantial part devoted to specifying file-system operations. File-system operations exhibit complex concurrent behaviour, comprising multiple actions affecting different parts of the state: typically, multiple atomic reads followed by an atomic update. However, the standard's description of concurrent behaviour is unsatisfactory: it is fragmented; contains ambiguities; and is generally under-specified. We provide a formal concurrent specification of POSIX file systems and demonstrate scalable reasoning for clients. Our specification is based on a concurrent specification language, which uses a modern concurrent separation logic for reasoning about abstract atomic operations, and an associated refinement calculus. Our reasoning about clients highlights an important difference between reasoning about modules built over a heap, where the interference on the shared state is restricted to the operations of the module, and modules built over a file system, where the interference cannot be restricted as the file system is a public namespace. We introduce specifications conditional on context invariants used to restrict the interference, and apply our reasoning to the example of lock files.

Cite As Get BibTex

Gian Ntzik, Pedro da Rocha Pinto, Julian Sutherland, and Philippa Gardner. A Concurrent Specification of POSIX File Systems. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 4:1-4:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.ECOOP.2018.4

Author Details

Gian Ntzik
  • Imperial College London & Amadeus, UK
Pedro da Rocha Pinto
  • Imperial College London, UK
Julian Sutherland
  • Imperial College London, UK
Philippa Gardner
  • Imperial College London, UK

Funding

EPSRC Grants EP/H008373/1, EP/K008528/1 and EP/L016796/1

References

  1. The Austin Group Mailing List. https://www.opengroup.org/austin/lists.html. Accessed: September 30, 2016.
  2. POSIX.1-2008, IEEE 1003.1-2008, The Open Group Base Specifications Issue 7. URL: http://pubs.opengroup.org/onlinepubs/9699919799/.
  3. Konstantine Arkoudas, Karen Zee, Viktor Kuncak, and Martin Rinard. Verifying a file system implementation. In Jim Davies, Wolfram Schulte, and Mike Barnett, editors, Formal Methods and Software Engineering, volume 3308 of Lecture Notes in Computer Science, pages 373-390. Springer Berlin Heidelberg, 2004. URL: http://dx.doi.org/10.1007/978-3-540-30482-1_32.
  4. Ralph-Johan Back and Joakim Wright. Refinement calculus: a systematic introduction. Springer Science &Business Media, 2012. Google Scholar
  5. Stephen Brookes. Full abstraction for a shared-variable parallel language. Information and Computation, 127(2):145-163, 1996. URL: http://dx.doi.org/10.1006/inco.1996.0056.
  6. C. Calcagno, P. W. O'Hearn, and H. Yang. Local action and abstract separation logic. In 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pages 366-378, July 2007. URL: http://dx.doi.org/10.1109/LICS.2007.30.
  7. Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. Using crash hoare logic for certifying the fscq file system. In Proceedings of the 25th Symposium on Operating Systems Principles, SOSP '15, pages 18-37, New York, NY, USA, 2015. ACM. URL: http://dx.doi.org/10.1145/2815400.2815402.
  8. Pedro da Rocha Pinto. Reasoning with Time and Data Abstractions. PhD thesis, Imperial College London, 2016. Google Scholar
  9. Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. Tada: A logic for time and data abstraction. In Richard Jones, editor, ECOOP 2014 – Object-Oriented Programming, volume 8586 of Lecture Notes in Computer Science, pages 207-231. Springer Berlin Heidelberg, 2014. URL: http://dx.doi.org/10.1007/978-3-662-44202-9_9.
  10. Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew Parkinson, and Hongseok Yang. Views: Compositional reasoning for concurrent programs. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, pages 287-300, New York, NY, USA, 2013. ACM. URL: http://dx.doi.org/10.1145/2429069.2429104.
  11. Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, MatthewJ. Parkinson, and Viktor Vafeiadis. Concurrent abstract predicates. In Theo D’Hondt, editor, ECOOP 2010 – Object-Oriented Programming, volume 6183 of Lecture Notes in Computer Science, pages 504-528. Springer Berlin Heidelberg, 2010. URL: http://dx.doi.org/10.1007/978-3-642-14107-2_24.
  12. Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler, and Wolfgang Reif. Verification of a virtual filesystem switch. In Ernie Cohen and Andrey Rybalchenko, editors, Verified Software: Theories, Tools, Experiments, volume 8164 of Lecture Notes in Computer Science, pages 242-261. Springer Berlin Heidelberg, 2014. URL: http://dx.doi.org/10.1007/978-3-642-54108-7_13.
  13. Xinyu Feng. Local rely-guarantee reasoning. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '09, pages 315-327, New York, NY, USA, 2009. ACM. URL: http://dx.doi.org/10.1145/1480881.1480922.
  14. Kathleen Fisher, Nate Foster, David Walker, and Kenny Q. Zhu. Forest: A language and toolkit for programming with filestores. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP '11, pages 292-306, New York, NY, USA, 2011. ACM. URL: http://dx.doi.org/10.1145/2034773.2034814.
  15. L. Freitas, Zheng Fu, and J. Woocock. Posix file store in z/eves: an experiment in the verified software repository. In Engineering Complex Computer Systems, 2007. 12th IEEE International Conference on, pages 3-14, July 2007. URL: http://dx.doi.org/10.1109/ICECCS.2007.36.
  16. Leo Freitas, Jim Woodcock, and Andrew Butterfield. Posix and the verification grand challenge: A roadmap. 2014 19th International Conference on Engineering of Complex Computer Systems, 0:153-162, 2008. URL: http://dx.doi.org/10.1109/ICECCS.2008.35.
  17. Philippa Gardner, Gian Ntzik, and Adam Wright. Local reasoning for the posix file system. In Zhong Shao, editor, Programming Languages and Systems, volume 8410 of Lecture Notes in Computer Science, pages 169-188. Springer Berlin Heidelberg, 2014. URL: http://dx.doi.org/10.1007/978-3-642-54833-8_10.
  18. Maurice P. Herlihy and Jeannette M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3):463-492, 1990. URL: http://dx.doi.org/10.1145/78969.78972.
  19. WimH. Hesselink and MuhammadIkram Lali. Formalizing a hierarchical file system. Formal Aspects of Computing, 24(1):27-44, 2012. URL: http://dx.doi.org/10.1007/s00165-010-0171-2.
  20. Bart Jacobs and Frank Piessens. Expressive modular fine-grained concurrency specification. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '11, pages 271-282, New York, NY, USA, 2011. ACM. URL: http://dx.doi.org/10.1145/1926385.1926417.
  21. Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java, pages 41-55. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011. URL: http://dx.doi.org/10.1007/978-3-642-20398-5_4.
  22. Rajeev Joshi and GerardJ. Holzmann. A mini challenge: build a verifiable filesystem. Formal Aspects of Computing, 19(2):269-272, 2007. URL: http://dx.doi.org/10.1007/s00165-006-0022-3.
  23. Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '15, pages 637-650, New York, NY, USA, 2015. ACM. URL: http://dx.doi.org/10.1145/2676726.2676980.
  24. Carroll Morgan and Bernard Sufrin. Specification of the unix filing system. Software Engineering, IEEE Transactions on, SE-10(2):128-142, March 1984. URL: http://dx.doi.org/10.1109/TSE.1984.5010215.
  25. Carroll Morgan and Trevor Vickers. On the refinement calculus. Springer Science &Business Media, 2012. Google Scholar
  26. Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and GermánAndrés Delbianco. Communicating state transition systems for fine-grained concurrent resources. In Zhong Shao, editor, Programming Languages and Systems, volume 8410 of Lecture Notes in Computer Science, pages 290-310. Springer Berlin Heidelberg, 2014. URL: http://dx.doi.org/10.1007/978-3-642-54833-8_16.
  27. Gian Ntzik. Reasoning About POSIX File Systems. PhD thesis, Imperial College London, sep 2016. Google Scholar
  28. Gian Ntzik, Pedro da Rocha Pinto, and Philippa Gardner. Programming Languages and Systems: 13th Asian Symposium, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings, chapter Fault-Tolerant Resource Reasoning, pages 169-188. Springer International Publishing, Cham, 2015. URL: http://dx.doi.org/10.1007/978-3-319-26529-2_10.
  29. Gian Ntzik, Pedro da Rocha Pinto, Julian Sutherland, and Philippa Gardner. A concurrent specification of POSIX file systems (technical report). Technical Report 2018/3, Department of Computing, Imperial College London, 2018. URL: https://www.doc.ic.ac.uk/research/technicalreports/2018/#3.
  30. Gian Ntzik and Philippa Gardner. Reasoning about the posix file system: Local update and global pathnames. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, pages 201-220, New York, NY, USA, 2015. ACM. URL: http://dx.doi.org/10.1145/2814270.2814306.
  31. J.C. Reynolds. Separation logic: a logic for shared mutable data structures. In Logic in Computer Science, 2002. Proceedings. 17th Annual IEEE Symposium on, pages 55-74, 2002. URL: http://dx.doi.org/10.1109/LICS.2002.1029817.
  32. John C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Millennial Perspectives in Computer Science, pages 303-321. Palgrave, 2000. Google Scholar
  33. Tom Ridge, David Sheets, Thomas Tuerk, Andrea Giugliano, Anil Madhavapeddy, and Peter Sewell. Sibylfs: Formal specification and oracle-based testing for posix and real-world file systems. In Proceedings of the 25th Symposium on Operating Systems Principles, SOSP '15, pages 38-53, New York, NY, USA, 2015. ACM. URL: http://dx.doi.org/10.1145/2815400.2815411.
  34. Kasper Svendsen and Lars Birkedal. Impredicative concurrent abstract predicates. In Zhong Shao, editor, Programming Languages and Systems, volume 8410 of Lecture Notes in Computer Science, pages 149-168. Springer Berlin Heidelberg, 2014. URL: http://dx.doi.org/10.1007/978-3-642-54833-8_9.
  35. Kasper Svendsen, Lars Birkedal, and Matthew Parkinson. Modular reasoning about separation of concurrent data structures. In Matthias Felleisen and Philippa Gardner, editors, Programming Languages and Systems, volume 7792 of Lecture Notes in Computer Science, pages 169-188. Springer Berlin Heidelberg, 2013. URL: http://dx.doi.org/10.1007/978-3-642-37036-6_11.
  36. Aaron Joseph Turon and Mitchell Wand. A separation logic for refining concurrent objects. ACM SIGPLAN Notices, 46(1):247-258, 2011. Google Scholar
  37. Viktor Vafeiadis and Matthew Parkinson. A Marriage of Rely/Guarantee and Separation Logic, pages 256-271. Springer Berlin Heidelberg, Berlin, Heidelberg, 2007. URL: http://dx.doi.org/10.1007/978-3-540-74407-8_18.
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