Partial solution map

[mpizenberg]

This idea of this PR is to unify the history and memory into a single hash map. This should in theory speedup conflict resolution since we only have to access packages related to a satisfied incompatibility, and do not have to scan through the whole history. It is possible that this should also speedup backtracking since keeping decision level ranges for each package can enable skipping entirely to recompute term intersections for packages where all assignments appear previous to the backtracking decision level.

In practice, things might differ due to the implementation I did.

Also, this does not pass the tests, so I must have introduced a bug somewhere.

[Eh2406]

I pushed some code to compere the two to try and find the bug. It really looks like it is in previous_satisfier_level. But I cant find the exact problem.

[mpizenberg]

So I've fixed the behavior of the old partial_solution to return the correct decision level in case there is no previous satisfier. I suppose this didn't prevent the code from working but still hurt performances? Maybe there will be a performance change after this is integrated?

Now that this is fixed, I've identified an issue when backtracking by adding some debug logs. After backtracking to level 1 in the "conflict_resolution" unit test, the old partial solution contains in memory the following for package foo:

"foo": Derivations(
    Positive( Range { segments: [
        (
            SemanticVersion { major: 1, minor: 0, patch: 0, },
            None,
        ),
    ], }, ),
),

while in partial_solution_bis, I see

dated_derivations: [
    DatedDerivation {
        global_index: 2,
        decision_level: DecisionLevel(1),
        cause: Id::<SemanticVersion>>(1),
    },
],
assignments_intersection: Derivations(
    Negative( Range { segments: [] } ),
),

It's weird that the assignments_intersection is wrong while the dated_derivations contains the right derivations and the intersection is built by folding other dated derivations.

[mpizenberg]

Ahhh :facepalm: I was doing

acc.intersection(&term);
acc

instead of returning

acc.intersection(&term)

directly in the fold. That's what I get when switching from pure languages like Elm to Rust XD, I'm confusing what gets mutated and what does not ^^.

Anyway, that was one problem, but there are still others.

[mpizenberg]

Ok so now even the old partial_solution crashes (I guess due to the change I made to decision level). I'll have to dig deeper.

[mpizenberg]

WARNING: run all the tests, it may crash your computer (memory go to swap). I did not figure out how to increase the number of property tests shrinking for some of those that fail fast like prop_passes_int. I'd love to try getting a simple setup where this new partial_solution with fixed decision level crashes. Right now I'm only getting quite big tests cases.

[mpizenberg]

Alright, sorry I've been confusing myself, and maybe others, and as a result writing and coding wrong stuff. So here are some clarifications on the satisfier and previous satisfier search.

If there exists at least one assignment related to the incompatibility prior to the satisfier, whether or not it is the same package than the satisfier, we are guaranted to have a previous satisfier by construction.

So the only way there could be no previous satisfier is if:

• There is only one package (the satisfier one) in incompat
• There is no derivation prior to the satisfier for that package

Now let's explain why both the previous find_previous_satisfier and the modification I introduced are wrong and how to fix it.

In the previous code on partial_solution for the find_previous_satisfier function, we were passing as argument

previous_assignments = &self.history[0..=satisfier_idx]

and computing the previous satisfier decision level as:

previous_assignments[*satisfier_map.values().max().unwrap()]
    .decision_level
    .max(DecisionLevel(1))

This was wrong in the case where there is no assignment before the satisfier for the satisfier package. Because in such case, satisfier_map[satisfier_package] was never updated, and by definition will be the same than the satisfier and thus the same decision level. But in reality, it should behave differently.

• If there exists another package related to the satisfied incompatibility (so its length is > 1) then one of this other packages will be the previous satisfier package and its decision level may differ from the one of the satisfier.
• And if there exists no other package (the incompat has only one package), then it means (since there is no previous assignment) that there is no previous satisfier, and we must return DecisionLevel(1).

Now in my modified version of that function, I changed previous assignments argument to exclude the satisfier:

previous_assignments = &self.history[0..satisfier_idx]

and rewrote the previous decision level computation to:

        previous_assignments
            .get(*satisfier_map.values().max().unwrap())
            .map(|a| a.decision_level)
            .unwrap_or(DecisionLevel(1))
            .max(DecisionLevel(1))

Now this is also wrong. In the case there is no previous assignment related to the satisfier package, we still keep the max as being the one of the satisfier. But this time, when we try to get it, we get None because it isn't present in the previous assignments anymore and replace it by the decision level 1. However this is only correct when the incompatibility does not have another package, as explained at the beginning of this comment.

So, finally, to fix this situation, it seems that the correct implementation is to do two things, (1) truncate the previous satisfier slice before the satisfier:

previous_assignments = &self.history[0..satisfier_idx]

and remove the satisfier package from the satisfier_map before iterating over previous assignments:

        satisfier_map.remove(&package);

Then we compute the previous decision level as follows:

        if satisfier_map.is_empty() {
            DecisionLevel(1)
        } else {
            previous_assignments[*satisfier_map.values().max().unwrap()]
                .decision_level
                .max(DecisionLevel(1))
        }

[mpizenberg]

Alright, I've fixed partial_solution_bis too and it's now passing the tests :) Now I need to clean everything up and run some benchmarks!

[mpizenberg]

So the change I introduced to correctly follow pub instructions has a huge perf downside! The zuse bench basically went from 360ms to 710ms. But it appears both pass the tests, so it means that the fact they are taking a different path in the resolution has a big impact on performances.

Concretely, in my fix, when there is no previous derivation for the satisfier package, we will often return the decision level of another package, which may be smaller than the satisfier decision level, resulting in that branch of the algorithm:

If satisfier is a decision or if previousSatisfierLevel is different than satisfier's decision level: (1) save incompat, (2) backtrack, (3) return incompat

While in the implementation previous to my fix (which you can get by just changing ..satisfier_idx into ..=satisfier_idx), everytime there is no previous derivation in the satisfier package, we keep the satisfier index in the map, and therefore will return the same decision level for previous satisfier. We endup in the algorithm branch:

Otherwise, (1) let priorCause be the union of the terms in incompatibility and the terms in satisfier's cause, minus the terms referring to satisfier's package. (2) If satisfier doesn't satisfy term, add not (satisfier \ term) to priorCause. (rule of resolution) (3) Set incompatibility to priorCause.

So basically, the previous approach tend to call backtrack less often I suppose? or maybe it's something else like too much memory usage for incompatibilities? I'd love if you could have a look at that @Eh2406 too, let me know what you think.

[mpizenberg]

Now if I get back to the discussion of the new partial solution implementation with a single hashmap I am optimistic about the performances. Due to how I structured my code. For the time being I can only fairly compare it to the old partial solution implementation with the algorithm path based on the previous assignments slice ..satisfier_idx. I'd have to change a few things to compare with the algorithm path taken when previous assignments slice is ..=satisfier_idx.

But in the first case, for this new implementation in partial_solution_bis compared to partial_solution, I'm getting quite good performance improvements:

Benchmarking large_cases/elm_packages_str_SemanticVersion.ron: Warming up for 3.0000 s
Warning: Unable to complete 100 samples in 20.0s. You may wish to increase target time to 23.1s, or reduce sample count to 80.
large_cases/elm_packages_str_SemanticVersion.ron
                        time:   [219.46 ms 221.46 ms 223.33 ms]
                        change: [-1.3992% -0.4222% +0.4799%] (p = 0.39 > 0.05)
                        No change in performance detected.
Found 16 outliers among 100 measurements (16.00%)
  15 (15.00%) low severe
  1 (1.00%) low mild
Benchmarking large_cases/zuse_str_SemanticVersion.ron: Warming up for 3.0000 s
Warning: Unable to complete 100 samples in 20.0s. You may wish to increase target time to 61.9s, or reduce sample count to 30.
large_cases/zuse_str_SemanticVersion.ron
                        time:   [584.69 ms 588.50 ms 592.08 ms]
                        change: [-17.720% -17.014% -16.291%] (p = 0.00 < 0.05)
                        Performance has improved.
Found 24 outliers among 100 measurements (24.00%)
  23 (23.00%) low severe
  1 (1.00%) low mild
large_cases/large_case_u16_NumberVersion.ron
                        time:   [10.142 ms 10.203 ms 10.269 ms]
                        change: [-2.6538% -1.8760% -1.0098%] (p = 0.00 < 0.05)
                        Performance has improved.

[Eh2406]

Sounds like there are 2 things in this. 1. a change to what find_previous_satisfier returns. 2. a change to the data structure. Should we do it as 2 PR?

[mpizenberg]

Sounds like there are 2 things in this. 1. a change to what find_previous_satisfier returns. 2. a change to the data structure. Should we do it as 2 PR?

Yes this should be 2 distinct PRs. It's just that I stumbled upon that while reimplementing the _bis way because I had to re-read the documentation to make sure I'm doing things right. This PR is a bit of a mess with all the stuff I'm experimenting at the same time even though all that was necessary to get to that point. Once I'm done experimenting, I'll do a first PR regarding the change to find_previous_satisfier so that things get clearer.

[Eh2406]

I wonder if this got messed up in #79, if so sorry.

[mpizenberg]

I wonder if this got messed up in #79, if so sorry.

Indeed, that PR introduces a behavior change due to returning a different previous satisfier decision level but we would not have spotted that performance opportunity (due to different behavior) without your PR so it's fine :)

[Eh2406]

I wonder if there are asserts we can add to make shore that find_previous_satisfier and find_satisfier are returning the correct thing, during our existing tests. And are there ways to make tests (or better prop tests) that test it in isolation.