Towards property-based consistency verification

Abstract

We propose a novel approach to the verification of consistency models implemented in distributed storage systems. We base our work on a declarative semantic model defining consistency conditions as predicates expressing ordering and visibility of operations. This model allows for a testing methodology focused on correctness properties rather than operational semantics. Finally, we present and discuss the design and preliminary implementation of a practical property-based consistency verification framework.