A Language For Fine-Grained Consistency In Distributed Systems:Design And Implementation

Modern large-scale Internet services rely on distributed data systems that maintain multiple copies of data.As the scale of the Internet continues to expand,to quickly re-spond user's request in different regions,Many Internet service providers replicate data across multiple geographically dispersed data centers and provide a weak consistency guarantee to reduce user-perceived latency.Although the weak consistency model is sufficient to meet the needs of certain application scenarios.But it still has limitations.Some applications may require stronger consistency.In this case,the distributed sys-tem needs to support multiple consistency at the same time to provide different consis-tency guarantees for data with different consistency requirements.Since the semantics provided by the weak consistency model and strong consistency model are different,Programmers need to determine whether their program can meet their semantic require-ments by running under different consistency models,such as invariant violation or state convergence.This brings new challenges to distributed system programming.To solve the above problems,firstly,this paper proposes a fine-grained consis-tency model and the corresponding programming language.The new language takes into account both practicality and expressive ability,allowing programmers to express the consistency semantics they expect and avoiding efficiency loss.Secondly,this pa-per presents some properties of the fine-grained consistency model for programmers to have a deeper understanding.Also,by using different synchronization sets and depen-dency sets in operations,we can make the server meet one of the existing data-centric consistency.Thirdly,this paper presents program logics for verifying the convergence and invariant preservation of a given program.We also give the soundness proof of these logics.The key lemma of the proof has been implemented in the proof assistant Coq,with a total of 3100 lines of proof scripts.Finally,this paper presents the design and implementation of a fine-grained consistency distributed system based on the above consistency model and programming language.The system was checked in the TLA+model checking tool,with a total of 1500 lines of code.The system is implemented in Java and has a total of approximately 5,300 lines of code.The experimental results under different workloads show the reliability and scalability of the system.