Reasoning About Concurrent Programs Under Cloud Storage Systems

With the rapid growth of data and the promotion of public cloud platforms,more and more applications rely on Cloud Storage Systems(CSS).In recent years,accidents related to cloud storage systems have occurred frequently and caused considerable losses to operators and customers of CSS.The reliability of CSS needs to be improved significantly.There are some significant differences between CSS and traditional local storage systems.First,the basic storage unit of CSS is the block logically,while CSS still physically depends on the local storage system.Second,there are lots of concurrent programs running on the cloud platform.Improving the reliability of concurrent programs is more challenging than improving the sequential ones.The correctness of CSS is essential to its reliability.Separation Logic(SL)is one of the mainstream verification methods for storage resources.Though various tools based on SL have worked on modeling the CSS management program or reasoning about the concurrent program separately,none of them could deal with CSS.We propose a system for reasoning about the concurrent programs under the cloud storage environment.Our work includes the following:(1)Proposing a Modeling Language with a channel mechanism so that we can describe the concurrent programs;(2)Proposing an Assertion Language so that we can describe the state of the system that is composed of CSS and local storage systems;(3)Proposing a set of Hoare Style Rules so that we can reason about the programs;others,we give an example to show how it works.Our system can verify the correctness of concurrent programs under the cloud storage environment and significantly expand the validating range of SL and the verifiable range of CSS.In this way,we can improve the reliability of CSS and the computer systems that rely on cloud storage services,which have great theoretical significance and application value.