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

Provide "context isolation" primitives #175

Closed
robdockins opened this issue Jan 5, 2022 · 1 comment
Closed

Provide "context isolation" primitives #175

robdockins opened this issue Jan 5, 2022 · 1 comment

Comments

@robdockins
Copy link
Contributor

The What4 expression builder datastructure was originally designed to be single threaded and have essentially whole-program lifetime. As such, not much care was given to making it possible to isolate separate concurrent or sequential uses from each other. As time has gone on, however, reuse of the expression builder (both across threads and across time) has become more common.

There are a few places where different users of the expression builder can get into trouble sharing the data structure: these mostly have to do with various kinds of configuration options, and also the troublesome get/set current program location operations.
The Config datastructure, in particular, is basically a big mutable map filled with mutable values that can have nontrivial effects when written to (including things like changing the hash-consing setting).

We should design and provide APIs for allowing users of expression builders to isolate themselves from other concurrent and/or subsequent users. This will likely involve being able to do things like "clone" the current configuration state, set up local hash-consing contexts, and provide a different way for terms to be annotated with some notion of the current program location.

@robdockins
Copy link
Contributor Author

Fixed via #176

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

No branches or pull requests

1 participant