diff options
| author | Dmitry Torokhov <[email protected]> | 2020-01-10 14:56:04 -0800 |
|---|---|---|
| committer | Dmitry Torokhov <[email protected]> | 2020-01-10 14:56:04 -0800 |
| commit | 1bdd3e05a0a3b4a97ea88bc46fef8fb265c8b94c (patch) | |
| tree | 2244894a9ea0c941a8f32e5f3d196b4ea0eae24b /tools/memory-model/linux-kernel.cat | |
| parent | 643dd7416649bea2e8c61d8fdeeefb409a0ca5eb (diff) | |
| parent | c79f46a282390e0f5b306007bf7b11a46d529538 (diff) | |
Merge tag 'v5.5-rc5' into next
Sync up with mainline to get SPI "delay" API changes.
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 |