Multithreaded servers with shared memory are the dominant type of 
machines used to run critical network services and database management 
systems. To achieve the high availability required for these tasks it is necessary 
to incorporate mechanisms for error detection and recovery. The goal of my 
second year project was to develop a scheme for dynamic verification of memory 
systems for multithreaded servers. Since the memory consistency model 
defines end-to-end correctness of a shared memory system, dynamic verification 
of memory consistency can comprehensively detect errors in the memory system.

I will present a framework for dynamic verification of memory 
consistency (DVMC) in cache-coherent multithreaded systems. Three basic system properties 
are shown to be sufficient for ensuring memory consistency and a simple 
verification mechanism is given for each property. The framework can be applied to a 
wide range of memory consistency models by using a general method for 
describing ordering requirements.

In addition to a theoretical description of the verification 
mechanisms, I will describe an efficient implementation of the framework on a SPARC-based 
SMP. Simulation results show that the performance overhead is generally 
low and implementation costs are far from prohibitive, affirming the 
supposition that the availability and safety benefits gained from 
adding dynamic verification of consistency to a multithreaded server far outweigh the incurred costs.