Abstract
File systems not only have to be functionally correct, they also have to be crash-safe: a power cut while an operation is running must be guaranteed to lead to a consistent state after restart that loses as little information as possible. Specification and verification of crash-safety is particularly difficult for non-redundant write-back caches. This paper defines a novel crash-safety criterion that facilitates specification and verification of order-preserving caches. A power cut is basically observationally equivalent to a retraction of a few of the last executed operations. The approach is modular: It gives simple proof obligations for each individual component and for each refinement in the development. The theory is supported by our interactive theorem prover KIV and proof obligations for crash-safety have been verified for the Flashix flash file system.
Supported by the Deutsche Forschungsgemeinschaft (DFG), “Verifikation von Flash-Dateisystemen” (grants RE828/13-1 and RE828/13-2).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The classification of Bornholt et al. [3] defines sequential crash consistency.
- 2.
- 3.
Note that the POSIX specification [1] explicitly permits such short writes to surface at the system interface.
- 4.
In the actual models recovery is a separate operation that runs directly after a crash and tries to restore the state. To keep the presentation brief, we combine the crash and recovery into one transition here.
References
The Open Group Base Specifications Issue 7, IEEE Std 1003.1, 2013 edn. The IEEE and The Open Group (2013)
Amani, S., Murray, T.: Specifying a realistic file system. In: Proceedings of Workshop on Models for Formal Analysis of Real Systems. Electronic Proceedings in Theoretical Computer Science, vol. 196, pp. 1–9. Open Publishing Association (2015)
Bornholt, J., Kaufmann, A., Li, J., Krishnamurthy, A., Torlak, E., Wang, X.: Specifying and checking file system crash-consistency models. In: Proceedings of ASPLOS, pp. 83–98. ACM (2016)
Chajed, T., Chen, H., Chlipala, A., Kaashoek, M.F., Zeldovich, N., Ziegler, D.: Certifying a file system using crash hoare logic: correctness in the presence of crashes. Commun. ACM 60(4), 75–84 (2017)
Chen, H.: Certifying a crash-safe file system. Ph.D. thesis, Massachusetts Institute of Technology, Cambridge, MA, United States (2016)
Chen, H., Ziegler, D., Chlipala, A., Zeldovich, N., Kaashoek, M.F.: Using crash hoare logic for certifying the FSCQ file system. In: Proceedings of the Symposium on Operating Systems Principles (SOSP). ACM (2015)
de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, Cambridge (1998)
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.: Inside a verified flash file system: transactions and garbage collection. In: Gurfinkel, A., Seshia, S.A. (eds.) VSTTE 2015. LNCS, vol. 9593, pp. 73–93. Springer, Cham (2016). doi:10.1007/978-3-319-29613-5_5
Ernst, G., Pfähler, J., Schellhorn, G., Reif, W.: Modular, crash-safe refinement for ASMs with submachines. Sci. Comput. Program. (SCP) 131, 3–21 (2016)
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). doi:10.1007/978-3-642-54108-7_13
He, J., Hoare, C.A.R., Sanders, J.W.: Data refinement refined resume. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol. 213, pp. 187–196. Springer, Heidelberg (1986). doi:10.1007/3-540-16442-1_14
Koskinen, E., Yang, J.: Reducing crash recoverability to reachability. In: Proceedings of Principles of Programming Languages (POPL), pp. 97–108. ACM (2016)
Lali, M.I.: File system formalization: revisited. Int. J. Adv. Comput. Sci. 3(12), 602–606 (2013)
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, Cham (2014). doi:10.1007/978-3-319-06410-9_31
Ntzik, G., da Rocha Pinto, P., Gardner, P.: Fault-tolerant resource reasoning. In: Feng, X., Park, S. (eds.) APLAS 2015. LNCS, vol. 9458, pp. 169–188. Springer, Cham (2015). doi:10.1007/978-3-319-26529-2_10
Rosenblum, M., Ousterhout, J.K.: The design and implementation of a log-structured file system. ACM Trans. Comput. Syst. (TOCS) 10(1), 26–52 (1992)
Schellhorn, G., Ernst, G., Pfähler, J., Haneberg, D., Reif, W.: Development of a verified flash file system. ABZ 2014. LNCS, vol. 8477, pp. 9–24. Springer, Heidelberg (2014). doi:10.1007/978-3-662-43652-3_2
Sigurbjarnarson, H., Bornholt, J., Torlak, E., Wang, X.: Push-button verification of file systems via crash refinement. In: Symposium on Operating Systems Design and Implementation (OSDI). USENIX Association (2016)
Tseng, H-W., Grupp, L., Swanson, S.: Understanding the impact of power loss on flash memory. In: Proceedings of the Design Automation Conference (DAC), pp. 35–40. ACM (2011)
Tweedie, S.C.: Journaling the Linux ext2fs filesystem. In: The Fourth Annual Linux Expo (1998)
Woodcock, J., Davies, J.: Using Z: Specification, Proof and Refinement. Prentice Hall, Upper Saddle River (1996)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Pfähler, J., Ernst, G., Bodenmüller, S., Schellhorn, G., Reif, W. (2017). Modular Verification of Order-Preserving Write-Back Caches. In: Polikarpova, N., Schneider, S. (eds) Integrated Formal Methods. IFM 2017. Lecture Notes in Computer Science(), vol 10510. Springer, Cham. https://doi.org/10.1007/978-3-319-66845-1_25
Download citation
DOI: https://doi.org/10.1007/978-3-319-66845-1_25
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66844-4
Online ISBN: 978-3-319-66845-1
eBook Packages: Computer ScienceComputer Science (R0)