Race-condition when using Metatheory from multiple threads

[gkronber]

I'm getting errors when calling saturate for an egraph from multiple threads. I'm careful not to use any shared variables. The race condition seems to occur inside Metatheory (ale/3.0 branch).

Here is the test script

using Metatheory

function test_threads()
    println("thread pool size: $(Threads.threadpoolsize())")
    Threads.@threads for i in 1:1000
        theory = @theory a b c begin
            a + b == b + a
            a * b == b * a
            a + (b + c) == (a + b) + c
            a * (b * c) == (a * b) * c
        end

        g = EGraph{Expr}(:(1 + (2 + (3 + (4 + (5 + 6))))));
        params = SaturationParams(timeout=100)
        report = saturate!(g, theory, params)
        # println(g)
        # println(report)
    end
end

Calling this from a julia instance with 12 threads julia -t 12: leads to the following output (example)

julia> test_threads()
thread pool size: 12
ERROR: TaskFailedException

    nested task error: WARNING: both TermInterface and Meta export "isexpr"; uses of it in module Metatheory must be qualified
BoundsError: attempt to access 81-element Vector{UInt64} at index [247]
    Stacktrace:
      [1] getindex
        @ ./essentials.jl:13 [inlined]
      [2] getindex
        @ ./abstractarray.jl:1291 [inlined]
      [3] find
        @ ~/.julia/dev/Metatheory/src/EGraphs/unionfind.jl:21 [inlined]
      [4] find
        @ ~/.julia/dev/Metatheory/src/EGraphs/egraph.jl:226 [inlined]
      [5] canonicalize!(g::EGraph{Expr, Nothing}, n::Vector{UInt64})
        @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/egraph.jl:250
      [6] add!(g::EGraph{Expr, Nothing}, n::Vector{UInt64}, should_copy::Bool)
        @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/egraph.jl:279
      [7] instantiate_enode!(bindings::SubArray{UInt128, 1, Vector{…}, Tuple{…}, true}, g::EGraph{Expr, Nothing}, p::PatExpr)
        @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:133
      [8] apply_rule!(bindings::SubArray{…}, g::EGraph{…}, rule::EqualityRule, id::UInt64, direction::Int64, merges_buffer::OptBuffer{…})
        @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:145
      [9] eqsat_apply!(g::EGraph{…}, theory::Vector{…}, rep::Metatheory.EGraphs.SaturationReport, params::SaturationParams, ematch_buffer::OptBuffer{…}, merges_buffer::OptBuffer{…})
        @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:241
     [10] macro expansion
        @ ~/.julia/packages/TimerOutputs/Lw5SP/src/TimerOutput.jl:237 [inlined]
     [11] eqsat_step!(g::EGraph{…}, theory::Vector{…}, curr_iter::Int64, scheduler::Metatheory.EGraphs.Schedulers.BackoffScheduler, params::SaturationParams, report::Metatheory.EGraphs.SaturationReport, ematch_buffer::OptBuffer{…}, merges_buffer::OptBuffer{…})
        @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:299
     [12] saturate!(g::EGraph{Expr, Nothing}, theory::Vector{RewriteRule}, params::SaturationParams)
        @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:336
     [13] macro expansion
        @ ~/cuda/test_parallel_eqsat.jl:17 [inlined]
     [14] (::var"#10#threadsfor_fun#2"{var"#10#threadsfor_fun#1#3"{UnitRange{Int64}}})(tid::Int64; onethread::Bool)
        @ Main ./threadingconstructs.jl:214
     [15] #10#threadsfor_fun
        @ Main ./threadingconstructs.jl:181 [inlined]
     [16] (::Base.Threads.var"#1#2"{var"#10#threadsfor_fun#2"{var"#10#threadsfor_fun#1#3"{UnitRange{Int64}}}, Int64})()
        @ Base.Threads ./threadingconstructs.jl:153

...and 10 more exceptions.

Stacktrace:
 [1] threading_run(fun::var"#10#threadsfor_fun#2"{var"#10#threadsfor_fun#1#3"{UnitRange{Int64}}}, static::Bool)
   @ Base.Threads ./threadingconstructs.jl:171
 [2] macro expansion
   @ Main ./threadingconstructs.jl:219 [inlined]
 [3] test_threads()
   @ Main ~/cuda/test_parallel_eqsat.jl:7
 [4] top-level scope
   @ REPL[2]:1
Some type information was truncated. Use `show(err)` to see complete types.

With a single thread there is no error.

[0x0f0f0f]

What branch are you on? Are you on latest MT ale/3.0? We stopped using global buffers. The thing is, if you saturate a different e-graph object per-thread, this shouldn't happen and it's indeed a bug.

If you instead are trying to call saturate! on the same e-graph but from different threads, there's no mechanism for parallel saturation, and it's a hard task. Searching is fine, but applying matches must happen sequentially and after you union e-classes, ids are going to change, so if you change the ordering you also change the behavior.

[gkronber]

I pulled the latest changes from ale/3.0 but the problem persists. Am I missing something?

(@v1.10) pkg> status Metatheory
Status `~/.julia/environments/v1.10/Project.toml`
  [e9d8d322] Metatheory v3.0.0 `~/.julia/dev/Metatheory`

shell> cd ~/.julia/dev/Metatheory/
/home/gkronber/.julia/dev/Metatheory

shell> git status
On branch ale/3.0
Your branch is up to date with 'origin/ale/3.0'.

nothing to commit, working tree clean

shell> git log
commit 7709c902afbfd880405ec0c0916eee95c2e6d662 (HEAD -> ale/3.0, origin/ale/3.0)
Author: Alessandro Cheli <a@a.a>
Date:   Fri Jun 28 12:14:14 2024 +0200

    remove merges buffer

Yes, I only need the first case: saturate independent egraph objects on parallel threads.

[0x0f0f0f]

I pulled the latest changes from ale/3.0 but the problem persists. Am I missing something?

(@v1.10) pkg> status Metatheory
Status `~/.julia/environments/v1.10/Project.toml`
  [e9d8d322] Metatheory v3.0.0 `~/.julia/dev/Metatheory`

shell> cd ~/.julia/dev/Metatheory/
/home/gkronber/.julia/dev/Metatheory

shell> git status
On branch ale/3.0
Your branch is up to date with 'origin/ale/3.0'.

nothing to commit, working tree clean

shell> git log
commit 7709c902afbfd880405ec0c0916eee95c2e6d662 (HEAD -> ale/3.0, origin/ale/3.0)
Author: Alessandro Cheli <a@a.a>
Date:   Fri Jun 28 12:14:14 2024 +0200

    remove merges buffer

Yes, I only need the first case: saturate independent egraph objects on parallel threads.

I will investigate further. I think it's because each rule has its own custom callstack