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, Noctua designs a simple language SOIR, serving as an intermediate representation that bridges the semantic gaps between application codebase comprised by high-level language logics and database interactions, and SMT solver's verifiable instructions. Furthermore, we propose a light-weight program analyzer at the front-end, which re-uses the ability of the application development framework to translate consistency-related side effects and application invariants from codebase into SOIR code. Finally, we leverage a powerful SMT solver, Z3, to build our verification backend, which directly maps SOIR code into Z3 code efficiently with a new SMT encoding that decouples order information from object data, leading to an remarkable increase in the coverage of database semantics. We have implemented Noctua 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 from the real codebases with no user input. For synthetic applications that existing solutions can be applied, Noctua's delivered consistent analysis results. In contrast, Noctua is able to analyze real-world applications from GitHub while baseline systems fail to do so. In addition, we also demonstrated that Noctua's analysis and verification performance is considerably fast.