research-article

Reasoning about the POSIX file system: local update and global pathnames

Authors:

Philippa GardnerAuthors Info & Claims

OOPSLA 2015: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications

Pages 201 - 220

https://doi.org/10.1145/2814270.2814306

Published: 23 October 2015 Publication History

Abstract

We introduce a program logic for specifying a core sequential subset of the POSIX file system and for reasoning abstractly about client programs working with the file system. The challenge is to reason about the combination of local directory update and global pathname traversal (including '.' and symbolic links) which may overlap the directories being updated. Existing reasoning techniques are either based on first-order logic and do not scale, or on separation logic and can only handle linear pathnames (no '.' or symbolic links). We introduce fusion logic for reasoning about local update and global pathname traversal, introducing a novel effect frame rule to propagate the effect of a local update on overlapping pathnames. We apply our reasoning to the standard recursive remove utility (rm -r), discovering bugs in well-known implementations.

References

[1]

POSIX.1-2008, IEEE 1003.1-2008, The Open Group Base Specifications Issue 7. URL http://pubs.opengroup. org/onlinepubs/9699919799/.

[2]

K. Arkoudas, K. Zee, V. Kuncak, and M. Rinard. Verifying a File System Implementation. In LNCS: Formal Methods and Software Engineering. Springer Berlin Heidelberg, 2004.

[3]

N. Biri and D. Galmiche. Models and separation logics for resource trees. Journal of Logic and Computation, 17(4):687– 726, 2007.

Digital Library

[4]

R. Bornat, C. Calcagno, P. O’Hearn, and M. Parkinson. Permission Accounting in Separation Logic. In Proceedings of the 32Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, 2005.

Digital Library

[5]

R. Bornat, C. Calcagno, and H. Yang. Variables as Resource in Separation Logic. Electronic Notes in Theoretical Computer Science, 155:247–276, 2006.

Digital Library

[6]

J. Boyland. Checking Interference with Fractional Permissions. In Static Analysis, Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2003.

Digital Library

[7]

C. Calcagno, P. Gardner, and U. Zarfaty. Context Logic and Tree Update. In Proceedings of the 32Nd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL, 2005.

Digital Library

[8]

L. Cardelli and A. D. Gordon. Ambient logic. Mathematical Structures in Computer Science, 2003.

[9]

P. da Rocha Pinto, T. Dinsdale-Young, M. Dodds, P. Gardner, and M. Wheelhouse. A Simple Abstraction for Complex Concurrent Indexes. In Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA, 2011.

Digital Library

[10]

T. Dinsdale-Young, M. Dodds, P. Gardner, M. Parkinson, and V. Vafeiadis. Concurrent Abstract Predicates. In ECOOP. Springer Berlin Heidelberg, 2010.

Digital Library

[11]

T. Dinsdale-Young, L. Birkedal, P. Gardner, M. Parkinson, and H. Yang. Views: Compositional Reasoning for Concurrent Programs. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, 2013.

Digital Library

[12]

M. Dodds, X. Feng, M. Parkinson, and V. Vafeiadis. Deny-Guarantee Reasoning. In Proceedings of the 18th European Symposium on Programming Languages and Systems: Held As Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, ESOP, 2009.

Digital Library

[13]

G. Ernst, G. Schellhorn, D. Haneberg, J. Pfähler, and W. Reif. Verification of a Virtual Filesystem Switch. In Verified Software: Theories, Tools, Experiments, Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2014.

Digital Library

[14]

K. Fisher, N. Foster, D. Walker, and K. Q. Zhu. Forest: A Language and Toolkit for Programming with Filestores. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP, 2011.

Digital Library

[15]

L. Freitas, Z. Fu, and J. Woodcock. POSIX File Store in Z/Eves: An Experiment in the Verified Software Repository. Engineering of Complex Computer Systems, IEEE International Conference, 2007.

Digital Library

[16]

L. Freitas, J. Woodcock, and A. Butterfield. POSIX and the Verification Grand Challenge: A Roadmap. 2014 19th International Conference on Engineering of Complex Computer Systems, 0:153–162, 2008.

Digital Library

[17]

P. Gardner, S. Maffeis, and G. D. Smith. Towards a Program Logic for JavaScript. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, 2012.

Digital Library

[18]

P. Gardner, G. Ntzik, and A. Wright. Local Reasoning for the POSIX File System. In Programming Languages and Systems, Lecture Notes in Computer Science. Springer Berlin Heidelberg, 2014.

Digital Library

[19]

W. H. Hesselink and M. Lali. Formalizing a Hierarchical File System. REFINE, 2009.

Digital Library

[20]

A. Hobor and J. Villard. The Ramifications of Sharing in Data Structures. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, 2013.

Digital Library

[21]

R. Joshi and G. J. Holzmann. A Mini Challenge: Build a Verifiable Filesystem. Formal Aspects of Computing, 19(2): 269–272, 2007.

[22]

C. Morgan and B. Sufrin. Specification of the UNIX Filing System. Software Engineering, IEEE Transactions on, 1984.

Digital Library

[23]

G. Ntzik and P. Gardner. Reasoning about the POSIX File System: Local Update and Global Pathnames. Technical report, Imperial College London, 2015. URL http://hdl. handle.net/10044/1/25816.

[24]

J. C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In Logic in Computer Science, 2002. Proceedings. 17th Annual IEEE Symposium on, 2002.

Digital Library

Cited By

Becker BJeannerod NMarché CRégis-Gianas YSighireanu MTreinen R(2022)The CoLiS platform for the analysis of maintainer scripts in Debian software packagesInternational Journal on Software Tools for Technology Transfer10.1007/s10009-022-00671-124:5(717-733)Online publication date: 23-Sep-2022
https://doi.org/10.1007/s10009-022-00671-1
Kokologiannakis MKaysin IRaad AVafeiadis V(2021)PerSeVerE: persistency semantics for verification under ext4Proceedings of the ACM on Programming Languages10.1145/34343245:POPL(1-29)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434324
Becker BJeannerod NMarché CRégis-Gianas YSighireanu MTreinen R(2020)Analysing installation scenarios of Debian packagesTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-45237-7_14(235-253)Online publication date: 17-Apr-2020
https://doi.org/10.1007/978-3-030-45237-7_14
Show More Cited By

Index Terms

Reasoning about the POSIX file system: local update and global pathnames
1. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Reasoning about the POSIX file system: local update and global pathnames
OOPSLA '15

We introduce a program logic for specifying a core sequential subset of the POSIX file system and for reasoning abstractly about client programs working with the file system. The challenge is to reason about the combination of local directory update ...
Local Reasoning for the POSIX File System
Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410

We provide a program logic for specifying a core subset of the sequential POSIX file system, and for reasoning abstractly about client programs working with the file system.
A multiple-file write scheme for improving write performance of small files in Fast File System

Fast File System (FFS) stores files to disk in separate disk writes, each of which incurs a disk positioning (seek + rotation) limiting the write performance for small files. We propose a new scheme called co-writing to accelerate small file writes in ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

OOPSLA 2015: Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications

October 2015

953 pages

ISBN:9781450336895

DOI:10.1145/2814270

General Chair:
Jonathan Aldrich
Carnegie Mellon University, USA
,
Program Chair:
Patrick Eugster
Purdue University, USA

ACM SIGPLAN Notices Volume 50, Issue 10
OOPSLA '15
October 2015
953 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2858965
Editor:
Andy Gill
University of Kansas, Lawrence, KS
Issue’s Table of Contents

Copyright © 2015 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 October 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Engineering and Physical Sciences Research Council

Conference

SPLASH '15

Sponsor:

SIGPLAN

SPLASH '15: Conference on Systems, Programming, Languages, and Applications: Software for Humanity

October 25 - 30, 2015

PA, Pittsburgh, USA

Acceptance Rates

Overall Acceptance Rate 268 of 1,244 submissions, 22%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
237
Total Downloads

Downloads (Last 12 months)16
Downloads (Last 6 weeks)3

Reflects downloads up to 23 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Becker BJeannerod NMarché CRégis-Gianas YSighireanu MTreinen R(2022)The CoLiS platform for the analysis of maintainer scripts in Debian software packagesInternational Journal on Software Tools for Technology Transfer10.1007/s10009-022-00671-124:5(717-733)Online publication date: 23-Sep-2022
https://doi.org/10.1007/s10009-022-00671-1
Kokologiannakis MKaysin IRaad AVafeiadis V(2021)PerSeVerE: persistency semantics for verification under ext4Proceedings of the ACM on Programming Languages10.1145/34343245:POPL(1-29)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434324
Becker BJeannerod NMarché CRégis-Gianas YSighireanu MTreinen R(2020)Analysing installation scenarios of Debian packagesTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-45237-7_14(235-253)Online publication date: 17-Apr-2020
https://doi.org/10.1007/978-3-030-45237-7_14
Férée HÅman Pohjola JKumar ROwens SMyreen MHo S(2018)Program Verification in the Presence of I/OVerified Software. Theories, Tools, and Experiments10.1007/978-3-030-03592-1_6(88-111)Online publication date: 24-Nov-2018
https://doi.org/10.1007/978-3-030-03592-1_6
Jing YWang HHuang YZhang LXu JCao Y(2017)A modeling language to describe massive data storage management in cyber-physical systemsJournal of Parallel and Distributed Computing10.1016/j.jpdc.2016.12.008103:C(113-120)Online publication date: 1-May-2017
https://dl.acm.org/doi/10.1016/j.jpdc.2016.12.008
Najafzadeh MShapiro MEugster P(2017)Co-Design and Verification of an Available File SystemVerification, Model Checking, and Abstract Interpretation10.1007/978-3-319-73721-8_17(358-381)Online publication date: 29-Dec-2017
https://doi.org/10.1007/978-3-319-73721-8_17
Ntzik Gda Rocha Pinto PGardner P(2015)Fault-Tolerant Resource ReasoningProgramming Languages and Systems10.1007/978-3-319-26529-2_10(169-188)Online publication date: 9-Dec-2015
https://doi.org/10.1007/978-3-319-26529-2_10
Kokologiannakis MKaysin IRaad AVafeiadis V(2021)PerSeVerE: persistency semantics for verification under ext4Proceedings of the ACM on Programming Languages10.1145/34343245:POPL(1-29)Online publication date: 4-Jan-2021
https://doi.org/10.1145/3434324
Jing YWang HHuang YZhang LXu JCao Y(2017)A modeling language to describe massive data storage management in cyber-physical systemsJournal of Parallel and Distributed Computing10.1016/j.jpdc.2016.12.008103:C(113-120)Online publication date: 1-May-2017
https://dl.acm.org/doi/10.1016/j.jpdc.2016.12.008

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents