Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Inspecting TMVar and friends in Invariant #386

Open
NicolasT opened this issue Apr 7, 2023 · 0 comments
Open

Inspecting TMVar and friends in Invariant #386

NicolasT opened this issue Apr 7, 2023 · 0 comments

Comments

@NicolasT
Copy link

NicolasT commented Apr 7, 2023

With inspectTVar it's possible to inspect a ModelTVar n in an Invariant n context. This is very useful, however, it's unclear to me how the types provided by concurrency built on top of TVars can be inspected in Invariant.

As an example, a TMVar stm a is, basically, a newtype around TVar stm (Maybe a). If the TMVar constructor were exported, it'd be possible to implement inspectTMVar (= \(TMVar ctvar) -> inspectTVar ctvar or something like that), but since it isn't, we're kinda stuck.

Other STM types like TChan, TSem,... also wrap something in a TVar, but can't be inspected.

Adding inspectTMVar etc. to concurrency would add a dependency on dejafu to concurrency which is likely undesired. At the same time, exposing the various constructors could be undesired as well, since giving direct access to the inner TVar could easily break invariants.

I couldn't think of a good way to tackle this yet, but it seems quite useful/important not to be restricted to only TVars when defining invariant checks.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant