Formalization and Verification of Percolator Using CSP

Percolator is a distributed transaction model pro-posed by Google to deal with large-scale incremental data of search engines. Based on timestamps, it achieves the snapshot isolation level of multi-version concurrency control. Percolator also inspired distributed transaction models for many databases such as TiDB. In this paper, we model the architecture of Percola-tor using process algebra CSP and implement it with the help of the Process Analysis Toolkit (PAT). Subsequently, we verify and analyze several properties, including deadlock-free, divergence-free, consistency, and snapshot isolation. The verification results show that Percolator satisfies the above properties, but is not serializable, which may lead to data anomalies in some cases.