Specific experiments

• Uncached memory type and SC
• Write combine memory type and the message passing litmus test
• Write combine memory type and the store buffer litmus test
• Write combine memory type and the TSO model

Uncached memory type and SC

Assigning the UC (Uncached) memory type to all variables is an expensive technique to ban non-SC behaviours.

Write combine memory type and the message passing litmus test

The table below shows that assigning the WC (Write Combined) memory type to any end of a write-to-write sequence relaxes the TSO write-to-write ordering. The relaxation is achieved more easily by assigning WC to the first write (MP+WC+WB below).

Write combine memory type and the store buffer litmus test

Those tests demonstrate that the WC (Write-Combine) memory types and the non-temporal store instruction operating on the default (WB) memory type may yield different results. More precisely the former corresponds the observed store-buffer tests SB+pontnas and SB+pontnts;¹ while the the latter corresponds to the non-observed store-buffer tests SB+WC+WC, SB+WC+WC+NT and SB+WC+WC+preload.

Write combine memory type and the TSO model

Those tests demonstrate that assigning the WC (Write-Combine) memory type to all variables in a tests yields a memory model which is neither stronger nor weaker than the base TSO model.