Shared memory multiprocessors implement a simple view of shared memory
for the programmer. This view should abstract away from the underlying
hardware and the protocol implemented on it. A classical shared memory
model is sequential consistency. I am looking at the problem of
verifying that all traces of a shared memory system are sequentially
consistent.  A memory system is typically parameterized by three
parameters - number of processors, number of memory locations, and
number of data values that can be stored at each memory location. 
For a given memory system, we would like to prove sequential consistency for all 
values of the parameters. 
We have some preliminary results where we were able to prove sequential consistency 
for two example protocols - lazy caching and snoopy cache coherence. Our methodology 
involves induction over the number of processors and the use of sufficient conditions 
that let us conclude sequential consistency for any number of memory locations and
data values by proving it for a fixed number. These results have been reported in the 
following.

<ul>
<li> T.A. Henzinger, S. Qadeer, S.K. Rajamani.
<b> Verifying Sequential Consistency on Shared Memory Multiprocessors.</b>
Submitted to the Conference on Computer-Aided Verification, 1999.
</ul>