As NAND flash memory has become a widely used storage medium, traditional file systems face challenges in adapting to its unique characteristics. The Flash-Friendly File System (F2FS) is designed to optimize file and data management on NAND flash, addressing issues such as raw NAND interface compatibility, the "wandering tree" problem, high reading costs, and inefficient garbage collection. Through a log-structured foundation and various optimizations, including multi-head logging, node address table (NAT), and reserved in-place updated metadata sections, F2FS achieves enhanced performance, reliability, and prolonged lifespan. This study constructs a multi-head log model based on F2FS and introduces a new hardware-independent metric—Write Amplification Factor (WAF)—to analyze performance. The research demonstrates that separating node and data blocks is more effective in improving garbage collection efficiency than simple hot and cold data segregation.

Summary In existing computer systems, file systems are indispensable for organizing user data and system codes. However, several studies have reported certain file system errors that cause significant data loss or system crashes. Most of these errors are due to external failures, such as an unexpected power outage. However, comprehensively evaluating file system robustness to detect these errors is challenging. The various types of file systems use different data structures and algorithms for various applications. Moreover, file system errors may be triggered by an unpredictable external condition. In addition, a file system works in an operating system's kernel layer as a passive module and runs in a multi‐thread mode, which makes file system testing time‐intensive. Furthermore, the large number of states in file systems leads to greedy checking, which results in a state explosion. In this study, we comprehensively evaluated the robustness expected in multiple properties of file systems using a model checking approach. The evaluation covered the majority of the mainstream file system types and included both single‐thread and multi‐thread modes. We developed Promela models that abstracted the real file systems and subsequently checked them using a SPIN model checker. Our model was optimized to avoid state explosion during model checking. Using the model checking, we successfully detected corner‐case errors during an unexpected power outage. By analysing counterexamples generated by model checking, we determined an improved file system model capable of preventing errors in most mainstream file system types. Finally, we rechecked the improved file system model and verified the absence of all critical errors.

File systems are used to organize data on storage devices. The file systems may crash due to external failures, such as an unexpected power outage. Therefore, the robustness of the file system is essential. Although some existing works evaluated the robustness of file systems, they are not comprehensive enough and cost many resources. In this work, we design a file system model and verify properties related to the correctness of the file using the SPIN model checker. The robustness of the file system has been comprehensively evaluated in both single-thread and multi-thread modes. There is a critical error in the file system. By analyzing counterexamples given by model checking, we propose a mechanism to prevent it. Based on the mechanism, the robustness of the file system is effectively improved.