Abstract
The work presented here addresses a long-standing conceptual gap in flash file system verification: We map an abstract graph-based representation down to the flat blocks of bytes of the storage medium. Specifically, we consider grouping of file system objects into atomic transactions together with layout, allocation and garbage collection of on-flash storage space. Two major concerns guide the design and verification: proper handling of errors and, more importantly, guaranteed recovery from unexpected power cuts. Finding useful specifications of intermediate interfaces to address these concerns realistically dominates the verification effort.
This work is part of the project “Verifikation von Flash-Dateisystemen” (RE828/13-1) sponsored by the Deutsche Forschungsgemeinschaft (DFG).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
- 2.
With hard-links (which we support) this structure becomes an acyclic graph.
- 3.
- 4.
- 5.
A maximum group size of \(n = 4\) nodes is sufficient for all operations of the FS core. Note that an entire write operation is already decomposed into fixed-size writes of individual segments by higher components.
- 6.
- 7.
We need to be able to read all nodes from the erase block in order to perform garbage collection, but detecting partially written nodes reliably in between completely written ones is not possible.
- 8.
Note that wear-leveling is performed by a lower layer and therefore is not limited by the choice of block of the garbage collection, i.e., blocks in the log can be moved by wear-leveling.
References
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)
Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Lessons learned from Microkernel verification - specification is the new bottleneck. In: SSV, pp. 18–32 (2012)
Börger, E.: The ASM refinement method. Form. Asp. Comput. 15(1–2), 237–257 (2003)
Börger, E., Stärk, R.F.: Abstract State Machines – A Method for High-Level System Design and Analysis. Springer, Berlin (2003)
Butterfield, A., Woodcock, J.: Formalising flash memory: first steps. In: IEEE International Conference on Engineering of Complex Computer Systems, pp. 251–260 (2007)
Chen, H., Ziegler, D., Chlipala, A., Kaashoek, M.F., Kohler, E., Zeldovich, N.: Specifying crash safety for storage systems. In: 15th Workshop on Hot Topics in Operating Systems (HotOS XV). USENIX Association (2015)
Chen, H., Ziegler, D., Chlipala, A., Zeldovich, N., Kaashoek, M.F.: Using crash hoare logic for certifying the FSCQ file system. In: Proceedings of SOSP. ACM (2015)
Damchoom, K.: An incremental refinement approach to a development of a flash-based file system in Event-B, Ph.D. thesis, University of Southampton (2010)
Ernst, G., Pfähler, J., Schellhorn, G.: Web presentation of the Flash Filesystem (2015). https://swt.informatik.uni-augsburg.de/swt/projects/flash.html
Ernst, G., Pfähler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV - overview and VerifyThis competition. Softw. Tools Technol. Transf. (STTT) 17(6), 677–694 (2015)
Ernst, G., Pfähler, J., Schellhorn, G., Reif, W.: Modular, crash-safe refinement for ASMs with submachines. Science of Computer Programming, ABZ special issue, 2015 (submitted) (2014)
Ernst, G., Schellhorn, G., Haneberg, D., Pfähler, J., Reif, W.: A formal model of a virtual filesystem switch. In: Proceedings of Software and Systems Modeling (SSV), EPTCS, pp. 33–45 (2012)
Ernst, G., Schellhorn, G., Haneberg, D., Pfähler, J., Reif, W.: Verification of a Virtual Filesystem Switch. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 242–261. Springer, Heidelberg (2014)
Ferreira, M.A., Silva, S.S., Oliveira, J.N.: Verifying intel Flash File System core specification. In: Modelling and Analysis in VDM: Proceedings of the Fourth VDM/Overture Workshop, pp. 54–71, Technical report CS-TR-1099 (2008)
Freitas, L., Woodcock, J., Fu, Z.: POSIX file store in Z/Eves: an experiment in the verified software repository. Sci. Comput. Program. 74(4), 238–257 (2009)
Gleixner, T., Haverkamp, F., Bityutskiy, A.: UBI - Unsorted Block Images (2006). http://www.linux-mtd.infradead.org/doc/ubidesign/ubidesign.pdf
Hesselink, W.H., Lali, M.I.: Formalizing a hierarchical file system. Form. Asp. Comput. 24(1), 27–44 (2012)
Hunter, A.: A brief introduction to the design of UBIFS (2008). http://www.linux-mtd.infradead.org/doc/ubifs_whitepaper.pdf
Joshi, R., Holzmann, G.J.: A mini challenge: build a verifiable filesystem. Form. Asp. Comput. 19(2), 269–272 (2007)
Kang, E., Jackson, D.: Formal Modeling and Analysis of a Flash Filesystem in Alloy. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 294–308. Springer, Heidelberg (2008)
Marić, O., Sprenger, C.: Verification of a transactional memory manager under hardware failures and restarts. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 449–464. Springer, Heidelberg (2014)
Morgan, C., Sufrin, B.: Specification of the UNIX filing system. Specification Case Studies, pp. 91–140. Prentice Hall Ltd., Hertfordshire (1987)
Pfähler, J., Ernst, G., Schellhorn, G., Haneberg, D., Reif, W.: Formal specification of an erase block management layer for flash memory. In: Legay, A., Bertacco, V. (eds.) HVC 2013. LNCS, vol. 8244, pp. 214–229. Springer, Heidelberg (2013)
Ridge, T., Sheets, D., Tuerk, T., Giugliano, A., Madhavapeddy, A., Sewell, P.: SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems. In: Proceedings of SOSP. ACM (2015)
Schellhorn, G.: Completeness of fair ASM refinement. Sci. Comput. Program. 76(9), 756–773 (2009). Elsevier
Schellhorn, G., Ernst, G., Pfähler, J., Haneberg, D., Reif, W.: Development of a verified flash file system. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 9–24. Springer, Heidelberg (2014)
Schellhorn, G., Tofan, B., Ernst, G., Pfähler, J., Reif, W.: RGITL: a temporal logic framework for compositional reasoning about interleaved programs. Ann. Math. Artif. Intell. (AMAI) 71, 1–44 (2014)
Schierl, A., Schellhorn, G., Haneberg, D., Reif, W.: Abstract specification of the UBIFS file system for flash memory. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 190–206. Springer, Heidelberg (2009)
The Open Group: The Open Group Base Specifications Issue 7, IEEE Std 1003.1, 2008 Edition. http://www.unix.org/version3/online.html (login required)
UBI - Out-of-Band Data. http://www.linux-mtd.infradead.org/faq/ubi.html
Woodcock, J.C.P., Davies, J.: Using Z: Specification. Proof and Refinement. Prentice Hall International Series in Computer Science. Prentice Hall, New York (1996)
Acknowledgement
We thank the anonymous reviewers for their detailed and helpful comments.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Ernst, G., Pfähler, J., Schellhorn, G., Reif, W. (2016). Inside a Verified Flash File System: Transactions and Garbage Collection. In: Gurfinkel, A., Seshia, S.A. (eds) Verified Software: Theories, Tools, and Experiments. VSTTE 2015. Lecture Notes in Computer Science(), vol 9593. Springer, Cham. https://doi.org/10.1007/978-3-319-29613-5_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-29613-5_5
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-29612-8
Online ISBN: 978-3-319-29613-5
eBook Packages: Computer ScienceComputer Science (R0)