A Novel Two-Layer Concurrent Distributed Algorithm Based On Shared Memory For Formal Verification

With the advent of time-sharing systems and applications that support computer hardware interacting with external environments,concurrent distributed algorithms become more and more important,it is widely used in the concurrent distributed system,cloud computing system,reactive system,blockchain and so on.Formal methods develop and validates algorithms,software,or systems based on mathematical logic,and supports verification activities such as functional correctness,security,and activity by constructing and transforming protocols for algorithms,software,or systems.This paper focuses on the formal verification of the functional correctness of concurrent distributed algorithms based on shared variables.Based on the research team's existing work on formal specification languages and methods,formal derivation and verification of algorithms,a custom generic abstract sequential programming language(APLA)was developed.Firstly,based on the APLA language,the Concurrency operator is extended to the Concurrency APLA language,and its structured operation semantics is given.Secondly,based on the Rely-Guarantee reasoning method,a concurrent distributed algorithm with two shared variables is proposed to verify its correctness.The two layers are the system layer and the component layer,in which the system layer deals with the correctness verification of the concurrent level,that is,the interaction of multiple components,and the component layer deals with the sequence level,that is,the correctness verification of a single component.Then,the similarities and differences between the loop invariants of component-level loop code snippets and the loop invariants of sequential programs are discussed,the verification method of the concurrent distributed algorithm proposed in this paper can fuse the cyclic invariant strategy of sequential programs well.Finally,some concurrent algorithms are parameterized and validated by the characteristics of Concurrency Apla generic programming,so that they can adapt to multi-thread Concurrency and become more universal.In contrast to other approaches,this article deals with concurrent interleaving of threads,allowing interference between threads rather than avoiding interference.This interference uses the dependent predicate and the guarantee predicate in the RelyGuarantee reasoning method for record description.The method does not interfere with Freedom testing,is well composable and inherits the advantages of Hoare logic.For code fragments with loops,the new loop-invariant development strategy proposed by the research team applies to the Hoare logic,which can smoothly migrate to the development of loop-invariant code in the component layer of the concurrent program.