Formal Semantics And Verification Of Weak Memory Models

The memory consistency model of a shared memory multiprocessor specifies how memory accesses are made during program execution.It can help programmers to have a precise notion of shared memory semantics,and then write correct and efficient concurrent programs.Modern hardware architectures and programming languages employ weak(aka relaxed)memory models.They are used to increase the performance of concurrent programs by allowing program instructions to be executed in a different order to that specified by the programs.For weak memory models,prose-style definition is error prone and leads to ambiguity.Therefore,one of the interesting researches is giving a clear and rigorous description of weak memory models.In this thesis,we focus on weak memory models,including the Total Store Order(TSO)memory model,the Partial Store Order(PSO)memory model and the ARMv8 memory model supported by hardware architectures,and the C++11 memory model introduced by the C++11 standard.Different weak memory models bring in different relaxed-memory effects.TSO is a widely used weak memory model in x86 architecture.It omits store-load constraint by allowing each thread to employ a write buffer.The PSO memory model is similar to TSO.And the difference is that PSO does not guarantee that stores to different locations propagate to the shared memory in the order they were issued.The ARMv8 memory model defined by ARM architecture produces relaxedmemory effects through thread-local out-of-order,speculative execution and threadlocal buffering.Promising semantics proposed by Kang et al.provided the operational semantics for the C++11 memory model,and exhibited the relaxed-memory effects of C++11 by introducing the concepts of promise and timestamp.This thesis investigates the weak memory models by using formal methods,including the formal semantics,modeling and verification of weak memory models.For formal semantics,we apply Unifying Theories of Programming(UTP)to study the trace semantics,algebraic semantics and the linking between the two semantics for the weak memory models,and then the weak memory models can be described rigorously from different perspectives.Trace semantics refers to the traditional denotational semantics,and a trace is expressed as a sequence of snapshots.Program properties are usually expressed as algebraic laws(equations).In order to support the investigation of algebraic laws,we introduce the concepts of guarded choice and head normal form.This thesis also considers the linking between trace semantics and algebraic semantics.The linking is achieved through deriving trace semantics from algebraic semantics.Based on Communicating Sequential Processes(CSP),this thesis proposes the system modeling framework of the PSO memory model.In the model checker Process Analysis Toolkit(PAT),we verify the properties related to the reordering feature of PSO.The main contributions of this thesis include:· This thesis investigates the trace semantics,algebraic semantics and the linking between the two semantics for the TSO memory model,which can support to model the reordering in the TSO memory model.The store-load constraint is relaxed because of the write buffer in each thread.Aiming at this feature,considering trace semantics,we first generate all the traces of a program by using a variant of the traditional interleaving semantics,and then all the valid traces can be achieved,after kicking out those that do not satisfy program order and modification order.During the investigation of sequential and parallel expansion laws,all the actions in any sequential program under TSO can be exhibited using a vertical tree structure.· This thesis studies the trace semantics,algebraic semantics and the linking between the two semantics for the ARMv8 memory model,which is a basis of the formal model of ARMv8's relaxed-memory effects.Moreover,on the basis of the theoretical investigation of algebraic semantics,we implement the algebraic laws of ARMv8 in the rewriting engine Maude.Under the ARMv8 memory model,thread-local out-of-order,speculative execution and thread-local buffering may bring in relaxed-memory effects.Then,we study the trace semantics for the basic statements,and then explore the trace semantics for the programs under ARMv8 with the analysis of a variety of dependencies among program statements.When considering algebraic laws,the actions under ARMv8 are shown with a horizontal tree structure.· This thesis investigates the trace semantics and algebraic semantics for the C++11 memory model.The above method is scalable,which is suit for the relaxed memory ordering and release/acquire memory ordering under C++11.According to promising semantics,this thesis investigates the trace semantics for the C++11memory model,by using the concepts of promise,timestamp and thread view.Considering algebraic semantics,due to the highly abstract nature of the C++11memory model,we define a read mechanism for each variable in the generated configuration sequences under C++11.Consequently,the valid execution results of any program under this memory model can be provided,based on the achieved algebraic laws.· This thesis applies CSP to abstract and formalize the PSO memory model,which supports the verification of the properties related to the reordering feature of PSO.We summarize the behaviors of four core components,and then give the formal model of PSO with channel communication by the process algebra CSP.Finally,we use the model checking tool PAT to verify four related properties.