Skip to content

Commit 5ef39f0

Browse files
jorisdraljorisdral
committed
Strict MVars with invariant checking
1 parent df0ddc9 commit 5ef39f0

File tree

6 files changed

+277
-1
lines changed

6 files changed

+277
-1
lines changed

‎.github/workflows/cabal.project.local

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ package io-classes
88

99
package strict-mvar
1010
ghc-options: -Werror
11-
flags: +asserts
11+
flags: +asserts +checkmvarinvariant
1212

1313
package strict-stm
1414
ghc-options: -Werror

‎.github/workflows/haskell.yml

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -127,6 +127,9 @@ jobs:
127127
- name: si-timers [test]
128128
run: cabal run si-timers:test
129129

130+
- name: strict-mvar [test]
131+
run: cabal run strict-mvar:test
132+
130133
stylish-haskell:
131134
runs-on: ubuntu-22.04
132135

‎strict-mvar/src/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs

Lines changed: 188 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,188 @@
1+
{-# LANGUAGE BangPatterns #-}
2+
{-# LANGUAGE CPP #-}
3+
{-# LANGUAGE TupleSections #-}
4+
{-# LANGUAGE TypeFamilies #-}
5+
{-# LANGUAGE TypeOperators #-}
6+
7+
-- | This module corresponds to 'Control.Concurrent.MVar' in "base" package
8+
--
9+
module Control.Concurrent.Class.MonadMVar.Strict.Checked
10+
( -- * StrictMVar
11+
StrictMVar
12+
, castStrictMVar
13+
, toLazyMVar
14+
, fromLazyMVar
15+
, newEmptyMVar
16+
, newEmptyMVarWithInvariant
17+
, newMVar
18+
, newMVarWithInvariant
19+
, takeMVar
20+
, putMVar
21+
, readMVar
22+
, swapMVar
23+
, tryTakeMVar
24+
, tryPutMVar
25+
, isEmptyMVar
26+
, withMVar
27+
, withMVarMasked
28+
, modifyMVar_
29+
, modifyMVar
30+
, modifyMVarMasked_
31+
, modifyMVarMasked
32+
, tryReadMVar
33+
-- * Re-exports
34+
, MonadMVar
35+
) where
36+
37+
import Control.Concurrent.Class.MonadMVar (MonadMVar)
38+
import qualified Control.Concurrent.Class.MonadMVar as Lazy
39+
import GHC.Stack (HasCallStack)
40+
41+
--
42+
-- StrictMVar
43+
--
44+
45+
type LazyMVar m = Lazy.MVar m
46+
47+
-- | A strict MVar with invariant checking.
48+
--
49+
-- There is a weaker invariant for a 'StrictMVar' than for a 'StrictTVar' (see
50+
-- the @strict-stm@ package): although all functions that modify the
51+
-- 'StrictMVar' check the invariant, we do /not/ guarantee that the value inside
52+
-- the 'StrictMVar' always satisfies the invariant. Instead, we /do/ guarantee
53+
-- that if the 'StrictMVar' is updated with a value that does not satisfy the
54+
-- invariant, an exception is thrown. The reason for this weaker guarantee is
55+
-- that leaving an 'MVar' empty can lead to very hard to debug "blocked
56+
-- indefinitely" problems.
57+
data StrictMVar m a = StrictMVar {
58+
-- | The invariant that is checked whenever the 'StrictMVar' is updated.
59+
invariant :: !(a -> Maybe String)
60+
, mvar :: !(LazyMVar m a)
61+
}
62+
63+
castStrictMVar :: LazyMVar m ~ LazyMVar n
64+
=> StrictMVar m a -> StrictMVar n a
65+
castStrictMVar v = StrictMVar (invariant v) (mvar v)
66+
67+
-- | Get the underlying @MVar@
68+
--
69+
-- Since we obviously can not guarantee that updates to this 'LazyMVar' will be
70+
-- strict, this should be used with caution.
71+
--
72+
-- Similarly, we can not guarantee that updates to this 'LazyMVar' do not break
73+
-- the original invariant that the 'StrictMVar' held.
74+
toLazyMVar :: StrictMVar m a -> LazyMVar m a
75+
toLazyMVar = mvar
76+
77+
-- | Create a 'StrictMVar' from a 'LazyMVar'
78+
--
79+
-- It is not guaranteed that the 'LazyMVar' contains a value that is in WHNF, so
80+
-- there is no guarantee that the resulting 'StrictMVar' contains a value that
81+
-- is in WHNF. This should be used with caution.
82+
--
83+
-- The resulting 'StrictMVar' has a trivial invariant.
84+
fromLazyMVar :: Lazy.MVar m a -> StrictMVar m a
85+
fromLazyMVar = StrictMVar (const Nothing)
86+
87+
newEmptyMVar :: MonadMVar m => m (StrictMVar m a)
88+
newEmptyMVar = fromLazyMVar <$> Lazy.newEmptyMVar
89+
90+
newEmptyMVarWithInvariant ::
91+
MonadMVar m
92+
=> (a -> Maybe String) -> m (StrictMVar m a)
93+
newEmptyMVarWithInvariant inv = StrictMVar inv <$> Lazy.newEmptyMVar
94+
95+
newMVar :: MonadMVar m => a -> m (StrictMVar m a)
96+
newMVar !a = fromLazyMVar <$> Lazy.newMVar a
97+
98+
newMVarWithInvariant ::
99+
MonadMVar m
100+
=> (a -> Maybe String) -> a -> m (StrictMVar m a)
101+
newMVarWithInvariant inv !a =
102+
checkInvariant (inv a) $
103+
StrictMVar inv <$> Lazy.newMVar a
104+
105+
takeMVar :: MonadMVar m => StrictMVar m a -> m a
106+
takeMVar = Lazy.takeMVar . mvar
107+
108+
putMVar :: MonadMVar m => StrictMVar m a -> a -> m ()
109+
putMVar v !a = do
110+
Lazy.putMVar (mvar v) a
111+
checkInvariant (invariant v a) $ pure ()
112+
113+
readMVar :: MonadMVar m => StrictMVar m a -> m a
114+
readMVar v = Lazy.readMVar (mvar v)
115+
116+
swapMVar :: MonadMVar m => StrictMVar m a -> a -> m a
117+
swapMVar v !a = do
118+
oldValue <- Lazy.swapMVar (mvar v) a
119+
checkInvariant (invariant v a) $ pure oldValue
120+
121+
tryTakeMVar :: MonadMVar m => StrictMVar m a -> m (Maybe a)
122+
tryTakeMVar v = Lazy.tryTakeMVar (mvar v)
123+
124+
tryPutMVar :: MonadMVar m => StrictMVar m a -> a -> m Bool
125+
tryPutMVar v !a = do
126+
didPut <- Lazy.tryPutMVar (mvar v) a
127+
checkInvariant (invariant v a) $ pure didPut
128+
129+
isEmptyMVar :: MonadMVar m => StrictMVar m a -> m Bool
130+
isEmptyMVar v = Lazy.isEmptyMVar (mvar v)
131+
132+
withMVar :: MonadMVar m => StrictMVar m a -> (a -> m b) -> m b
133+
withMVar v = Lazy.withMVar (mvar v)
134+
135+
withMVarMasked :: MonadMVar m => StrictMVar m a -> (a -> m b) -> m b
136+
withMVarMasked v = Lazy.withMVarMasked (mvar v)
137+
138+
-- | 'modifyMVar_' is defined in terms of 'modifyMVar'.
139+
modifyMVar_ :: MonadMVar m => StrictMVar m a -> (a -> m a) -> m ()
140+
modifyMVar_ v io = modifyMVar v io'
141+
where io' a = (,()) <$> io a
142+
143+
modifyMVar :: MonadMVar m => StrictMVar m a -> (a -> m (a,b)) -> m b
144+
modifyMVar v io = do
145+
(a', b) <- Lazy.modifyMVar (mvar v) io'
146+
checkInvariant (invariant v a') $ pure b
147+
where
148+
io' a = do
149+
(!a', b) <- io a
150+
-- Returning @a'@ along with @b@ allows us to check the invariant /after/
151+
-- filling in the MVar.
152+
pure (a' , (a', b))
153+
154+
-- | 'modifyMVarMasked_' is defined in terms of 'modifyMVarMasked'.
155+
modifyMVarMasked_ :: MonadMVar m => StrictMVar m a -> (a -> m a) -> m ()
156+
modifyMVarMasked_ v io = modifyMVar v io'
157+
where io' a = (,()) <$> io a
158+
159+
modifyMVarMasked :: MonadMVar m => StrictMVar m a -> (a -> m (a,b)) -> m b
160+
modifyMVarMasked v io = do
161+
(a', b) <- Lazy.modifyMVar (mvar v) io'
162+
checkInvariant (invariant v a') $ pure b
163+
where
164+
io' a = do
165+
(!a', b) <- io a
166+
-- Returning @a'@ along with @b@ allows us to check the invariant /after/
167+
-- filling in the MVar.
168+
pure (a', (a', b))
169+
170+
tryReadMVar :: MonadMVar m => StrictMVar m a -> m (Maybe a)
171+
tryReadMVar v = Lazy.tryReadMVar (mvar v)
172+
173+
--
174+
-- Dealing with invariants
175+
--
176+
177+
-- | Check invariant (if enabled)
178+
--
179+
-- @checkInvariant mErr x@ is equal to @x@ if @mErr == Nothing@, and throws an
180+
-- error @err@ if @mErr == Just err@.
181+
checkInvariant :: HasCallStack => Maybe String -> a -> a
182+
183+
#if CHECK_MVAR_INVARIANT
184+
checkInvariant Nothing k = k
185+
checkInvariant (Just err) _ = error $ "Invariant violation: " ++ err
186+
#else
187+
checkInvariant _err k = k
188+
#endif

‎strict-mvar/strict-mvar.cabal

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,11 @@ source-repository head
2424
location: https://github.com/input-output-hk/io-sim
2525
subdir: strict-mvar
2626

27+
flag checkmvarinvariant
28+
Description: Enable runtime invariant checks on StrictMVar
29+
Manual: True
30+
Default: False
31+
2732
flag asserts
2833
description: Enable assertions
2934
manual: False
@@ -33,6 +38,7 @@ library
3338
hs-source-dirs: src
3439

3540
exposed-modules: Control.Concurrent.Class.MonadMVar.Strict
41+
, Control.Concurrent.Class.MonadMVar.Strict.Checked
3642
default-language: Haskell2010
3743
build-depends: base >= 4.9 && <4.19,
3844
io-classes >= 1.0 && <1.2
@@ -46,3 +52,28 @@ library
4652

4753
if flag(asserts)
4854
ghc-options: -fno-ignore-asserts
55+
56+
if flag(checkmvarinvariant)
57+
cpp-options: -DCHECK_MVAR_INVARIANT
58+
59+
test-suite test
60+
type: exitcode-stdio-1.0
61+
hs-source-dirs: test
62+
main-is: Main.hs
63+
64+
other-modules: Test.Control.Concurrent.Class.MonadMVar.Strict.Checked
65+
default-language: Haskell2010
66+
build-depends: base >=4.9 && <4.18,
67+
QuickCheck,
68+
tasty,
69+
tasty-quickcheck,
70+
strict-mvar,
71+
72+
ghc-options: -Wall
73+
-Wno-unticked-promoted-constructors
74+
-Wcompat
75+
-Wincomplete-uni-patterns
76+
-Wincomplete-record-updates
77+
-Wpartial-fields
78+
-Widentities
79+
-fno-ignore-asserts

‎strict-mvar/test/Main.hs

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
module Main where
2+
3+
import qualified Test.Control.Concurrent.Class.MonadMVar.Strict.Checked as Checked
4+
import Test.Tasty
5+
6+
main :: IO ()
7+
main = defaultMain $
8+
testGroup "Test" [
9+
testGroup "Control" [
10+
testGroup "Concurrent" [
11+
testGroup "Class" [
12+
testGroup "MonadMVar" [
13+
testGroup "Strict" [
14+
testGroup "Checked" [
15+
Checked.tests
16+
]
17+
]
18+
]
19+
]
20+
]
21+
]
22+
]

‎strict-mvar/test/Test/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
-- | Tests in this module depend on the @+checkmvarinvariant@ flag being
2+
-- enabled.
3+
module Test.Control.Concurrent.Class.MonadMVar.Strict.Checked where
4+
5+
import Control.Concurrent.Class.MonadMVar.Strict.Checked
6+
import Test.QuickCheck.Monadic
7+
import Test.Tasty
8+
import Test.Tasty.QuickCheck
9+
10+
tests :: TestTree
11+
tests = testGroup "Checked" [
12+
testProperty "prop_invariantShouldFail" prop_invariantShouldFail
13+
, testProperty "prop_invariantShouldNotFail" prop_invariantShouldNotFail
14+
]
15+
16+
-- | Invariant that checks whether an @Int@ is positive.
17+
invPositiveInt :: Int -> Maybe String
18+
invPositiveInt x
19+
| x >= 0 = Nothing
20+
| otherwise = Just $ "x<0 for x=" <> show x
21+
22+
prop_invariantShouldFail :: Property
23+
prop_invariantShouldFail = once $ expectFailure $ monadicIO $ run $ do
24+
v <- newMVarWithInvariant invPositiveInt 0
25+
modifyMVar_ v (\x -> pure $ x - 1)
26+
pure ()
27+
28+
prop_invariantShouldNotFail :: Property
29+
prop_invariantShouldNotFail = monadicIO $ run $ do
30+
v <- newMVarWithInvariant invPositiveInt 0
31+
modifyMVar_ v (\x -> pure $ x + 1)
32+
pure ()

0 commit comments

Comments
 (0)