title: The Operational POWER/ARM Model --- Model Changelog and Options
author: Susmit Sarkar
date: 2014-08-05

This document adds to the prose description of the operational model. Here we note the major changes made to the model, and some ways of recovering older deprecated behaviour within our PPCMEM tool.

Changelog (inclusive of PPCMEM bug fixes)

Roughly in reverse-chronological order, since PLDI'11:

--- the following two were described in our PLDI'12 paper ---

Model Options

With the (old) model option barrier_coherence_weak, Precondition 5 of Accept a Successful Write-Conditional Request was absent, and Precondition 3 of Write Reaching its Coherence only asked for a barrier from the writing thread. This version describes the (default) barrier_coherence_strong model option.

Action 1 of Satisfy Memory Read from Storage Subsystem is not done for the (old, buggy) model option restart_on_read_commit. Correspondingly, the Commit Instruction has an additional action: for a read, restart all in-flight memory reads and read-reserves that have read from a different write to the same address (unless that read read-from an in-flight write). This version describes the (default) model option restart_on_read_satisfy.