Sufficient System Requirements for Supporting the PLpc Memory Model
Sarita V. Adve, Kourosh Gharachorloo, Anoop Gupta, John LeRoy Hennessy, Mark D. Hill · 1993
The paper, Programming for Different Memory Consistency Models [GAG + 92], defines the PLpc memory model. This companion note formalizes the system requirements for PLpc along with a proof that shows these requirements are sufficient for supporting this model. In addition, we prove the correctness of the conditions presented in the original paper [GAG + 92] for porting PLpc programs to the various hardware-centric models. The reader should be familiar with the material in the original paper on PLpc [GAG + 92] before reading this supplement. 1 Introduction This is a supplementary note to the paper that defines the PLpc memory model [GAG + 92]. Section 2 provides a brief overview of the PLpc model along with the key definitions; a few definitions are changed slightly compared to the original versions to either address subtle correctness issues or to increase clarity. Section 3 specifies the sufficient system requirements for supporting PLpc; this specification is based upon a ge...