Noctua: Towards Automated and Practical Fine-grained Consistency Analysis

Relaxing strong consistency plays a vital role in achieving scalability and availability for geo-replicated web applications. However, making relaxation correct in modern implementations, typically written in dynamic languages and utilizing high-level object-oriented database abstractions, remains a challenge, despite the existence of numerous proposed analysis tools.

Here, we present a fully automated verification framework Noctua for understanding fine-grained consistency semantics in web applications. At its core is a simple intermediate representation SOIR that bridges the semantic gaps between high-level languages, database interactions and SMT solver's verification. Noctua's lightweight program analyzer reuses the ability of the language runtime and framework to translate consistency-related effects and application invariants from codebases into SOIR code. Finally, Noctua's verification backend maps SOIR code into SMT verification conditions with a new SMT encoding that decouples order information and thus allows more database semantics to be covered.

We have implemented Noctua 1 for a popular dynamic language, Python, and evaluated its correctness and applicability with two synthetic and four existing Python web applications. The evaluation results highlight that Noctua is able to understand consistency semantics considerably fast from the real codebases with no user input. For synthetic applications that existing solutions can be applied, Noctua's delivered consistent analysis results.

• Work done during his study at USTC.