Automated Analysis And Reasoning Of Fine-Grained Distributed Consistency Semantics

Since the 21st century,the Internet has flourished,giving rise to a large number of Internet services and applications,such as various social networking sites,online streaming sites,e-commerce sites,and so on.And as technology advances and the cost of using computers and networks continues to fall,the number of users that need to be served by various Internet services continues to rise.The large number of users poses serious challenges to all kinds of Internet services:they need to be able to accommodate to meet the huge number of users and also to respond to the huge number of requests from users in a timely manner.In this context,sacrificing consistency for better system availability and scalability has become an appropriate choice for contemporary Internet services,and the traditional strong consistency model is gradually replaced by the weak consistency model.However,it is not obvious to use the weak consistency correctly,which is not only error-prone,but also quite tedious and boring.And weak consistency,if used incorrectly,can affect system performance at best,or cause economic loss at worst.Thus,the automated analysis of weak consistency becomes an urgent need.Although many automated or semi-automated solutions have been proposed so far,they are not practical for existing codebases of real projects due to various drawbacks.In order to solve the problem of consistency analysis of existing codebases of real applications,this thesis proposes a modular and fully automated analysis framework for fine-grained consistency analysis.The framework works by first converting the source code of the application into a unified intermediate representation language through program analysis to encode the semantics of database accesses in the application,then generating the consistency verification conditions from the intermediate representation and the consistency checking rules,and finally completing the automated consistency verification by invoking an automated theorem prover.The framework can eventually output a configuration for a fine-grained consistency model,so that the application can be easily deployed as a weakly-consistent geo-replicated distributed system,obtaining performance benefits for free without sacrificing the correctness.The framework consists of three components:(1)the thesis proposes an intermediate representation language.The IR language is able to encode most of the objectoriented semantics of database access,and admits a straightforward and efficient SMT encoding,which can optimize the reasoning process of the SMT solver.(2)The thesis proposes an efficient analysis framework which works well for dynamic languages like Python.Additionally,our analysis adopts a co-design strategy with the framework,where the framework embeds the analysis code,effectively reducing the workload of the analyzer,and greatly improving the analysis precision at the same time.This method also enables the run-time reproduction of the analysis results,making the framework aware which code path the program is in,so as to select the appropriate distributed coordination strategy.(3)The thesis designed an automated consistency verifier suitable for a fine-grained consistency model.It works by invoking an SMT solver.Apart from the optimized SMT encoding,it incorporates new checking rules,further relaxing the weakest consistency model assumed from causal consistency to eventual consistency when compared with the state-of-the-art automated consistency verification tool.