Add an independency between writes and commits.

An unsynchronised write and a commit to the same CRef are independent if
the buffer is nonempty, because the commit will take from the front of
the buffer and the write will append to the end.

See [RMMVerification], lemma 5.25. It doesn't translate directly because
of the different models, but it's the same optimisation in spirit.

README.markdown

@@ -35,3 +35,7 @@ provided where non-paywalled ones are available.
 - [Empirical] *Concurrency Testing Using Schedule Bounding: an
   Empirical Study*, P. Thompson, A. Donaldson, and A. Betts (2014)
   http://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2014/PPoPP.pdf
+
+- [RMMVerification] *On the Verification of Programs on Relaxed Memory
+  Models*, A. Linden (2014)
+  https://orbi.ulg.ac.be/bitstream/2268/158670/1/thesis.pdf

dejafu/Test/DejaFu/SCT/Internal.hs

@@ -333,6 +333,13 @@ dependentActions memtype buf a1 a2 = case (a1, a2) of
   (UnsynchronisedWrite r1, UnsynchronisedRead  r2) -> r1 == r2
   (UnsynchronisedWrite r1, UnsynchronisedWrite r2) -> r1 == r2
 
+  -- Unsynchronised writes and synchronisation where the buffer is not
+  -- empty.
+  --
+  -- See [RMMVerification], lemma 5.25.
+  (UnsynchronisedWrite r1, _) | same crefOf && isCommit a2 r1 && isBuffered buf r1 -> False
+  (_, UnsynchronisedWrite r2) | same crefOf && isCommit a1 r2 && isBuffered buf r2 -> False
+
   -- Unsynchronised reads where a memory barrier would flush a
   -- buffered write
   (UnsynchronisedRead r1, _) | isBarrier a2 -> isBuffered buf r1 && memtype /= SequentialConsistency