Race-condition when using Metatheory from multiple threads #224
Description
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
endCalling 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.