diff options
| -rw-r--r-- | tools/memory-model/README | 8 | ||||
| -rw-r--r-- | tools/memory-model/linux-kernel.cat | 2 | ||||
| -rw-r--r-- | tools/memory-model/lock.cat | 3 |
3 files changed, 6 insertions, 7 deletions
diff --git a/tools/memory-model/README b/tools/memory-model/README index 9d7d4f23503f..2b87f3971548 100644 --- a/tools/memory-model/README +++ b/tools/memory-model/README @@ -20,13 +20,17 @@ that litmus test to be exercised within the Linux kernel. REQUIREMENTS ============ -Version 7.49 of the "herd7" and "klitmus7" tools must be downloaded -separately: +Version 7.52 or higher of the "herd7" and "klitmus7" tools must be +downloaded separately: https://github.com/herd/herdtools7 See "herdtools7/INSTALL.md" for installation instructions. +Note that although these tools usually provide backwards compatibility, +this is not absolutely guaranteed. Therefore, if a later version does +not work, please try using the exact version called out above. + ================== BASIC USAGE: HERD7 diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat index 95bf45f1215f..8dcb37835b61 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -1,7 +1,5 @@ // SPDX-License-Identifier: GPL-2.0+ (* - * Requires herd version 7.51+6 or higher. - * * Copyright (C) 2015 Jade Alglave <j.alglave@ucl.ac.uk>, * Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria * Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>, diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat index 305ded17e741..a059d1a6d8a2 100644 --- a/tools/memory-model/lock.cat +++ b/tools/memory-model/lock.cat @@ -6,9 +6,6 @@ (* * Generate coherence orders and handle lock operations - * - * Warning: spin_is_locked() crashes herd7 versions strictly before 7.48. - * spin_is_locked() is functional from herd7 version 7.49. *) include "cross.cat" |