diff options
| author | Ingo Molnar <mingo@kernel.org> | 2019-12-30 08:10:51 +0100 |
|---|---|---|
| committer | Ingo Molnar <mingo@kernel.org> | 2019-12-30 08:10:51 +0100 |
| commit | 28336be568bb473d16ba80db0801276fb4f1bbe5 (patch) | |
| tree | cf2d7a56e6c3ea08139d8d9a5a58b296bd172136 /tools/memory-model/linux-kernel.cat | |
| parent | 5cbaefe9743bf14c9d3106db0cc19f8cb0a3ca22 (diff) | |
| parent | fd6988496e79a6a4bdb514a4655d2920209eb85d (diff) | |
Merge tag 'v5.5-rc4' into locking/kcsan, to resolve conflicts
Conflicts:
init/main.c
lib/Kconfig.debug
Signed-off-by: Ingo Molnar <mingo@kernel.org>
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 |