Analysis and Verification of Solid State Drives

Abstract

Solid state drives (SSDs) are emerging as the primary storage device in diverse newlinecomputing environments ranging from personal computing to high-performance newlinedata centers. The sophisticated controller design, inherent parallelism in the flashbased newlinestorage, and efficient utilization of the internal caches enable SSDs to achieve newlinesubstantial performance gain over conventional hard disks. However, the complex newlinedesign of the SSD also increases the probability of bugs or design faults in the newlineSSD. Hence, we employ formal modeling and verification to ensure the absence newlineof bugs in the SSD design. First, we present a formal model of the NAND flash newlinememory (back-end of the SSD) that supports advanced operations necessary for newlinehigh performance. We prove that our model satisfies several vital properties associated newlinewith a functionally correct device. Next, we present the formal model newlinefor the SSD flash translation layer (FTL), which is the most complex part of the newlineSSD controller/front-end. Introducing new features to an SSD design results in newlineupgrading an existing design and thereby making the design more complex; in newlineaddition, this could introduce more design bugs. We first considered the FTL of a newlinestandard SSD. Then, we systematically extended the base-model to incorporate a newlinesecurity feature like recovery from a ransomware attack to model a ransomwareproof newlineSSD FTL. We present a systematic approach to extend an FTL design that newlineinvolves design and proof reuse. newlineThe next objective of our thesis is to design a fair SSD. Fairness became a newlinemajor concern after the emergence of NVMe (Non Volatile Memory Express) host newlineprotocol-based SSDs. We develop a fuzzy-based fairness control technique at the newlinefront-end data cache level. Our approach substantially improved the overall performance newlineand fairness of the SSD. We observed that cache management policy newlinecould significantly impact the performance, endurance, and robustness of the SSD. newlineWe present an extensive survey of SSD internal cache management policies.