Advertisement

Modular Verification of Order-Preserving Write-Back Caches

  • Jörg PfählerEmail author
  • Gidon Ernst
  • Stefan Bodenmüller
  • Gerhard Schellhorn
  • Wolfgang Reif
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10510)

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.

Keywords

Write-back caching Crash-safe refinement Flash file systems 

References

  1. 1.
    The Open Group Base Specifications Issue 7, IEEE Std 1003.1, 2013 edn. The IEEE and The Open Group (2013)Google Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    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)Google Scholar
  4. 4.
    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)CrossRefGoogle Scholar
  5. 5.
    Chen, H.: Certifying a crash-safe file system. Ph.D. thesis, Massachusetts Institute of Technology, Cambridge, MA, United States (2016)Google Scholar
  6. 6.
    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)Google Scholar
  7. 7.
    de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, Cambridge (1998)CrossRefzbMATHGoogle Scholar
  8. 8.
    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)CrossRefGoogle Scholar
  9. 9.
    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 Google Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    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 CrossRefGoogle Scholar
  12. 12.
    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 CrossRefGoogle Scholar
  13. 13.
    Koskinen, E., Yang, J.: Reducing crash recoverability to reachability. In: Proceedings of Principles of Programming Languages (POPL), pp. 97–108. ACM (2016)Google Scholar
  14. 14.
    Lali, M.I.: File system formalization: revisited. Int. J. Adv. Comput. Sci. 3(12), 602–606 (2013)Google Scholar
  15. 15.
    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 CrossRefGoogle Scholar
  16. 16.
    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 CrossRefGoogle Scholar
  17. 17.
    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)CrossRefGoogle Scholar
  18. 18.
    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 CrossRefGoogle Scholar
  19. 19.
    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)Google Scholar
  20. 20.
    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)Google Scholar
  21. 21.
    Tweedie, S.C.: Journaling the Linux ext2fs filesystem. In: The Fourth Annual Linux Expo (1998)Google Scholar
  22. 22.
    Woodcock, J., Davies, J.: Using Z: Specification, Proof and Refinement. Prentice Hall, Upper Saddle River (1996)zbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Jörg Pfähler
    • 1
    Email author
  • Gidon Ernst
    • 1
  • Stefan Bodenmüller
    • 1
  • Gerhard Schellhorn
    • 1
  • Wolfgang Reif
    • 1
  1. 1.Institute for Software and Systems EngineeringUniversity of AugsburgAugsburgGermany

Personalised recommendations