From a84368953f7d9f24d7b8e75279adc3602a540959 Mon Sep 17 00:00:00 2001
From: Michael Walker <mike@barrucadu.co.uk>
Date: Wed, 6 Sep 2017 16:03:28 +0100
Subject: [PATCH] Add tests for the ticket casCRef returns

---
 dejafu-tests/Cases/MultiThreaded.hs  | 27 ++++++++++++++++++++++-----
 dejafu-tests/Cases/SingleThreaded.hs | 11 +++++++++++
 2 files changed, 33 insertions(+), 5 deletions(-)

diff --git a/dejafu-tests/Cases/MultiThreaded.hs b/dejafu-tests/Cases/MultiThreaded.hs
index 430e242..e8ea6f8 100644
--- a/dejafu-tests/Cases/MultiThreaded.hs
+++ b/dejafu-tests/Cases/MultiThreaded.hs
@@ -1,7 +1,7 @@
 module Cases.MultiThreaded where
 
 import Control.Exception (ArithException(..))
-import Control.Monad (void)
+import Control.Monad (void, unless)
 import Test.DejaFu (Failure(..), gives, gives')
 import Test.Framework (Test)
 
@@ -23,10 +23,11 @@ tests =
       , T "race"     cvarRace $ gives' [0,1]
       ]
     , tg "CRef"
-      [ T "race"        crefRace       $ gives' [0,1]
-      , T "cas modify"  crefCASModify  $ gives' [0,1]
-      , T "cas race"    crefCASRace    $ gives' [(True, 2), (False, 2)]
-      , T "cas tickets" crefCASTickets $ gives' [(True, False, 1), (False, True, 2)]
+      [ T "race"            crefRace        $ gives' [0,1]
+      , T "cas modify"      crefCASModify   $ gives' [0,1]
+      , T "cas race"        crefCASRace     $ gives' [(True, 2), (False, 2)]
+      , T "cas race (redo)" crefCASRaceRedo $ gives' [(True, 1), (True, 2)]
+      , T "cas tickets"     crefCASTickets  $ gives' [(True, False, 1), (False, True, 2)]
       ]
     , tg "STM"
       [ T "atomicity"   stmAtomic     $ gives' [0,2]
@@ -151,6 +152,22 @@ crefCASRace = do
   v <- readCRef x
   pure (b, v)
 
+-- | Failed CAS can use the new ticket to succeed.
+crefCASRaceRedo :: MonadConc m => m (Bool, Int)
+crefCASRaceRedo = do
+  x <- newCRef (0::Int)
+  t <- readForCAS x
+  v <- newEmptyMVar
+  j <- spawn $ do
+    o@(f, t') <- casCRef x t 1
+    takeMVar v
+    if f then pure o else casCRef x t' 1
+  writeCRef x 2
+  putMVar v ()
+  b <- fst <$> readMVar j
+  v <- readCRef x
+  pure (b, v)
+
 -- | A ticket is only good for one CAS.
 crefCASTickets :: MonadConc m => m (Bool, Bool, Int)
 crefCASTickets = do
diff --git a/dejafu-tests/Cases/SingleThreaded.hs b/dejafu-tests/Cases/SingleThreaded.hs
index ca28515..702001c 100644
--- a/dejafu-tests/Cases/SingleThreaded.hs
+++ b/dejafu-tests/Cases/SingleThreaded.hs
@@ -41,6 +41,7 @@ tests =
     , testDejafu crefWrite      "write"       $ gives' [True]
     , testDejafu crefModify     "modify"      $ gives' [True]
     , testDejafu crefTicketPeek "ticket peek" $ gives' [True]
+    , testDejafu crefTicketPeek "ticket peek (2)" $ gives' [True]
     , testDejafu crefCas1       "cas"         $ gives' [(True, True)]
     , testDejafu crefCas2       "cas (modified)" $ gives' [(False, False)]
     ]
@@ -189,6 +190,16 @@ crefTicketPeek = do
 
   (5==) <$> peekTicket tick
 
+-- | A @Ticket@ contains the value as of when it was created (and
+-- casCRef returns a correct new ticket).
+crefTicketPeek2 :: MonadConc m => m Bool
+crefTicketPeek2 = do
+  ref  <- newCRef (5::Int)
+  tick <- readForCAS ref
+  (_, tick') <- casCRef ref tick 6
+
+  (6==) <$> peekTicket tick'
+
 -- | A compare-and-swap can be done on a @CRef@ which hasn't been
 -- modified.
 crefCas1 :: MonadConc m => m (Bool, Bool)