Design And Formal Verification Of An Effective Replicated Transaction System

With the advent of the era of big data,the importance of data storage has become higher,and the number of geo-replicated distributed databases has gradually increased.However,developing correct,scalable,and fault-tolerant distributed databases is hard and labor-intensive.As a prevalent transaction,RAMP(Read Atomic Multi-Partition)transaction is widely used in the research of distributed transaction system design.However,the two replicated RAMP transaction designs currently proposed by RAMP developers,PHR(Prepare-F HA RAMP)and SHR(Sticky HA RAMP),are only at the brief introduction stage without development or formal expression,and no work has been done to analyze the two replicated transaction designs for consistency properties and performance properties.Meanwhile,in order to ensure RA(Read Atomicity),PHR and SHR clients need to send requests twice while performing read operations,which will bring a high delay.The thesis proposes our own replicated transaction design SHR-Faster with lower latency based on the two replicated RAMP designs PHR and SHR.Compared with PHR and SHR,SHR-Faster reduces the number of client-server interactions during read requests on the basis of ensuring RA consistency.SHR-Faster not only satisfies the required data consistency,but also performs better in terms of performance.In the thesis we use formal modeling and model checking techniques to formalize designs of replicated RAMP transactions for geo-replicated databases and verify their consistency properties in order to prove that SHR-Faster satisfies the required consistency properties.The main idea is to formalize in Maude formal,executable specifications of three replicated RAMP designs.We then use Maude's LTL model checker and the CAT tool to analyze these specifications against data consistency properties such as the RA and the read your writes.Our model checking results show that SHR-Faster satisfies all expected consistency properties.Last,the thesis verifies that our promising design has more desirable performance with lower latency compared to PHR and SHR through statistical model checking(SMC).The main approach is to transform the above untimed,non-probabilistic,and nondeterministic Maude models into timed and purely probabilistic models,and then subject the probabilistic models of three designs to realistic transaction workloads with a wider range of experimental parameters.Our SMC analysis result shows that SHRFaster incurs less transaction latency than the other designs under all experiments.