From 3121f0a9b9c1ed2c9ff65879e1990909f8b0aec3 Mon Sep 17 00:00:00 2001 From: Joris Dral Date: Mon, 10 Jul 2023 13:08:52 +0200 Subject: [PATCH] Strict checked MVars and TVars --- .github/workflows/haskell.yml | 2 +- cabal.project | 10 + strict-checked-vars/CHANGELOG.md | 5 + strict-checked-vars/LICENSE | 177 ++++++++++++++++ strict-checked-vars/NOTICE | 14 ++ strict-checked-vars/README.md | 63 ++++++ .../Class/MonadMVar/Strict/Checked.hs | 194 ++++++++++++++++++ .../Class/MonadSTM/Strict/TVar/Checked.hs | 161 +++++++++++++++ strict-checked-vars/strict-checked-vars.cabal | 75 +++++++ strict-checked-vars/test/Main.hs | 9 + .../Class/MonadMVar/Strict/Checked.hs | 43 ++++ strict-checked-vars/test/Test/Utils.hs | 23 +++ 12 files changed, 775 insertions(+), 1 deletion(-) create mode 100644 strict-checked-vars/CHANGELOG.md create mode 100644 strict-checked-vars/LICENSE create mode 100644 strict-checked-vars/NOTICE create mode 100644 strict-checked-vars/README.md create mode 100644 strict-checked-vars/src/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs create mode 100644 strict-checked-vars/src/Control/Concurrent/Class/MonadSTM/Strict/TVar/Checked.hs create mode 100644 strict-checked-vars/strict-checked-vars.cabal create mode 100644 strict-checked-vars/test/Main.hs create mode 100644 strict-checked-vars/test/Test/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs create mode 100644 strict-checked-vars/test/Test/Utils.hs diff --git a/.github/workflows/haskell.yml b/.github/workflows/haskell.yml index 91f658d43..2a1bb8750 100644 --- a/.github/workflows/haskell.yml +++ b/.github/workflows/haskell.yml @@ -34,7 +34,7 @@ jobs: strategy: fail-fast: false matrix: - ghc: ["8.10.7", "9.2.7", "9.6.1"] + ghc: ["8.10.7", "9.2.7", "9.6.2"] os: [ubuntu-latest, macos-latest, windows-latest] env: diff --git a/cabal.project b/cabal.project index b09cf8c4e..a6e80f253 100644 --- a/cabal.project +++ b/cabal.project @@ -27,6 +27,7 @@ packages: heapwords measures orphans-deriving-via + strict-checked-vars -- Ensures colourized output from test runners test-show-details: direct @@ -41,3 +42,12 @@ if impl(ghc >= 9.6) , protolude:binary , protolude:bytestring , protolude:text + +-- TODO: remove when a new version of strict-mvar (>1.1.0.0) is released +source-repository-package + type: git + location: https://github.com/input-output-hk/io-sim + tag: 1b2c22b376f5cda314b9ab444caaf77764961a18 + --sha256: 1qdxcqr4sl93n036p3pz1rvk6zf4qbsadzw4lgsp9agkh8pvs16y + subdir: + strict-mvar \ No newline at end of file diff --git a/strict-checked-vars/CHANGELOG.md b/strict-checked-vars/CHANGELOG.md new file mode 100644 index 000000000..f50aed29f --- /dev/null +++ b/strict-checked-vars/CHANGELOG.md @@ -0,0 +1,5 @@ +# Revision history of strict-checked-vars + +## 0.1.0.0 + +* Initial version, not released on Hackage. diff --git a/strict-checked-vars/LICENSE b/strict-checked-vars/LICENSE new file mode 100644 index 000000000..f433b1a53 --- /dev/null +++ b/strict-checked-vars/LICENSE @@ -0,0 +1,177 @@ + + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS diff --git a/strict-checked-vars/NOTICE b/strict-checked-vars/NOTICE new file mode 100644 index 000000000..15b771a00 --- /dev/null +++ b/strict-checked-vars/NOTICE @@ -0,0 +1,14 @@ +Copyright 2019-2023 Input Output Global Inc (IOG). + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. + diff --git a/strict-checked-vars/README.md b/strict-checked-vars/README.md new file mode 100644 index 000000000..aa5ef6f7c --- /dev/null +++ b/strict-checked-vars/README.md @@ -0,0 +1,63 @@ +# Strict `MVar`s and `TVar`s with invariant checking + +The `strict-checked-vars` package provides a strict interface to mutable +variables (`MVar`) and `TVar`s with invariant checking. It builds on top of +`strict-mvar`, `strict-stm` and `io-classes`, and thus it provides the interface +for `MVar`/`TVar` implementations for both +[IO](https://hackage.haskell.org/package/base-4.18.0.0/docs/Prelude.html#t:IO) +and [io-sim](https://hackage.haskell.org/package/io-sim). + +## Checked and unchecked variants + +There are currently two variant implementations of `StrictTVar`s. +* From `strict-stm`: `Control.Concurrent.Class.MonadSTM.Strict.TVar` +* From `strict-checked-vars`: `Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked` + +Similarly, there are currently two variant implementations of `StrictMVar`s. +* From `strict-mvar`: `Control.Concurrent.Class.MonadMVar.Strict` +* From `strict-checked-vars`: `Control.Concurrent.Class.MonadMVar.Strict.Checked` + + +The _unchecked_ modules provide the simplest implementation of strict variables: +a light wrapper around lazy variables that forces values to WHNF before they are +put inside the variable. The _checked_ module does the exact same thing, but it +has the additional feature that the user can provide an invariant that is +checked each time a new value is placed inside the variable. The checked modules +are drop-in replacements for the unchecked modules, though invariants will be +trivially true in that case. Non-trivial invariants can be set when creating a +new variable. + +```haskell +newMVarWithInvariant :: MonadMVar m + => (a -> Maybe String) + -> a + -> m (StrictMVar m a) + +newEmptyMVarWithInvariant :: MonadMVar m + => (a -> Maybe String) + -> m (StrictMVar m a) + +newTVarWithInvariant :: (MonadSTM m, HasCallStack) + => (a -> Maybe String) + -> a + -> STM m (StrictTVar m a) + +newTVarWithInvariantIO :: (MonadSTM m, HasCallStack) + => (a -> Maybe String) + -> a + -> m (StrictTVar m a) +``` + +**Note:** though the checked modules are drop-in replacements for the unchecked +modules, the `StrictMVar`/`StrictTVar` types are distinct. This means we can't +make mixed use of the checked and unchecked modules. + +## Guarantees for invariant checking on `StrictMVar`s + +Although all functions that modify a checked `StrictMVar` will check the +invariant, we do *not* guarantee that the value inside the `StrictMVar` always +satisfies the invariant. Instead, we *do* guarantee that if the `StrictMVar` is +updated with a value that does not satisfy the invariant, an exception is thrown +*after* the new value is written to the `StrictMVar`. The reason for this weaker +guarantee is that leaving an `MVar` empty can lead to very hard to debug +"blocked indefinitely" problems. \ No newline at end of file diff --git a/strict-checked-vars/src/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs b/strict-checked-vars/src/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs new file mode 100644 index 000000000..07b26e383 --- /dev/null +++ b/strict-checked-vars/src/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs @@ -0,0 +1,194 @@ +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +-- | This module corresponds to "Control.Concurrent.MVar" in the @base@ package. +-- +-- This module can be used as a drop-in replacement for +-- "Control.Concurrent.Class.MonadMVar.Strict", but not the other way around. +module Control.Concurrent.Class.MonadMVar.Strict.Checked ( + -- * StrictMVar + LazyMVar + , StrictMVar + , castStrictMVar + , fromLazyMVar + , isEmptyMVar + , modifyMVar + , modifyMVarMasked + , modifyMVarMasked_ + , modifyMVar_ + , newEmptyMVar + , newEmptyMVarWithInvariant + , newMVar + , newMVarWithInvariant + , putMVar + , readMVar + , swapMVar + , takeMVar + , toLazyMVar + , tryPutMVar + , tryReadMVar + , tryTakeMVar + , withMVar + , withMVarMasked + -- * Re-exports + , MonadMVar + ) where + +import Control.Concurrent.Class.MonadMVar.Strict (LazyMVar, MonadMVar) +import qualified Control.Concurrent.Class.MonadMVar.Strict as Strict +import GHC.Stack (HasCallStack) + +{------------------------------------------------------------------------------- + StrictMVar +-------------------------------------------------------------------------------} + +-- | A strict MVar with invariant checking. +-- +-- There is a weaker invariant for a 'StrictMVar' than for a 'StrictTVar': +-- although all functions that modify the 'StrictMVar' check the invariant, we +-- do /not/ guarantee that the value inside the 'StrictMVar' always satisfies +-- the invariant. Instead, we /do/ guarantee that if the 'StrictMVar' is updated +-- with a value that does not satisfy the invariant, an exception is thrown. The +-- reason for this weaker guarantee is that leaving an 'MVar' empty can lead to +-- very hard to debug "blocked indefinitely" problems. +data StrictMVar m a = StrictMVar { + -- | The invariant that is checked whenever the 'StrictMVar' is updated. + invariant :: !(a -> Maybe String) + , mvar :: !(Strict.StrictMVar m a) + } + +castStrictMVar :: LazyMVar m ~ LazyMVar n + => StrictMVar m a -> StrictMVar n a +castStrictMVar v = StrictMVar (invariant v) (Strict.castStrictMVar $ mvar v) + +-- | Get the underlying @MVar@ +-- +-- Since we obviously can not guarantee that updates to this 'LazyMVar' will be +-- strict, this should be used with caution. +-- +-- Similarly, we can not guarantee that updates to this 'LazyMVar' do not break +-- the original invariant that the 'StrictMVar' held. +toLazyMVar :: StrictMVar m a -> LazyMVar m a +toLazyMVar = Strict.toLazyMVar . mvar + +-- | Create a 'StrictMVar' from a 'LazyMVar' +-- +-- It is not guaranteed that the 'LazyMVar' contains a value that is in WHNF, so +-- there is no guarantee that the resulting 'StrictMVar' contains a value that +-- is in WHNF. This should be used with caution. +-- +-- The resulting 'StrictMVar' has a trivial invariant. +fromLazyMVar :: LazyMVar m a -> StrictMVar m a +fromLazyMVar = StrictMVar (const Nothing) . Strict.fromLazyMVar + +newEmptyMVar :: MonadMVar m => m (StrictMVar m a) +newEmptyMVar = StrictMVar (const Nothing) <$> Strict.newEmptyMVar + +newEmptyMVarWithInvariant :: MonadMVar m + => (a -> Maybe String) + -> m (StrictMVar m a) +newEmptyMVarWithInvariant inv = StrictMVar inv <$> Strict.newEmptyMVar + +newMVar :: MonadMVar m => a -> m (StrictMVar m a) +newMVar a = StrictMVar (const Nothing) <$> Strict.newMVar a + +newMVarWithInvariant :: (HasCallStack, MonadMVar m) + => (a -> Maybe String) + -> a + -> m (StrictMVar m a) +newMVarWithInvariant inv a = + checkInvariant (inv a) $ + StrictMVar inv <$> Strict.newMVar a + +takeMVar :: MonadMVar m => StrictMVar m a -> m a +takeMVar = Strict.takeMVar . mvar + +putMVar :: (HasCallStack, MonadMVar m) => StrictMVar m a -> a -> m () +putMVar v a = do + Strict.putMVar (mvar v) a + checkInvariant (invariant v a) $ pure () + +readMVar :: MonadMVar m => StrictMVar m a -> m a +readMVar v = Strict.readMVar (mvar v) + +swapMVar :: (HasCallStack, MonadMVar m) => StrictMVar m a -> a -> m a +swapMVar v a = do + oldValue <- Strict.swapMVar (mvar v) a + checkInvariant (invariant v a) $ pure oldValue + +tryTakeMVar :: MonadMVar m => StrictMVar m a -> m (Maybe a) +tryTakeMVar v = Strict.tryTakeMVar (mvar v) + +tryPutMVar :: (HasCallStack, MonadMVar m) => StrictMVar m a -> a -> m Bool +tryPutMVar v a = do + didPut <- Strict.tryPutMVar (mvar v) a + checkInvariant (invariant v a) $ pure didPut + +isEmptyMVar :: MonadMVar m => StrictMVar m a -> m Bool +isEmptyMVar v = Strict.isEmptyMVar (mvar v) + +withMVar :: MonadMVar m => StrictMVar m a -> (a -> m b) -> m b +withMVar v = Strict.withMVar (mvar v) + +withMVarMasked :: MonadMVar m => StrictMVar m a -> (a -> m b) -> m b +withMVarMasked v = Strict.withMVarMasked (mvar v) + +-- | 'modifyMVar_' is defined in terms of 'modifyMVar'. +modifyMVar_ :: (HasCallStack, MonadMVar m) + => StrictMVar m a + -> (a -> m a) + -> m () +modifyMVar_ v io = modifyMVar v io' + where io' a = (,()) <$> io a + +modifyMVar :: (HasCallStack, MonadMVar m) + => StrictMVar m a + -> (a -> m (a,b)) + -> m b +modifyMVar v io = do + (a', b) <- Strict.modifyMVar (mvar v) io' + checkInvariant (invariant v a') $ pure b + where + io' a = do + (a', b) <- io a + -- Returning @a'@ along with @b@ allows us to check the invariant /after/ + -- filling in the MVar. + pure (a' , (a', b)) + +-- | 'modifyMVarMasked_' is defined in terms of 'modifyMVarMasked'. +modifyMVarMasked_ :: (HasCallStack, MonadMVar m) + => StrictMVar m a + -> (a -> m a) + -> m () +modifyMVarMasked_ v io = modifyMVar v io' + where io' a = (,()) <$> io a + +modifyMVarMasked :: (HasCallStack, MonadMVar m) + => StrictMVar m a + -> (a -> m (a,b)) + -> m b +modifyMVarMasked v io = do + (a', b) <- Strict.modifyMVarMasked (mvar v) io' + checkInvariant (invariant v a') $ pure b + where + io' a = do + (a', b) <- io a + -- Returning @a'@ along with @b@ allows us to check the invariant /after/ + -- filling in the MVar. + pure (a', (a', b)) + +tryReadMVar :: MonadMVar m => StrictMVar m a -> m (Maybe a) +tryReadMVar v = Strict.tryReadMVar (mvar v) + +-- +-- Dealing with invariants +-- + +-- | Check invariant +-- +-- @checkInvariant mErr x@ is equal to @x@ if @mErr == Nothing@, and throws an +-- error @err@ if @mErr == Just err@. +checkInvariant :: HasCallStack => Maybe String -> a -> a +checkInvariant Nothing k = k +checkInvariant (Just err) _ = error $ "StrictMVar invariant violation: " ++ err diff --git a/strict-checked-vars/src/Control/Concurrent/Class/MonadSTM/Strict/TVar/Checked.hs b/strict-checked-vars/src/Control/Concurrent/Class/MonadSTM/Strict/TVar/Checked.hs new file mode 100644 index 000000000..139cdc135 --- /dev/null +++ b/strict-checked-vars/src/Control/Concurrent/Class/MonadSTM/Strict/TVar/Checked.hs @@ -0,0 +1,161 @@ +{-# LANGUAGE TypeFamilies #-} + +-- | This module corresponds to "Control.Concurrent.STM.TVar" in the @stm@ package. +-- +-- This module can be used as a drop-in replacement for +-- "Control.Concurrent.Class.MonadSTM.Strict.TVar", but not the other way +-- around. +module Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked ( + -- * StrictTVar + LazyTVar + , StrictTVar + , castStrictTVar + , fromLazyTVar + , modifyTVar + , newTVar + , newTVarIO + , newTVarWithInvariant + , newTVarWithInvariantIO + , readTVar + , readTVarIO + , stateTVar + , swapTVar + , toLazyTVar + , writeTVar + -- * MonadLabelSTM + , labelTVar + , labelTVarIO + -- * MonadTraceSTM + , traceTVar + , traceTVarIO + ) where + +import Control.Concurrent.Class.MonadSTM (InspectMonad, + MonadLabelledSTM, MonadSTM, MonadTraceSTM, STM, TraceValue, + atomically) +import qualified Control.Concurrent.Class.MonadSTM.Strict.TVar as Strict +import GHC.Stack (HasCallStack) + +{------------------------------------------------------------------------------- + StrictTVar +-------------------------------------------------------------------------------} + +type LazyTVar m = Strict.LazyTVar m + +data StrictTVar m a = StrictTVar { + -- | Invariant checked whenever updating the 'StrictTVar'. + invariant :: !(a -> Maybe String) + , tvar :: !(Strict.StrictTVar m a) + } + +castStrictTVar :: LazyTVar m ~ LazyTVar n + => StrictTVar m a -> StrictTVar n a +castStrictTVar v = StrictTVar (invariant v) (Strict.castStrictTVar $ tvar v) + +-- | Get the underlying @TVar@ +-- +-- Since we obviously cannot guarantee that updates to this 'LazyTVar' will be +-- strict, this should be used with caution. +-- +-- Similarly, we can not guarantee that updates to this 'LazyTVar' do not break +-- the original invariant that the 'StrictTVar' held. +toLazyTVar :: StrictTVar m a -> LazyTVar m a +toLazyTVar = Strict.toLazyTVar . tvar + +-- | Create a 'StrictMVar' from a 'LazyMVar' +-- +-- It is not guaranteed that the 'LazyTVar' contains a value that is in WHNF, so +-- there is no guarantee that the resulting 'StrictTVar' contains a value that +-- is in WHNF. This should be used with caution. +-- +-- The resulting 'StrictTVar' has a trivial invariant. +fromLazyTVar :: LazyTVar m a -> StrictTVar m a +fromLazyTVar = StrictTVar (const Nothing) . Strict.fromLazyTVar + +newTVar :: MonadSTM m => a -> STM m (StrictTVar m a) +newTVar a = StrictTVar (const Nothing) <$> Strict.newTVar a + +newTVarIO :: MonadSTM m => a -> m (StrictTVar m a) +newTVarIO = newTVarWithInvariantIO (const Nothing) + +newTVarWithInvariant :: (MonadSTM m, HasCallStack) + => (a -> Maybe String) + -> a + -> STM m (StrictTVar m a) +newTVarWithInvariant inv a = + checkInvariant (inv a) $ + StrictTVar inv <$> Strict.newTVar a + +newTVarWithInvariantIO :: (MonadSTM m, HasCallStack) + => (a -> Maybe String) + -> a + -> m (StrictTVar m a) +newTVarWithInvariantIO inv a = + checkInvariant (inv a) $ + StrictTVar inv <$> Strict.newTVarIO a + +readTVar :: MonadSTM m => StrictTVar m a -> STM m a +readTVar = Strict.readTVar . tvar + +readTVarIO :: MonadSTM m => StrictTVar m a -> m a +readTVarIO = Strict.readTVarIO . tvar + +writeTVar :: (MonadSTM m, HasCallStack) => StrictTVar m a -> a -> STM m () +writeTVar v a = + checkInvariant (invariant v a) $ + Strict.writeTVar (tvar v) a + +modifyTVar :: MonadSTM m => StrictTVar m a -> (a -> a) -> STM m () +modifyTVar v f = readTVar v >>= writeTVar v . f + +stateTVar :: MonadSTM m => StrictTVar m s -> (s -> (a, s)) -> STM m a +stateTVar v f = do + a <- readTVar v + let (b, a') = f a + writeTVar v a' + return b + +swapTVar :: MonadSTM m => StrictTVar m a -> a -> STM m a +swapTVar v a' = do + a <- readTVar v + writeTVar v a' + return a + +-- +-- Dealing with invariants +-- + +-- | Check invariant +-- +-- @checkInvariant mErr x@ is equal to @x@ if @mErr == Nothing@, and throws an +-- error @err@ if @mErr == Just err@. +checkInvariant :: HasCallStack => Maybe String -> a -> a +checkInvariant Nothing k = k +checkInvariant (Just err) _ = error $ "StrictTVar invariant violation: " ++ err + +{------------------------------------------------------------------------------- + MonadLabelledSTM +-------------------------------------------------------------------------------} + +labelTVar :: MonadLabelledSTM m => StrictTVar m a -> String -> STM m () +labelTVar = Strict.labelTVar . tvar + +labelTVarIO :: MonadLabelledSTM m => StrictTVar m a -> String -> m () +labelTVarIO v = atomically . labelTVar v + +{------------------------------------------------------------------------------- + MonadTraceSTM +-------------------------------------------------------------------------------} + +traceTVar :: MonadTraceSTM m + => proxy m + -> StrictTVar m a + -> (Maybe a -> a -> InspectMonad m TraceValue) + -> STM m () +traceTVar p = Strict.traceTVar p . tvar + +traceTVarIO :: MonadTraceSTM m + => StrictTVar m a + -> (Maybe a -> a -> InspectMonad m TraceValue) + -> m () +traceTVarIO = Strict.traceTVarIO . tvar diff --git a/strict-checked-vars/strict-checked-vars.cabal b/strict-checked-vars/strict-checked-vars.cabal new file mode 100644 index 000000000..0640a1c8d --- /dev/null +++ b/strict-checked-vars/strict-checked-vars.cabal @@ -0,0 +1,75 @@ +cabal-version: 3.0 +name: strict-checked-vars +version: 0.1.0.0 +synopsis: + Strict MVars and TVars with invariant checking for IO and IOSim + +description: + Strict @MVar@ and @TVar@ interfaces with invariant checking compatible with + [IO](https://hackage.haskell.org/package/base-4.18.0.0/docs/Prelude.html#t:IO) + & [io-sim](https://hackage.haskell.org/package/io-sim). + +license: Apache-2.0 +license-files: + LICENSE + NOTICE + +copyright: 2019-2023 Input Output Global Inc (IOG). +author: IOG Engineering Team +maintainer: operations@iohk.io +category: Concurrency +build-type: Simple +extra-doc-files: + CHANGELOG.md + README.md + +bug-reports: https://github.com/input-output-hk/io-sim/issues +tested-with: GHC ==8.10 || ==9.2 || ==9.4 || ==9.6 + +source-repository head + type: git + location: https://github.com/input-output-hk/ouroboros-consensus + subdir: strict-checked-vars + +library + hs-source-dirs: src + exposed-modules: + Control.Concurrent.Class.MonadMVar.Strict.Checked + Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked + + default-language: Haskell2010 + build-depends: + , base >=4.9 && <4.19 + , io-classes ^>=1.1 + , strict-mvar ^>=1.1 + , strict-stm ^>=1.1 + + ghc-options: + -Wall -Wno-unticked-promoted-constructors -Wcompat + -Wincomplete-uni-patterns -Wincomplete-record-updates + -Wpartial-fields -Widentities + +test-suite test + type: exitcode-stdio-1.0 + hs-source-dirs: test + main-is: Main.hs + other-modules: + Test.Control.Concurrent.Class.MonadMVar.Strict.Checked + Test.Utils + + default-language: Haskell2010 + build-depends: + , base >=4.9 && <4.19 + , io-sim + , nothunks + , QuickCheck + , strict-checked-vars + , strict-mvar + , strict-stm + , tasty + , tasty-quickcheck + + ghc-options: + -Wall -Wno-unticked-promoted-constructors -Wcompat + -Wincomplete-uni-patterns -Wincomplete-record-updates + -Wpartial-fields -Widentities -fno-ignore-asserts diff --git a/strict-checked-vars/test/Main.hs b/strict-checked-vars/test/Main.hs new file mode 100644 index 000000000..4b7213dbc --- /dev/null +++ b/strict-checked-vars/test/Main.hs @@ -0,0 +1,9 @@ +module Main where + +import qualified Test.Control.Concurrent.Class.MonadMVar.Strict.Checked as Checked +import Test.Tasty + +main :: IO () +main = defaultMain $ testGroup "strict-checked-vars" [ + Checked.tests + ] diff --git a/strict-checked-vars/test/Test/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs b/strict-checked-vars/test/Test/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs new file mode 100644 index 000000000..bdedfa2d4 --- /dev/null +++ b/strict-checked-vars/test/Test/Control/Concurrent/Class/MonadMVar/Strict/Checked.hs @@ -0,0 +1,43 @@ +{-# LANGUAGE RankNTypes #-} + +module Test.Control.Concurrent.Class.MonadMVar.Strict.Checked where + +import Control.Concurrent.Class.MonadMVar.Strict.Checked +import Test.QuickCheck.Monadic +import Test.Tasty +import Test.Tasty.QuickCheck +import Test.Utils + +tests :: TestTree +tests = testGroup "Test.Control.Concurrent.Class.MonadMVar.Strict" [ + testGroup "Checked" [ + testGroup "IO" [ + testProperty "prop_invariantShouldFail" $ + once $ expectFailure $ monadicIO prop_invariantShouldFail + , testProperty "prop_invariantShouldNotFail" $ + once $ monadicIO prop_invariantShouldNotFail + ] + , testGroup "IOSim" [ + testProperty "prop_invariantShouldFail" $ + once $ expectFailure $ monadicSim prop_invariantShouldFail + , testProperty "prop_invariantShouldNotFail" $ + once $ monadicSim prop_invariantShouldNotFail + ] + ] + ] + +-- | Invariant that checks whether an @Int@ is positive. +invPositiveInt :: Int -> Maybe String +invPositiveInt x + | x >= 0 = Nothing + | otherwise = Just $ "x<0 for x=" <> show x + +prop_invariantShouldNotFail :: MonadMVar m => PropertyM m () +prop_invariantShouldNotFail = run $ do + v <- newMVarWithInvariant invPositiveInt 0 + modifyMVar_ v (\x -> pure $ x + 1) + +prop_invariantShouldFail :: MonadMVar m => PropertyM m () +prop_invariantShouldFail = run $ do + v <- newMVarWithInvariant invPositiveInt 0 + modifyMVar_ v (\x -> pure $ x - 1) diff --git a/strict-checked-vars/test/Test/Utils.hs b/strict-checked-vars/test/Test/Utils.hs new file mode 100644 index 000000000..8600a2c6d --- /dev/null +++ b/strict-checked-vars/test/Test/Utils.hs @@ -0,0 +1,23 @@ +{-# LANGUAGE RankNTypes #-} + +module Test.Utils ( + monadicSim + , runSimGen + ) where + +import Control.Monad.IOSim (IOSim, runSimOrThrow) +import Test.QuickCheck (Gen, Property, Testable (..)) +import Test.QuickCheck.Gen.Unsafe (Capture (..), capture) +import Test.QuickCheck.Monadic (PropertyM, monadic') + +{------------------------------------------------------------------------------- + Property runners (copied from "Ouroboros.Network.Testing.QuickCheck") +-------------------------------------------------------------------------------} + +runSimGen :: (forall s. Gen (IOSim s a)) -> Gen a +runSimGen f = do + Capture eval <- capture + return $ runSimOrThrow (eval f) + +monadicSim :: Testable a => (forall s. PropertyM (IOSim s) a) -> Property +monadicSim m = property (runSimGen (monadic' m))