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 stron...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.展开更多
基金supported by the National Key Research and Development Program of China under Grant 2022YFC2503903the National Natural Science Foundation of China under Grants 61972005,62302459,and 62172016.
文摘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.
