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.展开更多
Transactional memory （TM） is an easy-using parallel programming model that avoids common problems associated with conventional locking techniques. Several researchers have proposed a large amount of alternative hard...Transactional memory （TM） is an easy-using parallel programming model that avoids common problems associated with conventional locking techniques. Several researchers have proposed a large amount of alternative hardware and software TM implementations. However, few ones focus on formal reasoning about these TM programs. In this paper, we propose a framework at assembly level for reasoning about lazy software transactional memory （STM） programs. First, we give a software TM implementation based on lightweight locks. These locks axe also one part of the shared memory. Then we define the semantics of the model operationally, and the lightweight locks in transaction axe non-blocking, avoiding deadlocks among transactions. Finally we design a logic -- a combination of permission accounting in separation logic and concurrent separation logic -- to verify various properties of concurrent programs based on this machine model. The whole framework is formalized using a proof-carrying-code （PCC） framework.展开更多
基金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.
基金Supported by the National Natural Science Foundation of China under Grant Nos.60928004 and 90718026
文摘Transactional memory （TM） is an easy-using parallel programming model that avoids common problems associated with conventional locking techniques. Several researchers have proposed a large amount of alternative hardware and software TM implementations. However, few ones focus on formal reasoning about these TM programs. In this paper, we propose a framework at assembly level for reasoning about lazy software transactional memory （STM） programs. First, we give a software TM implementation based on lightweight locks. These locks axe also one part of the shared memory. Then we define the semantics of the model operationally, and the lightweight locks in transaction axe non-blocking, avoiding deadlocks among transactions. Finally we design a logic -- a combination of permission accounting in separation logic and concurrent separation logic -- to verify various properties of concurrent programs based on this machine model. The whole framework is formalized using a proof-carrying-code （PCC） framework.
