Dear Spiral user, We’re pleased to introduce Helix, https://helix.imperial.ac.uk/ Imperial’s new repository for research datasets. Please use Helix for all future dataset deposits. There is no change to Spiral - continue depositing as usual. For queries, contact the Research Data Management team at rdm-enquiries@imperial.ac.uk. Kind regards, the Spiral Team. The Spiral team
Reasoning about the POSIX file system: Local update and global pathnames
File(s)
oopsla2015.pdf (658.76 KB)
Accepted version
Author(s)
Ntzik, G
Gardner, P
Type
Conference Paper
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.
Date Issued
2015-10-23
Date Acceptance
2015-08-03
Citation
Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2015, pp.201-220
URI
DOI
ISBN
978-1-4503-3689-5
Publisher
ACM
Start Page
201
End Page
220
Journal / Book Title
Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
Copyright Statement
© ACM, 2015. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, {OCt 2015} https://dx.doi.org/10.1145/2814270.2814306
Source
2015 ACM SIGPLAN International Conference on Object-Oriented Programming Systems Languages and Applications (OOPSLA 2015)
Subjects
POSIX
file systems
local reasoning
global pathnames
separation logic
Publication Status
Published
Start Date
2015-10-25
Finish Date
2015-10-30
Coverage Spatial
Pittsburgh, PA, USA