diff options
| author | Daniel Baumann <daniel.baumann@progress-linux.org> | 2024-08-07 13:18:06 +0000 |
|---|---|---|
| committer | Daniel Baumann <daniel.baumann@progress-linux.org> | 2024-08-07 13:18:06 +0000 |
| commit | 638a9e433ecd61e64761352dbec1fa4f5874c941 (patch) | |
| tree | fdbff74a238d7a5a7d1cef071b7230bc064b9f25 /tools/memory-model/lock.cat | |
| parent | Releasing progress-linux version 6.9.12-1~progress7.99u1. (diff) | |
| download | linux-638a9e433ecd61e64761352dbec1fa4f5874c941.tar.xz linux-638a9e433ecd61e64761352dbec1fa4f5874c941.zip | |
Merging upstream version 6.10.3.
Signed-off-by: Daniel Baumann <daniel.baumann@progress-linux.org>
Diffstat (limited to 'tools/memory-model/lock.cat')
| -rw-r--r-- | tools/memory-model/lock.cat | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat index 53b5a49273..21ba650869 100644 --- a/tools/memory-model/lock.cat +++ b/tools/memory-model/lock.cat @@ -102,19 +102,19 @@ let rf-lf = rfe-lf | rfi-lf * within one of the lock's critical sections returns False. *) -(* rfi for RU events: an RU may read from the last po-previous UL *) -let rfi-ru = ([UL] ; po-loc ; [RU]) \ ([UL] ; po-loc ; [LKW] ; po-loc) - -(* rfe for RU events: an RU may read from an external UL or the initial write *) -let all-possible-rfe-ru = - let possible-rfe-ru r = +(* + * rf for RU events: an RU may read from an external UL or the initial write, + * or from the last po-previous UL + *) +let all-possible-rf-ru = + let possible-rf-ru r = let pair-to-relation p = p ++ 0 - in map pair-to-relation (((UL | IW) * {r}) & loc & ext) - in map possible-rfe-ru RU + in map pair-to-relation ((((UL | IW) * {r}) & loc & ext) | + (((UL * {r}) & po-loc) \ ([UL] ; po-loc ; [LKW] ; po-loc))) + in map possible-rf-ru RU (* Generate all rf relations for RU events *) -with rfe-ru from cross(all-possible-rfe-ru) -let rf-ru = rfe-ru | rfi-ru +with rf-ru from cross(all-possible-rf-ru) (* Final rf relation *) let rf = rf | rf-lf | rf-ru |