Nine Shades of RAM

Abstract

The processors of multi-core machines communicate via a shared memory in a highly nontrivial way. Thus, not surprisingly, memory components play an important role in the construction of such machines. We start in Sect. 4.1 with a basic construction of (static) random access memory (RAM). Next, we derive in Sect. 4.2 five specialized designs: read only memory (ROM), multi-bank RAM, cache state RAM, and special purpose register RAM (SPR RAM). In Sect. 4.3 we then generalize the construction to multi-port RAM; this is RAM with more than one address and data port. We need multi-port RAMs in 4 flavours: 3-port RAM for the construction of general purpose register files, general 2-port RAM, 2-port combined multi-bank RAM-ROM, and 2-port cache state RAM.

For the correctness proof of a RAM construction, we consider a hardware configuration h which has the abstract state of the RAM h.S as well as the hardware components implementing this RAM. The abstract state of the RAM is coupled with the state of its implementation by means of an abstraction relation. Given that both the abstract RAM specification and RAM implementation have the same inputs, we show that their outputs are also always the same.

The material in this section builds clearly on [12]. The new variations of RAMs (like general 2-port RAM or 2-port cache state RAM), that we have introduced, are needed in later chapters. Correctness proofs for the various flavours of RAM are quite similar. Thus, if one lectures about this material, it suffices to present only a few of them in the classroom.

The title of this chapter is inspired by the song “Forty Shades of Green” written in 1959 by Johnny Cash and not by a recent novel.