Comparison with Power hardware

• Invalid behaviours, herd model
• Invalid behaviours, experimental model

We witness a few model invalidations. Those are due to a difference in the reservation granularity: our models assume that, if a reservation and a store conditonal are made to different addresses, then the store conditional will always fail. By contrast, hardware reservations are at an unspecified granularity, likely a cache line. As a consquence, if two different locations x and y happen to reside in the same cache line, reserving location x and then attempting a store conditional on location y may succeed.

Invalid behaviours, herd model

The following table lists the behaviours that are forbidden by herd model model, yet observed on hardware.

Invalid behaviours, experimental model

The following table lists the behaviours that are forbidden by herd experimental model, yet observed on hardware.