From c41734f251d075236a28d712496a58ddd21fdedc Mon Sep 17 00:00:00 2001 From: Michael Walker Date: Thu, 2 Nov 2017 21:34:34 +0000 Subject: [PATCH] Make write/commit dependency avoidance less widely applicable It was probably unsound before. --- dejafu/Test/DejaFu/SCT/Internal.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/dejafu/Test/DejaFu/SCT/Internal.hs b/dejafu/Test/DejaFu/SCT/Internal.hs index 02f0a04..963e9d9 100644 --- a/dejafu/Test/DejaFu/SCT/Internal.hs +++ b/dejafu/Test/DejaFu/SCT/Internal.hs @@ -668,8 +668,8 @@ dependentActions memtype ds a1 a2 = case (a1, a2) of -- empty. -- -- See [RMMVerification], lemma 5.25. - (UnsynchronisedWrite r1, _) | same crefOf && isCommit a2 r1 && isBuffered ds r1 -> False - (_, UnsynchronisedWrite r2) | same crefOf && isCommit a1 r2 && isBuffered ds r2 -> False + (UnsynchronisedWrite r1, PartiallySynchronisedCommit _) | same crefOf && isBuffered ds r1 -> False + (PartiallySynchronisedCommit _, UnsynchronisedWrite r2) | same crefOf && isBuffered ds r2 -> False -- Unsynchronised reads where a memory barrier would flush a -- buffered write