Multiprocessor architectures, such as Digital's Alpha [5], Sun's SPARC [8] and the PowerPC, consist of a number of processors that read and write a shared global memory. The documents that define them usually specify the behaviour of the shared memory via constraints on the sets of reads and writes. Formalisms such as process algebra or temporal logic, that are popular in the verification community, are not used. There is thus a `gap' between the models found in architecture manuals and those underlying standard verification technologies.
During a visit to DEC SRC in 1993 I started to look at this problem from a HOL perspective. What I did is written up in two unfinished papers: A formalization of a simplified subset of the Alpha shared memory model, and a Memory access semantics for a multiprocessor instruction set. Other people at SRC and elsewhere have been exploring different approaches. Particularly interesting is Corella, Stone and Barton's paper A formal specification of the PowerPC shared memory architecture (Francisco Corella is an ex HVG member and has also done interesting work on mechanizing set theory), the work of Attiya and Friedman on Programming Alpha based multiprocessors the easy way, some recent work by Manfred Broy on specifying the Alpha shared memory (Mike Gordon has a copy) and the HUG'94 paper Towards a HOL theory of memory [1].
One source of complexity in memory models is the behaviour of caches. An interesting project would be to specify a memory system with a cache and to show that it satisfies the axioms of an abstract memory model. This is related to cache coherency, see Section 3.3.