diff options
| author | Thomas Zimmermann <tzimmermann@suse.de> | 2023-03-13 10:14:05 +0100 |
|---|---|---|
| committer | Thomas Zimmermann <tzimmermann@suse.de> | 2023-03-13 10:14:05 +0100 |
| commit | b3c9a04135bdbd3aabd5e9534bad0fe6df505f8a (patch) | |
| tree | 2372cd098db2a0e45da99125258e454b827cb577 /tools/memory-model/linux-kernel.bell | |
| parent | fe9ae05cfbe587dda724fcf537c00bc2f287da62 (diff) | |
| parent | eeac8ede17557680855031c6f305ece2378af326 (diff) | |
Merge drm/drm-fixes into drm-misc-fixes
Backmerging to get latest upstream.
Signed-off-by: Thomas Zimmermann <tzimmermann@suse.de>
Diffstat (limited to 'tools/memory-model/linux-kernel.bell')
| -rw-r--r-- | tools/memory-model/linux-kernel.bell | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell index 5be86b1025e8..70a9073dec3e 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -82,3 +82,9 @@ flag ~empty different-values(srcu-rscs) as srcu-bad-nesting let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) | LKR | LKW | UL | LF | RL | RU let Plain = M \ Marked + +(* Redefine dependencies to include those carried through plain accesses *) +let carry-dep = (data ; rfi)* +let addr = carry-dep ; addr +let ctrl = carry-dep ; ctrl +let data = carry-dep ; data |