استدلال درباره سیستم های ذخیره سازی ابری Reasoning about Cloud Storage Systems

1. Introduction Data creation is occurring at a record rate, referred to big data, has emerged as a widely recognized trend. Cloud computing is a fast-growing technology to perform massivescale and complex computing. Big data and cloud computing are conjoined [10]. The former provides users the ability to process queries across multiple datasets, and the latter provides the underlying engine. As an elementary part of cloud computing, cloud storage plays an important role in underlying data collection, storage, maintenance and output. Nowadays, many clouding computing systems have already been put into use, with their own cloud storage systems (CSSs). One typical example is Google File System (GFS) [8], which is a scalable distributed file system for large dataintensive applications and takes Google cloud computing into practice. Like GFS, CSSs have more characteristics than traditional storage systems. An important one is that data files are stored in a way of block. That is, the storage resources of CSSs consist of small block spaces with a fixed size. When storing a data file, the system may first cut the file into some segments, and then put these segments into proper blocks, taking every segment as a whole. Take GFS as an example. Roughly, GFS works as follows. When a costumer makes a request to store a file in a GFS, the system cuts the file into several fragments, each with an equal size (usually 64MB) except for the last one. Then the system assigns a sequence of blocks (called “chunks” [8] in GFS) to deposit fragments of the file, one by one. Accordingly, each chunk is of size 64M. Finally it returns all the block addresses so that it can build a file table to record the relation between the file fragments and the blocks. Other CSSs, like HDFS [6], have a similar procedure. At first glance, the above procedure of saving a file into blocks in a CSS looks similar to that of saving values into memory cells in a memory management system. But there are still some substantial differences. For example, an array can be put into a series of continuous memory cells, whereas there are no “continuous” block addresses in most CSSs. Instead, a file may be put into several discrete blocks, even spreading in different block servers. These differences make the properties of cloud storage management very different from those of traditional memory management. Although the concept of block storage has been proposed for many years, it becomes more complicated in CSSs. Therefore it brings the problem how to ensure the reliability of such CSSs. The reliability of CSSs may include many issues, such as retrievability, search efficiency, correctness of management programs, etc. Here we focus on the correctness of management programs, which is the basis of the reliability of CSSs. Formal methods are mature enough for developing the correctness of most computer programs. Furthermore, formal method for traditional file system is a hot topic. P. Gardner and G. Nizik proposed their work about local reasoning for the POSIX file system [7, 16]. W.H Hesselink and M.I Lal provided abstract definitions for file systems which are defined as a partial function from paths to data [11]. In addition, some efforts to formalize CSSs have been made. V. Serbanescu et al. proposed a modeling method for distributed data aggregation service relied on a storage system [19, 20]. Stephen et al.