A framework for semantic reasoning about Byzantine quorum systems
Evelyn Pierce, Lorenzo Alvisi · 2001
We present a set of definitions and theorems that allow us to reason about the semantics of quorum system variables, including Byzantine quorum system variables, as a class. Using these tools, we present a formal proof that the problem of atomic semantics for such variables can be reduced to the simpler problem of regular semantics for such systems. Specifically, any regular masking quorum system protocol can be combined with a writeback mechanism to produce an atomic protocol. We then describe a subclass of TS-variables for which the latter problem is not solvable by traditional approaches in an asynchronous environment. Finally, for such variables we define the notion of pseudoregular and pseudoatomic semantics, and show briey that the same reduction holds for these concepts.