PLDI11 vs. Model


This note lists the differences between ppcmem, the simulator of the PLDI11 model, and herd (on the Power architecture). Notice that ppcmem does not always terminate in the allocated time and memory bounds, so that this comparison does not cover all our test set.

Checking PLDI11 against Model

More behaviours

We take the following, quite unexpected, behaviour to be a bug of ppcmem, as eieio was added afterhand.

There is one such test
Z6.1+sync+eieio+addrAllowForbidNo, 0/3.9GNo, 0/1.0GNo, 0/27G
   Allow unseenAllow unseenAllow unseen

Morever, if we replace eieio by lwsync the resulting test Z6.1+sync+lwsync+addr is forbidden by the two models. We see no reason for eieio and lwsync to differ here.

There is one such test

Less behaviours

The following table lists the behaviours that are allowed by our model yet forbidden by PLDI’11:

There are 4 such tests
MP+sync+ctrl-detrForbidAllowNo, 0/3.1GOk, 12k/34G
   Allow unseen  
DETOUR0821ForbidAllowOk, 2/3.6GNo, 0/3.4GOk, 25k/43G
    Allow unseen 
MP+lwsync+addr-po-detrForbidAllowOk, 3/2.9GOk, 21k/31G
MP+sync+addr-po-detrForbidAllowOk, 1/2.9GOk, 17k/31G

As those behaviours are observed on Power7 hardware, the above table also demonstrates that the PLDI’11 model is invalidated by hardware experiments.

This document was translated from LATEX by HEVEA.