diff options
Diffstat (limited to 'tools/memory-model')
| -rw-r--r-- | tools/memory-model/linux-kernel.cat | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat index 3a4d3b49e85c..cfc1b8fd46da 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -81,7 +81,7 @@ let dep = addr | data let rwdep = (dep | ctrl) ; [W] let overwrite = co | fr let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb) -let to-r = addr | (dep ; [Marked] ; rfi) +let to-r = (addr ; [R]) | (dep ; [Marked] ; rfi) let ppo = to-r | to-w | fence | (po-unlock-lock-po & int) (* Propagation: Ordering from release operations and strong fences. *) |