summaryrefslogtreecommitdiff
path: root/tools/memory-model
diff options
context:
space:
mode:
Diffstat (limited to 'tools/memory-model')
-rw-r--r--tools/memory-model/README8
-rw-r--r--tools/memory-model/linux-kernel.cat2
-rw-r--r--tools/memory-model/lock.cat3
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"