[PATCH] advsync: Adjust context to herd7 litmus test

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

 



>From 3db6dc5ae7f71c42f91742064ec38db750f3f25d Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@xxxxxxxxx>
Date: Mon, 26 Jun 2017 22:33:30 +0900
Subject: [PATCH] advsync: Adjust context to herd7 litmus test

Commit 96ab6febd94c ("advsync: Convert memory-misordering table to
herd7 litmus test") needs further adjustment.

Signed-off-by: Akira Yokosawa <akiyks@xxxxxxxxx>
---
 advsync/memorybarriers.tex | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/advsync/memorybarriers.tex b/advsync/memorybarriers.tex
index e9e9de1..4a2c334 100644
--- a/advsync/memorybarriers.tex
+++ b/advsync/memorybarriers.tex
@@ -50,7 +50,7 @@ code that makes direct use of explicit memory barriers for data structures
 in shared memory.
 For example, the litmus test in
 Figure~\ref{fig:advsync:Memory Misordering: Store-Buffering Litmus Test}
-appears to guarantee that the assertion never fires.
+appears to guarantee that the \co{exists} clause is never validated.
 After all, if \nbco{0:r2=0},\footnote{
 	That is, Thread~\co{P0()}'s instance of local variable \co{r2}
 	equals zero.
@@ -60,10 +60,10 @@ as shown in the \co{exists} clause, we might hope that Thread~\co{P0()}'s
 load from~\co{x1} must have happened before Thread~\co{P1()}'s store to~\co{x1},
 which might raise
 further hopes that Thread~\co{P1()}'s load from~\co{x0} must happen after
-Thread~\co{P0()}'s store to~\co{x0}, so that \nbco{1:r2=0}, as required by the
-assertion.
+Thread~\co{P0()}'s store to~\co{x0}, so that \nbco{1:r2=2},
+which should negate the \co{exits} clause.
 The example is symmetric, so similar hopeful reasoning might lead
-us to hope that \nbco{1:r2=0} guarantees that \nbco{0:r2=1}.
+us to hope that \nbco{1:r2=0} guarantees that \nbco{0:r2=2}.
 Unfortunately, the lack of memory barriers in
 Figure~\ref{fig:advsync:Memory Misordering: Store-Buffering Litmus Test}
 dashes these hopes.
-- 
2.7.4

--
To unsubscribe from this list: send the line "unsubscribe perfbook" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at  http://vger.kernel.org/majordomo-info.html



[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Index of Archives]     [Linux NFS]     [Linux NILFS]     [Linux USB Devel]     [Video for Linux]     [Linux Audio Users]     [Yosemite News]     [Linux Kernel]     [Linux SCSI]

  Powered by Linux