<p>Cloud storage systems are crucial for ensuring business stability and data reliability. Among them, block-based cloud storage systems (BCSSs) have been widely adopted in the industry due to their high efficiency and strong performance. However, system failures occur from time to time, causing significant financial losses to companies. Therefore, verifying the reliability of BCSSs has become important and urgent. Nevertheless, since blocks in these systems are of finite but variable sizes, it is difficult to describe and verify properties using first-order logic or separation logic. To address this issue, we propose Sequence-Heap Separation Logic (SeqSL), which introduces sequence values and sequence variables into separation logic. Our logic can simplify property expressions while enhancing the ability to describe these systems. To provide a theoretical foundation for verification, we study the decidability of this logic, with the main conclusions as follows. 1) The satisfiability problem of the fragment with a single quantifier alternation is decidable, and belongs to 2-EXPTIME (2-Exponential Time). As a by-product, we propose a decision procedure for this decidable fragment. 2) The satisfiability problem of the fragment with two quantifier alternations is undecidable.</p>

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

A Separation Logic for Sequences in Block-Based Cloud Storage Systems and Its Decidability

  • Tian-Yue Cao,
  • Bo-Wen Zhang,
  • Zhao Jin,
  • Yong-Zhi Cao,
  • Han-Pin Wang

摘要

Cloud storage systems are crucial for ensuring business stability and data reliability. Among them, block-based cloud storage systems (BCSSs) have been widely adopted in the industry due to their high efficiency and strong performance. However, system failures occur from time to time, causing significant financial losses to companies. Therefore, verifying the reliability of BCSSs has become important and urgent. Nevertheless, since blocks in these systems are of finite but variable sizes, it is difficult to describe and verify properties using first-order logic or separation logic. To address this issue, we propose Sequence-Heap Separation Logic (SeqSL), which introduces sequence values and sequence variables into separation logic. Our logic can simplify property expressions while enhancing the ability to describe these systems. To provide a theoretical foundation for verification, we study the decidability of this logic, with the main conclusions as follows. 1) The satisfiability problem of the fragment with a single quantifier alternation is decidable, and belongs to 2-EXPTIME (2-Exponential Time). As a by-product, we propose a decision procedure for this decidable fragment. 2) The satisfiability problem of the fragment with two quantifier alternations is undecidable.