barrucadu/dejafu
1
1
Fork 0
mirror of https://github.com/barrucadu/dejafu.git synced 2025-01-05 04:05:17 +03:00
Code Issues Projects Releases Wiki Activity

Add missing symmetric cases to dependentActions

Browse Source
This commit is contained in:
Michael Walker 2015-11-30 16:30:16 +00:00
parent efa65859b1
commit 917c8a3954
1 changed files with 2 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
dejafu/Test/DejaFu/SCT/Internal.hs
View File

@ -329,11 +329,13 @@ dependentActions memtype buf a1 a2 = case (a1, a2) of
-- a relaxed memory model, as an unsynchronised write gives rise to
-- a commit, which synchronises.
(UnsynchronisedRead r1, UnsynchronisedWrite r2) -> r1 == r2
(UnsynchronisedWrite r1, UnsynchronisedRead r2) -> r1 == r2
(UnsynchronisedWrite r1, UnsynchronisedWrite r2) -> r1 == r2
-- Unsynchronised reads where a memory barrier would flush a
-- buffered write
(UnsynchronisedRead r1, _) | isBarrier a2 -> isBuffered buf r1 && memtype /= SequentialConsistency
(_, UnsynchronisedRead r2) | isBarrier a1 -> isBuffered buf r2 && memtype /= SequentialConsistency
(_, _)
-- Two actions on the same CRef where at least one is synchronised