Formalization and verification of shared memory
Sanesh C. Gopalakrishnan, Ali Sezgin · 2004
Shared memory verification, checking the conformance of an implementation to a shared memory model, is an important, albeit complex on many levels, problem. One of the major reasons for this complexity is the implicit manipulation of semantic constructs to verify a memory model, instead of the desired syntactic methods, as they are amenable to be mechanized. The work presented in this dissertation is mainly aimed at reformulating shared memory verification through a new formalization so that the modified presentation of the problem manifests itself as purely syntactic. (Shared) memories are viewed as structures that define relations over the set of programs, an ordered set of instructions, and their executions, an ordered set of responses. As such, specifications (basically memory models that describe the set of executions considered correct with respect to a program) and implementations (that describe how an execution relates to a program both temporally and logically) have the same semantic basis. However, whereas a specification itself is described as a relation, an implementation is modelled by a transducer, where the relation it realizes is its language. This conscientious effort to distinguish between specification and implementation is not without merit: a memory model needs to be described and formalized only once, regardless of the implementation whose conformance is to be verified. Once the framework is constructed, shared memory verification reduces to language inclusion; that is, checking whether the relation realized by the implementation is a subset of the memory model. The observation that a specification can be approximated by an infinite hierarchy of finite-state transducers (implementations), called the memory model machines, results in the aforementioned syntactic formulation of the problem: regular language inclusion between two finite-state automata where one automaton has the same language (relation) as the implementation and the other has the same language as one of the memory model machines. On a different level but still related to shared memory verification, the problem of checking the interleaved-sequentiality of an execution (an execution is interleaved-sequential if it can be generated by a sequentially consistent memory), is considered. The problem is transformed into an equivalent constraint satisfaction problem. Thanks to this transformation, it is proved that if a memory implementation generates a non interleaved-sequential and unambiguous execution (no two writes in the execution have the same address and data values), then it necessarily generates one such execution of bounded size, the bound being a function of the address and the data spaces of the implementation.