基于分离逻辑的云存储系统并发正确性验证

摘要

云存储系统的应用日益广泛，其可靠性尤为受研究者关注。现有的基于块分离逻辑的验证方法能很好地描述和验证具备“文件-块-数据”三层架构的云存储系统的各类性质，文章在此基础上提出一种验证云存储系统并发正确性的方法，工作包括：(1)扩展云存储系统的建模语言，增加对线程间通信等并发行为的描述；(2)扩展断言语言，用于描述云存储环境下与并发执行和存储控制相关的系统性质；(3)提出一组霍尔规则，用于推导系统的性质。文章给出的验证实例能说明该方法的有效性。文章的工作扩展了块分离逻辑的适用范围，为MapReduce等框架下的并发程序正确性验证工作提供了理论基础。

关键词

分离逻辑 / 并发程序验证 / 云存储系统