Abstract
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.
Chapter PDF
Similar content being viewed by others
References
Filesystem Hierarchy Standard Group. Filesystem hierarchy standard
POSIX.1-2008, IEEE 1003.1-2008, The Open Group Base Specifications Issue 7
Variables as resource in separation logic. Electronic Notes in Theoretical Computer Science 155, 247–276 (2006)
Arkoudas, K., Zee, K., Kuncak, V., Rinard, M.: Verifying a File System Implementation. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 373–390. Springer, Heidelberg (2004)
Calcagno, C., Gardner, P., Zarfaty, U.: Context logic and tree update. SIGPLAN Not. (2005)
Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M., Yang, H.: Views: compositional reasoning for concurrent programs. In: POPL (2013)
Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 504–528. Springer, Heidelberg (2010)
Fisher, K., Foster, N., Walker, D., Zhu, K.Q.: Forest: a language and toolkit for programming with filestores. In: ICFP (2011)
Freitas, L., Fu, Z., Woodcock, J.: POSIX file store in Z/Eves: an experiment in the verified software repository. In: IEEE International Conference on Engineering of Complex Computer Systems (2007)
Freitas, L., Woodcock, J., Butterfield, A.: POSIX and the verification grand challenge: A roadmap. In: ICECCS (2008)
Gardner, P., Ntzik, G., Wright, A.: Local Reasoning for the POSIX File System. Technical report, Imperial College London (2014), http://www.doc.ic.ac.uk/~gn408/POSIXFS/
Gardner, P., Raad, A., Wheelhouse, M., Wright, A.: Abstract Local Reasoning for Concurrent Libraries. In preparation (2014)
Gardner, P., Smith, G., Wheelhouse, M., Zarfaty, U.: Local Hoare reasoning about DOM. In: PODS (2008)
Gardner, P., Wheelhouse, M.: Small specifications for tree update, http://www.doc.ic.ac.uk/~pg/papers/move.pdf
Hesselink, W.H., Lali, M.: Formalizing a hierarchical file system. In: REFINE (2009)
Hobor, A., Villard, J.: The ramifications of sharing in data structures. In: POPL (2013)
Joshi, R., Holzmann, G.J.: A mini challenge: build a verifiable filesystem. Form. Asp. Comput. (2007)
Morgan, C., Sufrin, B.: Specification of the UNIX Filing System. IEEE Transactions on Software Engineering (1984)
Ntzik, G.: Local Reasoning about File Systems. PhD thesis (expected, 2014)
Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL (2005)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS (2002)
Smith, G.: Local Reasoning about Web Programs. PhD thesis (2011)
Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 149–168. Springer, Heidelberg (2014)
Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In: ICFP (2013)
Wright, A.: Structural Separation Logic. PhD thesis, Imperial College London (2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gardner, P., Ntzik, G., Wright, A. (2014). Local Reasoning for the POSIX File System. In: Shao, Z. (eds) Programming Languages and Systems. ESOP 2014. Lecture Notes in Computer Science, vol 8410. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54833-8_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-54833-8_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54832-1
Online ISBN: 978-3-642-54833-8
eBook Packages: Computer ScienceComputer Science (R0)