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

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.