|
@@ -1,15 +1,15 @@
|
|
- =========================
|
|
|
|
- LINUX KERNEL MEMORY MODEL
|
|
|
|
- =========================
|
|
|
|
|
|
+ =====================================
|
|
|
|
+ LINUX KERNEL MEMORY CONSISTENCY MODEL
|
|
|
|
+ =====================================
|
|
|
|
|
|
============
|
|
============
|
|
INTRODUCTION
|
|
INTRODUCTION
|
|
============
|
|
============
|
|
|
|
|
|
-This directory contains the memory model of the Linux kernel, written
|
|
|
|
-in the "cat" language and executable by the (externally provided)
|
|
|
|
-"herd7" simulator, which exhaustively explores the state space of
|
|
|
|
-small litmus tests.
|
|
|
|
|
|
+This directory contains the memory consistency model (memory model, for
|
|
|
|
+short) of the Linux kernel, written in the "cat" language and executable
|
|
|
|
+by the externally provided "herd7" simulator, which exhaustively explores
|
|
|
|
+the state space of small litmus tests.
|
|
|
|
|
|
In addition, the "klitmus7" tool (also externally provided) may be used
|
|
In addition, the "klitmus7" tool (also externally provided) may be used
|
|
to convert a litmus test to a Linux kernel module, which in turn allows
|
|
to convert a litmus test to a Linux kernel module, which in turn allows
|