Weak shared memory consistency models, especially those used by modern microprocessor families, are quite complex. The bus and/or directory-based protocols that help realize shared memory multiprocessors using these microprocessors are also exceedingly complex. Thus, the correctness problem - that all the executions generated by the multiprocessor for any given concurrent program are also allowed by the memory model - is a major challenge. In this paper, we present a formal approach to verify protocol implementation models against weak shared memory models through automatable refinement checking supported by a model checker. We define a taxonomy of weak shared memory models that includes most published commercial memory models, and detail how our approach applies over all these models. In our approach, the designer follows a prescribed procedure to build a highly simplified intermediate abstraction for the given implementation. The intermediate abstraction and the implementation are concurrently run using a model-checker, checking for refinement. The intermediate abstraction can be proved correct against the memory model specification using theorem proving. We have verified four different Alpha as well as Itanium memory model implementations against their respective specifications. The results are encouraging in terms of the uniformity of the procedure, the high degree of automation, acceptable run-times, and empirically observed bug-hunting efficacy. The use of parallel model-checking, based on a version of the parallel MurΦ model checker we have recently developed for the MPI library, has been essential to finish the search in a matter of a few hours.
展开▼
