Abstract
Flash translation layer (FTL) is a part of software running on the NAND flash memory, which is ubiquitous in various devices. FTL algorithm hides the complexity of NAND flash characteristics and provides a simple and standard interface like magnetic disks. In this paper, we present a general and abstract formal model for FTL algorithms, define their functional correctness as refinement, and propose a verification framework. We demonstrate its use by verifying a classic FTL algorithm BAST. Our entire development has been formalized in the proof assistant Coq.
Foundation item: National Natural Science Foundation of China (61632005, 61502031); The State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences Open Project Fund (SYSKF1804).
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
References
Guo, Y.: The Coq Implementation of a Simple FTL Algorithm and the Functional Correctness Proof (2014)
Coq Development Team, INRIA: The Coq Proof Assistant Reference Manual (2012)
Apple Inc.: MacBook Air Flash Storage Drive Replacement Program (2013)
Klein, G., Elphinstone, K., Heiser, G.: seL4: formal verification of an OS kernel. In: Proceedings of SOSP 2009, pp. 207–220, October 2009
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). https://doi.org/10.1007/978-3-540-87603-8_23
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). https://doi.org/10.1007/978-3-319-06410-9_31
Butterfield, A., Woodcock, J.: Formalising flash memory: first steps. In: IEEE International Conference on Engineering of Complex Computer Systems, pp. 251–260 (2007)
Semiconductor, Hynix and others: Open NAND flash interface specification (2006)
Cooke, J.: The inconvenient truths of NAND flash memory. In: Micron MEMCON, 7 (2005)
Thatcher, J., Coughlin, T., Handy, J., Ekker, N.: NAND flash solid state storage for the enterprise: an in-depth look at reliability. Solid State Storage Initiative (SNIA) (2009)
Grupp, L.M., Davis, J.D., Swanson, S.: The bleak future of NAND flash memory. In: Proceedings of the 10th USENIX Conference on File and Storage Technologies, p. 2 (2012)
Grupp, L.M., Caulfield, A.M., Coburn, J., Swanson, S., Yaakobi, Ei., Siegel, P.H., Wolf, J.K.: Characterizing flash memory: anomalies, observations, and applications. In: 42nd Annual IEEE/ACM International Symposium on Microarchitecture, MICRO-42, pp. 24–33. ACM (2009)
Kim, J., Kim, J.M., Noh, S.H., Min, S.L., Cho, Y.: A space-efficient flash translation layer for CompactFlash systems. IEEE Trans. Consum. Electron. 48, 366–375 (2002)
Lee, S.-W., Park, D.: A log buffer-based flash translation layer using fully-associative sector translation. ACM Trans. Embed. Comput. Syst. (TECS) 6, 18 (2007)
Kim, S.-Y., Jung, S.-I.: A log-based flash translation layer for large NAND flash memory. In: The 8th International Conference Advanced Communication Technology, ICACT 2006, vol. 3, pp. 1641–1644. IEEE (2006)
Gupta, A., Kim, Y., Urgaonkar, B.: DFTL: a flash translation layer employing demand-based selective caching of page-level address mappings. In: Proceedinngs of ASPLOS 2009, pp. 229–240. ACM (2009)
Zheng, M., Tucek, J., Qin, F., Lillibridge, M.: Understanding the robustness of SSDS under power fault. In: FAST, pp. 271–284 (2013)
Lu, L., Arpaci-Dusseau, A.C., Arpaci-Dusseau, R.H., Lu, S.: A study of Linux file system evolution. ACM Trans. Storage (TOS) 10, 3 (2014)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Qiao, L., Li, S., Yang, H., Yang, M. (2019). A Formal Modeling and Verification Framework for Flash Translation Layer Algorithms. In: Guan, N., Katoen, JP., Sun, J. (eds) Dependable Software Engineering. Theories, Tools, and Applications. SETTA 2019. Lecture Notes in Computer Science(), vol 11951. Springer, Cham. https://doi.org/10.1007/978-3-030-35540-1_5
Download citation
DOI: https://doi.org/10.1007/978-3-030-35540-1_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-35539-5
Online ISBN: 978-3-030-35540-1
eBook Packages: Computer ScienceComputer Science (R0)