diff options
| author | Dmitry Torokhov <dmitry.torokhov@gmail.com> | 2020-01-31 17:42:33 -0800 |
|---|---|---|
| committer | Dmitry Torokhov <dmitry.torokhov@gmail.com> | 2020-01-31 17:42:33 -0800 |
| commit | b19efcabb587e5470a423ef778905f47e5a47f1a (patch) | |
| tree | 8863c2233ed8a30d55c4e4029a98c3d7faf359a8 /tools/memory-model/linux-kernel.cat | |
| parent | 996d5d5f89a558a3608a46e73ccd1b99f1b1d058 (diff) | |
| parent | c5ccf2ad3d33413fee06ae87d0b970d8cc540db6 (diff) | |
Merge branch 'next' into for-linus
Prepare input updates for 5.6 merge window.
Diffstat (limited to 'tools/memory-model/linux-kernel.cat')
| -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 ea2ff4b94074..2a9b4fe4a84e 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -197,7 +197,7 @@ empty (wr-incoh | rw-incoh | ww-incoh) as plain-coherence (* Actual races *) let ww-nonrace = ww-vis & ((Marked * W) | rw-xbstar) & ((W * Marked) | wr-vis) let ww-race = (pre-race & co) \ ww-nonrace -let wr-race = (pre-race & (co? ; rf)) \ wr-vis +let wr-race = (pre-race & (co? ; rf)) \ wr-vis \ rw-xbstar^-1 let rw-race = (pre-race & fr) \ rw-xbstar flag ~empty (ww-race | wr-race | rw-race) as data-race |