Or, when do we need LoadStore barrier?
According to Doug Lea,
(LoadStore) ensures that Load1's data are loaded before all data associated with Store2 and subsequent store instructions are flushed
So, it seems that the result of the load is only available after the store is finished.
After all, the result of the load could be at stale status until the last moment before the store finished.
So in my opinion, this barrier only works for the following pattern:
load r1 [x1]; // load operation
#LoadStore barrier
store [y1] r2; // store operation
...
//other operations really need newest [x1]
...
Is this example correct? Please correct me if not.
Also, can you provide a specific situation where this pattern occurs?
I really appreciate any advice or suggestion.
Also, can you provide a specific situation where this pattern occurs?
Envisions a 'read copy update' list. A process gets a current version of the list with a 'load' and it 'stores' the version to reserve it in another structure or location. After this is complete, the process can use that version of the list.
The important point is that different time orders of memory can exist. So the 'load store' pattern needs to take account of other processing performing accesses to the same memory. In this case, some update of the version could cause an inconsistency. But mainly the 'load/store' by itself is not the issue. It is the global management of the information.
I think there are many other patterns. For instance Dr Alglave's paper Herding Cats in Fig 4. has some tables that should be familiar with Doug Lea's Java memory model page you cite. Specifically the 'R/W' is used for load buffering (duplicate 'R/W' ordering) and other patterns such as write to read causality. If you look at chapter 9, you can find reference to different open source 'C' programs which were scanned for these patterns with cbmc (also seems to be ported to esbmc).