Stream: t-cargo/PubGrub

Topic: There is a bug! https://github.com/mpizenberg/pubgrub-rs/...


view this post on Zulip Eh2406 (Oct 08 2020 at 02:53):

Ok so I can't fuzz to make sure two runs have the same output, because it mostly depends on the hashing. That may get fixed tomorrow, but in the meantime, I can test that two runs ether bouth pass or both fail. Something's not right if one passes and one fails. Inspired by a related test in cargo https://github.com/rust-lang/cargo/blob/master/crates/resolver-tests/tests/resolve.rs#L93. Run the proptest code and get a wall of failing. Rerun with the output in ron format, and hand minimize. and here is the case:

view this post on Zulip Eh2406 (Oct 08 2020 at 02:53):

{
    0:{
        0:{}
    },
    1:{
        2:{}
    },
    2:{
        0:{},
        1:{
            1:[(0,Some(1))]
        }
    },
    3:{
        0:{
            1:[(3,None)]
        },
        1:{
            1:[(2,None)]
        },
    },
    4:{
        0:{
            2:[(0,None)],
            3:[(0,None)]
        }
    }
}

view this post on Zulip Eh2406 (Oct 08 2020 at 02:55):

Driven by:

#[cfg(feature = "serde")]
#[test]
fn err_the_same_1() {
    let s = std::fs::read_to_string("test-examples/err_the_same_u16_NumberVersion.ron").unwrap();
    let dependency_provider: OfflineDependencyProvider<u16, NumberVersion> =
        ron::de::from_str(&s).unwrap();

    let one = resolve(&dependency_provider, 4, 0).is_ok();
    for _ in 0..5 {
        assert_eq!(one, resolve(&dependency_provider, 4, 0).is_ok())
    }
}

view this post on Zulip Eh2406 (Oct 08 2020 at 02:58):

Most of the time the resolve returns

Ok(
    {
        2: NumberVersion(
            0,
        ),
        1: NumberVersion(
            2,
        ),
        4: NumberVersion(
            0,
        ),
        3: NumberVersion(
            1,
        ),
    },
)

but about 1/3 calls return an error. That feels to me like there has to be a bug somewhere.

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 08:34):

Indeed! I'll have a look at this one tonight

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 08:50):

Just rewriting it with letters and numbers to make it easier to analyze later

a0 has no dep
b2 has no dep
c0 has no dep
c1 dep on b0
d0 dep on b>=3
d1 dep on b>=2
e0 dep on c and d

Solution: e0, d1, b2, c0

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 09:13):

Alright, simplified this a bit, we get to that test, that has the same issues as described:

use std::collections::HashMap;

use pubgrub::error::PubGrubError;
use pubgrub::range::Range;
use pubgrub::report::{DefaultStringReporter, Reporter};
use pubgrub::solver::{resolve, OfflineDependencyProvider};
use pubgrub::version::NumberVersion;

#[test]
/// a0 dep on b and c
/// b0 dep on d0
/// b1 dep on d1 (not existing)
/// c0 has no dep
/// c1 dep on d2 (not existing)
/// d0 has no dep
///
/// Solution: a0, b0, c0, d0
fn problem() {
    let mut dependency_provider = OfflineDependencyProvider::<&str, NumberVersion>::new();
    dependency_provider.add_dependencies("a", 0, vec![("b", Range::any()), ("c", Range::any())]);
    dependency_provider.add_dependencies("b", 0, vec![("d", Range::exact(0))]);
    dependency_provider.add_dependencies("b", 1, vec![("d", Range::exact(1))]);
    dependency_provider.add_dependencies("c", 0, vec![]);
    dependency_provider.add_dependencies("c", 1, vec![("d", Range::exact(2))]);
    dependency_provider.add_dependencies("d", 0, vec![]);

    // Solution.
    let mut expected_solution = HashMap::new();
    expected_solution.insert("a", 0.into());
    expected_solution.insert("b", 0.into());
    expected_solution.insert("c", 0.into());
    expected_solution.insert("d", 0.into());

    // Run the algorithm.
    for _ in 0..10 {
        match resolve(&dependency_provider, "a", 0) {
            Ok(computed_solution) => assert_eq!(expected_solution, computed_solution),
            Err(PubGrubError::NoSolution(derivation_tree)) => {
                panic!("{}", DefaultStringReporter::report(&derivation_tree));
            }
            Err(err) => panic!("{:?}", err),
        };
    }
}

Don't hesitate to have a try at figuring it out. I'll have a try tonight

view this post on Zulip Alex Tokarev (Oct 08 2020 at 10:38):

Don't hesitate to have a try at figuring it out.

If only I could work on this full time :D

view this post on Zulip Eh2406 (Oct 08 2020 at 14:28):

If you find that job, can I get highered too?

view this post on Zulip Eh2406 (Oct 08 2020 at 14:37):

the report is

Because there is no version of b in 2 <= v and b 0 depends on d 0, b [ 0, 1 [  [ 2, ∞ [ depends on d 0.
And because b 1 depends on d 1 and a 0 depends on b, a 0 is forbidden.

@Matthieu Pizenberg Do you have advice on how to start debugging?

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 15:17):

I think it's an instance of a bug I've been chasing for quite some time. I'll let you know where to put some println as a start

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 15:25):

So it's an issue related to computation of prior causes. So the first thing I'd do is uncomment and slightly change the three commented lines in core.rsjust after computation of prior cause. Something like

eprintln!("\ncause 1: {}", &current_incompat);
eprintln!("cause 2: {} (satisfier)", &cause);
eprintln!("prior cause: {}\n", &prior_cause);

and add a eprintln!("backtrack"); in core::State::backtrack function to cover all branches of conflict resolution

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 15:36):

If you do this, at some point in there will be something like this:

cause 1: b [ 0, 1 [  [ 2,  [ depends on d 0
cause 2: b 1 depends on d 1 (satisfier)
prior cause: b  is forbidden

This is a weird situation because we have to compute prior cause something in the form of { a1, not b1} with something of the form {a2, not b2} which will result in something of the form {a1 union a2, not b1 union not b2}, with the "not b1 union not b2" that may return "not none" which is always satisfied and thus removed from the incompatibility. Leaving us with the "a1 union a2" side, which here is "b * is forbidden" , i.e. { b: any }

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 15:38):

The issue here comes either from the fact that the two causes are not good, or from the fact that prior computation is not good.
And these corresponds to places where we might have some misinterpretation of my part from pubgrub description on github. Specifically ...

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 15:44):

The documentation uses incompatibility everywhere for things that are function arguments and mutated in place. In particular, in unit propagation (https://github.com/dart-lang/pub/blob/master/doc/solver.md#unit-propagation) it says to "run conflict resolution with incompatibility" and later "Add not term to the partial solution with incompatibility as its cause" whereas meanwhile conflict resolution also uses the word incompatibility and mutates it in place with prior causes. I have not looked at dart code, but from my tests in elm, it "worked" (most of the time) when I used the root cause returned by conflict resolution as its cause. And when it didn't (this very bug) changing to the original incompatibility would not solve it.

BUT, that may be a side effect of the second place where interpretation plays a role in that document ...

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 15:53):

At the end of the conflict resolution algorithm (https://github.com/dart-lang/pub/blob/master/doc/solver.md#conflict-resolution) there is an explanation of how to compute a prior cause, and it is pretty confusing. While the general text above says things pretty clear like

In fact, we can generalize this: given any incompatibilities {t1, q} and {t2, r}, we can derive {q, r, t1 ∪ t2}

the actual algorithm description does something very twisted, using new type of operations like the set \ as in not (satisfier \ term). Every time I've tried to analyze this deeply I came to the conclusion that all operations with the terms of that package are the same than doing term union not(satisfier) and remove it if that becomes not none which is always satisfied. And that itself was the same as just doing the union of all the terms in the two causes (but I may be wrong here) and applying the same removal for other packages always satisfied.

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 15:55):

I'm pretty sure I've done every variation that may be a correct interpretation of those things. But I've never looked at the dart code so ... maybe the key is here

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 15:57):

Or maybe, this is not a problem in unit propagation or conflict resolution but a side effect of a problem somewhere else. But that's why I've put a lot of property testing of the other base components of this algorithm like range, or term.

I hope that since you have a fresh eye on this, you'll see what I didn't

view this post on Zulip Eh2406 (Oct 08 2020 at 15:57):

This all sounds like it has been a lot of work on your part and very frustrating.

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 15:58):

Yes that has been frustration number 1 ahah

view this post on Zulip Eh2406 (Oct 08 2020 at 15:59):

And exactly why I want fuzz testing on as much as possible. It is so hard to look at an algorithm (in words or code) and be sure it is correct.

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 15:59):

And before you came up with that example, everywhere I had seen this manifest, saying there was no solution was actually the right answer, even if the reason it found didn't make much sense

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 16:00):

So I was in doubt, but thinking, maybe it works but the slight variations I have make it so the explanation is a bit weird

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 16:02):

In a way, it's almost a satisfaction that you proved it's a bug. I'm not in doubt anymore ahah

view this post on Zulip Eh2406 (Oct 08 2020 at 16:07):

That is a relief. I was worried you'd be upset. I was pretty upset when proptest found its first bug in stable functionality in Cargo, and I was the one that wrote the test.

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 16:09):

Don't worry, I'm dealing with researcher code on a daily basis, I'm used to things being broken in very subtle algorithmic ways ^^. It's way better to have a simple example of why that's broken

view this post on Zulip Eh2406 (Oct 08 2020 at 16:13):

so far I added the eprintln you suggested. Still figuring out what it means.

start

cause 1: b 2 <= v is forbidden
cause 2: b 0 depends on d 0
prior cause: b [ 0, 1 [  [ 2, ∞ [ depends on d 0


cause 1: b [ 0, 1 [  [ 2, ∞ [ depends on d 0
cause 2: b 1 depends on d 1
prior cause: b ∗ is forbidden


cause 1: b ∗ is forbidden
cause 2: a 0 depends on b
prior cause: a 0 is forbidden

thread 'problem' panicked at 'Because there is no version of b in 2 <= v and b 0 depends on d 0, b [ 0, 1 [  [ 2, ∞ [ depends on d 0.
And because b 1 depends on d 1 and a 0 depends on b, a 0 is forbidden.'

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 16:15):

those are the two incompatibilities used to compute a prior cause incompatibility in one step of the conflict resolution loop

view this post on Zulip Eh2406 (Oct 08 2020 at 16:22):

As I am reading it:

cause 1: b [ 0, 1 [  [ 2, ∞ [ depends on d 0
cause 2: b 1 depends on d 1
prior cause: b ∗ is forbidden

is just wrong.
cause 1: I read as b not v1 depends on d0, which is an odd way of saying it but is true.
cause 2: I read as b1depends on d1, witch is straightforwardly true.
prior cause: is just wrong. and does not follow.

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 16:41):

So the first one would read "Every version of b except version 1 depend on d0"

view this post on Zulip Eh2406 (Oct 08 2020 at 16:41):

and that is true

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 16:42):

It's just that I didn't implement a check for such situation so it just prints the segments (which are equivalent to every of except 1)

view this post on Zulip Eh2406 (Oct 08 2020 at 16:43):

Yes. That makes sence.

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 16:43):

As for the prior cause, it's indeed not logical, but that's what computing the union of terms gives

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 16:44):

99% of the time, we have {a, not b} and {b, not c} as in "a depends on b" and "b depends on c"

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 16:45):

the union of all terms give {a, b union not(b), c}, but "b union not(b)" resolves to "not none" which is always satisfied so it is removed

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 16:47):

That's what says the rule of resolution explained here: https://github.com/dart-lang/pub/blob/master/doc/solver.md#conflict-resolution

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 16:47):

It might take some time to digest it all

view this post on Zulip Eh2406 (Oct 08 2020 at 16:50):

I think the next step for me, is to make a test that directly calls Incompatibility::union with that one case. Well actually I have a meeting in 10, witch will make me mad, so then I will need a walk. Then I will try to redigest that reading materials vis this case.

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 16:55):

But sometimes, the search for a satisfier (whose incompatibility cause is used for computation of the prior cause) makes us work with to incompats of the form {a1, b1} {a2, b2} where both incompats refer to the same packages. And it gets weird when a1 and a2 are different. So I think I'd rather argue that it does not makes sense to use those two incompats to compute a prior cause but that would mean that it's the search for the previous satisfier that's wrong, and I've read it multiple times

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 16:57):

Fuzzing the satisfier search would be great, but I'm not sure how to do that. Anyway the best solution is maybe just have a look at the dart implementation on those very points

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 17:37):

ooohh, I've just had a quick look at dart pub implementation. I'm seeing an intersection here where terms of the two causes used for prior cause are merged: https://github.com/dart-lang/pub/blob/23a59a380cdc88aca6a50f9b0147ecdd3b948919/lib/src/solver/incompatibility.dart#L68
That might be the reason ...
Have to go now, so I'll continue looking later but seems promising

view this post on Zulip Eh2406 (Oct 08 2020 at 17:42):

Good find!
In case it is helpful here is the isolated test case I was working on:

    #[test]
    fn bad_union() {
        use crate::version::NumberVersion;
        let i1: Map<&str, Term<NumberVersion>> = [
            ("d", Term::Negative(Range::exact(0))),
            ("b", Term::Positive(Range::exact(1).negate())),
        ]
        .iter()
        .cloned()
        .collect();
        let i2: Map<&str, Term<NumberVersion>> = [
            ("d", Term::Negative(Range::exact(1))),
            ("b", Term::Positive(Range::exact(1))),
        ]
        .iter()
        .cloned()
        .collect();

        assert_eq!(
            [("b", Term::Positive(Range::<NumberVersion>::any()))]
                .iter()
                .cloned()
                .collect::<Map<_, _>>(),
            Incompatibility::union(8, &i1, &i2, Kind::DerivedFrom(7, 4)).package_terms
        );
    }

If we decide that is at fault.

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 18:45):

Test is passing :)

I'll clean up a bit my mess and make a PR

view this post on Zulip Eh2406 (Oct 08 2020 at 18:51):

I look forward to reading the explanation, and fuzzing more!

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 18:53):

Explanation is basically I had the wrong assumptions about what the following meant

let priorCause be the union of the terms in incompatibility and the terms in satisfier's cause

view this post on Zulip Alex Tokarev (Oct 08 2020 at 19:00):

Great job @Matthieu Pizenberg for solving this and @Eh2406 for reporting and submitting test cases!
Looks like I wasn't on time to participate with this much. At least I managed to make determinism PR satisfactory while you were busy here :)

view this post on Zulip Alex Tokarev (Oct 08 2020 at 19:04):

I think we should make a test case that reproduces this on top of determinism PR. I'll check if the test submitted by @Eh2406 fails when using rustc-hash hash function.

view this post on Zulip Eh2406 (Oct 08 2020 at 19:10):

Note that the original version (and the one I can use for fuzzing) will always pass with any form of determinism. N calles will always return the same thing. We will need better properties to know if it is the correct thing.

view this post on Zulip Alex Tokarev (Oct 08 2020 at 19:10):

Unfortunately both original with RON and minified pass. @Eh2406 How did you generate the first test case? Maybe I could make one that would fail with rustc-hash.

view this post on Zulip Alex Tokarev (Oct 08 2020 at 19:12):

Yeah I see. I thought one of them produces Err solution from time to time.

view this post on Zulip Eh2406 (Oct 08 2020 at 19:15):

Right, without determinism we can check if run1.is_ok() == run2.is_ok()and find a bug when it is not. With determinism we can check run1 == run2 and have it always pass.

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 19:15):

That test case was found thanks to the awesome property of not being reproducible lol.
Well it's true, but I'm kidding here since we do want to be able to reproduce people bugs

view this post on Zulip Eh2406 (Oct 08 2020 at 19:17):

The only reason to let a user pick the hasher (that I can think of) is to have the proptest:
run_with_hash_1.is_ok() == run_with_hash_2.is_ok()

view this post on Zulip Eh2406 (Oct 08 2020 at 19:18):

But it is not worth threading a HashBuilder type everyware.

view this post on Zulip Matthieu Pizenberg (Oct 08 2020 at 19:33):

https://github.com/mpizenberg/pubgrub-rs/pull/23 fix :)

view this post on Zulip Eh2406 (Oct 08 2020 at 19:34):

I will try the fuzz test on it, before we have a chance to merge the determinism.

view this post on Zulip Eh2406 (Oct 08 2020 at 19:44):

Rebased, and running 3 times its passing

view this post on Zulip Matthieu Pizenberg (Oct 09 2020 at 11:22):

I did a little write up of my thoughts on the prior cause computation with incompatibilities. It's a bit "mathy" but I hope it is still clear: https://github.com/mpizenberg/pubgrub-rs/pull/23#issuecomment-706122058


Last updated: Oct 21 2021 at 21:46 UTC