Skip to content

Thread safety #574

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

Open
wants to merge 6 commits into
base: master
Choose a base branch
from
Open

Thread safety #574

wants to merge 6 commits into from

Conversation

vouillon
Copy link
Member

@vouillon vouillon commented May 13, 2025

This PR makes RE thread-safe with OCaml 5.

We want the overhead to be minimal while matching a string, and allow concurrent string matching. Basically, RE works by traversing an automaton which is built lazily. So, there is no locking while traversing the automaton, but only when it is updated.

For that, we take advantage of the fact that double-checked locking is sound under the OCaml memory-model. When we reach a part of the automaton that has not been initialized yet, we acquire a mutex to update it. All the datastructures used to build this automaton are protected by this mutex.

vouillon added 3 commits May 12, 2025 17:02
Since other thread can create automaton states with an index larger the
size of the position array, we compare at each step that the current
index fits when running the automaton.
This is slow, but we can check that TSan reports no data race.
vouillon added 3 commits May 17, 2025 01:00
Basically, we are building an automaton lazily. We use double-checked
locking to avoid acquiring a mutex when traversing a part of the
automaton which has already been computed. The memory model ensures that
we see either an uninitialized state or the initialized state. If we see
the initialized state, we can just proceed. Otherwise, we acquire a
mutex and update the state after checking this has not been done by
another thread.
Use a fake implementation of mutexes and domains in this case to avoid a
dependency on the threads library
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

Successfully merging this pull request may close these issues.

1 participant