diff options
Diffstat (limited to 'tools/memory-model/linux-kernel.bell')
| -rw-r--r-- | tools/memory-model/linux-kernel.bell | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell index 7c9ae48b9437..8ae47545df97 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -94,3 +94,6 @@ let carry-dep = (data ; [~ Srcu-unlock] ; rfi)* let addr = carry-dep ; addr let ctrl = carry-dep ; ctrl let data = carry-dep ; data + +flag ~empty (if "lkmmv2" then 0 else _) + as this-model-requires-variant-higher-than-lkmmv1 |