Multithreading support

[olynch]

Continuation of #231.

[github-actions]

Benchmark Results

	egg-sym	egg-cust	MT@52b48461e73...	MT@0b2e6c9f11b...	egg-sym/MT@52b...	egg-cust/MT@52...	MT@0b2e6c9f11b...
egraph_addexpr	1.41 ms		4.96 ms	4.9 ms	0.284		0.989
basic_maths_simpl2	12.7 ms	5.12 ms	21.4 ms	20 ms	0.592	0.239	0.936
prop_logic_freges_theorem	2.55 ms	1.54 ms	1.04 ms	1.07 ms	2.45	1.48	1.03
calc_logic_demorgan	61 μs	35.4 μs	75.5 μs	78.6 μs	0.808	0.469	1.04
calc_logic_freges_theorem	22 ms	11.9 ms	44.1 ms	41.8 ms	0.5	0.27	0.949
basic_maths_simpl1	6.08 ms	2.8 ms	5.02 ms	4.72 ms	1.21	0.558	0.939
egraph_constructor	0.0862 μs		0.0915 μs	0.0901 μs	0.942		0.985
prop_logic_prove1	35.9 ms	13 ms	42.6 ms	41.2 ms	0.844	0.305	0.968
prop_logic_demorgan	79.8 μs	44.3 μs	94.7 μs	99.5 μs	0.843	0.467	1.05
while_superinterpreter_while_10			18.8 ms	18.4 ms			0.982
prop_logic_rewrite			121 μs	120 μs			0.994
time_to_load			506 ms	505 ms			0.997

Benchmark Plots

A plot of the benchmark results have been uploaded as an artifact to the workflow run for this PR.
Go to "Actions"->"Benchmark a pull request"->[the most recent run]->"Artifacts" (at the bottom).

[olynch]

@0x0f0f0f the benchmarks look good!

[gkronber]

I just tested this again with multiple threads (julia -t 12).

using Metatheory

function run_eq()
  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)
end

function test_threads()
    println("thread pool size: $(Threads.threadpoolsize())")
    Threads.@threads for i in 1:1000
        run_eq()
    end
end

The issue does not seem to be resolved. Usually the error when accessing one of the dictionaries in the EGraph.

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

    nested task error: KeyError: key VecExpr(UInt64[0xc7970979e9cc1f1a, 0x0000000000000011, 0x4079ccad1b3303eb, 0x6b268fa6aca9af40, 0x0000000000000006, 0x0000000000000005]) not found
    Stacktrace:
      [1] getindex(h::Dict{Metatheory.EGraphs.IdKey, EClass{Nothing}}, key::Metatheory.EGraphs.IdKey)
        @ Base ./dict.jl:498 [inlined]
      [2] add!(g::EGraph{Expr, Nothing}, n::VecExpr, should_copy::Bool)
        @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/egraph.jl:276
      [3] instantiate_enode!(bindings::SubArray{UInt128, 1, Vector{…}, Tuple{…}, true}, g::EGraph{Expr, Nothing}, p::PatExpr)
        @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:137
      [4] apply_rule!(bindings::SubArray{…}, g::EGraph{…}, rule::EqualityRule, id::UInt64, direction::Int64)
        @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:174
      [5] eqsat_apply!(g::EGraph{…}, theory::Vector{…}, rep::Metatheory.EGraphs.SaturationReport, params::SaturationParams, ematch_buffer::OptBuffer{…})
        @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:242
      [6] macro expansion
        @ ~/.julia/packages/TimerOutputs/Lw5SP/src/TimerOutput.jl:237 [inlined]
      [7] eqsat_step!(g::EGraph{…}, theory::Vector{…}, curr_iter::Int64, scheduler::Metatheory.EGraphs.Schedulers.BackoffScheduler, params::SaturationParams, report::Metatheory.EGraphs.SaturationReport, ematch_buffer::OptBuffer{…})
        @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:287
      [8] saturate!(g::EGraph{Expr, Nothing}, theory::Vector{RewriteRule}, params::SaturationParams)
        @ Metatheory.EGraphs ~/.julia/dev/Metatheory/src/EGraphs/saturation.jl:324
      [9] run_eq()
        @ Main ./REPL[17]:11
     [10] macro expansion
        @ ./REPL[16]:4 [inlined]
     [11] (::var"#1525#threadsfor_fun#154"{var"#1525#threadsfor_fun#153#155"{UnitRange{Int64}}})(tid::Int64; onethread::Bool)
        @ Main ./threadingconstructs.jl:214
     [12] #1525#threadsfor_fun
        @ Main ./threadingconstructs.jl:181 [inlined]
     [13] (::Base.Threads.var"#1#2"{var"#1525#threadsfor_fun#154"{var"#1525#threadsfor_fun#153#155"{UnitRange{Int64}}}, Int64})()
        @ Base.Threads ./threadingconstructs.jl:153

...and 10 more exceptions.

Stacktrace:
 [1] threading_run(fun::var"#1525#threadsfor_fun#154"{var"#1525#threadsfor_fun#153#155"{UnitRange{Int64}}}, static::Bool)
   @ Base.Threads ./threadingconstructs.jl:171
 [2] macro expansion
   @ Main ./threadingconstructs.jl:219 [inlined]
 [3] test_threads()
   @ Main ./REPL[16]:3
 [4] top-level scope
   @ REPL[18]:1 

[gkronber]

I do not understand exactly how the rules are compiled, but I guess that the compiled rules (generated functions) are shared over all threads and I suspect that the generated patterns are shared as well. This means that updating the pattern nodes is a race condition and not allowed. For example as here:

function instantiate_enode!(bindings, @nospecialize(g::EGraph), p::PatLiteral)::Id
  add_constant_hashed!(g, p.value, v_head(p.n))
  add!(g, p.n, true)
end

instantiate_enode!(bindings, @nospecialize(g::EGraph), p::PatVar)::Id = v_pair_first(bindings[p.idx])
function instantiate_enode!(bindings, g::EGraph{ExpressionType}, p::PatExpr)::Id where {ExpressionType}
  add_constant_hashed!(g, p.head, p.head_hash)

  for i in v_children_range(p.n)
    @inbounds p.n[i] = instantiate_enode!(bindings, g, p.children[i - VECEXPR_META_LENGTH])
  end
  add!(g, p.n, true)
end

function instantiate_enode!(bindings, g::EGraph{Expr}, p::PatExpr)::Id
  add_constant_hashed!(g, p.quoted_head, p.quoted_head_hash)
  v_set_head!(p.n, p.quoted_head_hash)

  for i in v_children_range(p.n)
    @inbounds p.n[i] = instantiate_enode!(bindings, g, p.children[i - VECEXPR_META_LENGTH])
  end
  add!(g, p.n, true)
end

Should be easy to test if this is the problem by just creating new VecExprs immediately instead of cloning them in add!()

[0x0f0f0f]

I do not understand exactly how the rules are compiled, but I guess that the compiled rules (generated functions) are shared over all threads and I suspect that the generated patterns are shared as well. This means that updating the pattern nodes is a race condition and not allowed. For example as here:

function instantiate_enode!(bindings, @nospecialize(g::EGraph), p::PatLiteral)::Id
  add_constant_hashed!(g, p.value, v_head(p.n))
  add!(g, p.n, true)
end

instantiate_enode!(bindings, @nospecialize(g::EGraph), p::PatVar)::Id = v_pair_first(bindings[p.idx])
function instantiate_enode!(bindings, g::EGraph{ExpressionType}, p::PatExpr)::Id where {ExpressionType}
  add_constant_hashed!(g, p.head, p.head_hash)

  for i in v_children_range(p.n)
    @inbounds p.n[i] = instantiate_enode!(bindings, g, p.children[i - VECEXPR_META_LENGTH])
  end
  add!(g, p.n, true)
end

function instantiate_enode!(bindings, g::EGraph{Expr}, p::PatExpr)::Id
  add_constant_hashed!(g, p.quoted_head, p.quoted_head_hash)
  v_set_head!(p.n, p.quoted_head_hash)

  for i in v_children_range(p.n)
    @inbounds p.n[i] = instantiate_enode!(bindings, g, p.children[i - VECEXPR_META_LENGTH])
  end
  add!(g, p.n, true)
end

Should be easy to test if this is the problem by just creating new VecExprs immediately instead of cloning them in add!()

True! @gkronber - we could try adjusting this in this PR

[codecov-commenter]

⚠️ Please install the to ensure uploads and comments are reliably processed by Codecov.

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 81.22%. Comparing base (0b2e6c9) to head (52b4846).
Report is 6 commits behind head on ale/3.0.

❗ Your organization needs to install the Codecov GitHub app to enable full functionality.

Additional details and impacted files

@@             Coverage Diff             @@
##           ale/3.0     #244      +/-   ##
===========================================
+ Coverage    81.06%   81.22%   +0.16%     
===========================================
  Files           19       19              
  Lines         1500     1513      +13     
===========================================
+ Hits          1216     1229      +13     
  Misses         284      284              

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[0x0f0f0f]

@gkronber do you mind contributing a small MWE of the problem to this branch as a test?

[gkronber]

Problem occurrs only in multi-threaded scenarios. I'm not sure how I could enforce an environment with multiple threads for a single test case. But I can have a look. Any hints are appreciated.

[gkronber]

While the race conditions for accessing p.n in instantiate_node! are easy to fix, this is not the only problem. The nodes in patterns are also accessed within the compiled matching functions (see bind_expr) and from lookup_pat.

[0x0f0f0f]

Problem occurrs only in multi-threaded scenarios. I'm not sure how I could enforce an environment with multiple threads for a single test case. But I can have a look. Any hints are appreciated.

@gkronber We have to set JULIA_NUM_THREADS in CI config

[gkronber]

I added a test that fails because of a race condition and changed the number of threads for the CI pipeline.

[gkronber]

Interestingly, 5398503 was sufficient to solve the problem for me. I've the feeling that it is only a partial fix, because the nodes in the patterns are shared and mutated from lookup_pattern as well as in ematching.

[olynch]

It seems to me like not copying would be a bug, even in the case of non-multithreading!

[0x0f0f0f]

Copying is done in add!

[olynch]

Interestingly, 5398503 was sufficient to solve the problem for me. I've the feeling that it is only a partial fix, because the nodes in the patterns are shared and mutated from lookup_pattern as well as in ematching.

Why would we ever want to mutate the pattern? That seems fundamentally ill-advised...

[0x0f0f0f]

Interestingly, 5398503 was sufficient to solve the problem for me. I've the feeling that it is only a partial fix, because the nodes in the patterns are shared and mutated from lookup_pattern as well as in ematching.

Why would we ever want to mutate the pattern? That seems fundamentally ill-advised...

@olynch that was an optimization to not allocate memory all the times, do you have any suggestion?

[olynch]

Could we maybe add some spare memory, indexed by thread id, to each pattern? Then that spare memory could be used in each thread to avoid allocation, and we wouldn't need to mutate the pattern?