"constraint not satisfiable" error message is not deterministic

[joelanford]

In operator-framework/operator-controller#352, I fixed a bug to make sure that operator-controller checks for unsat errors. To complete the fix, I also updated an e2e test to change the assertion on the message that is reported in the Resolved condition.

It turns out the assertion is flaky because the content of the message changes from run to run, only in terms of the order in which the individual constraint messages appear. This is problematic when this error message is written to a kubernetes status object because it results in a reconcile -> update status -> reconcile -> update status loop until we get "lucky" and deppy returns the same message two reconciles in a row.

Is is possible to update deppy to return a deterministic value for the unsat error message?

[joelanford]

In addition to making the order deterministic, I'd propose that we use ; instead of , as a delimiter because commas are often present an individual constraint string. Semi-colons make it a bit easier to grok the message, IMO.

[joelanford]

For now, I resorted to the following:

// prettyUnsatMessage ensures that the unsat message is deterministic and
// human-readable. It sorts the individual constraint strings lexicographically
// and joins them with a semicolon (rather than a comma, which the unsat.Error()
// function does). This function also has the side effect of sorting the items
// in the unsat slice.
func prettyUnsatMessage(unsat deppy.NotSatisfiable) string {
	sort.Slice(unsat, func(i, j int) bool {
		return unsat[i].String() < unsat[j].String()
	})
	msgs := make([]string, 0, len(unsat))
	for _, c := range unsat {
		msgs = append(msgs, c.String())
	}
	return fmt.Sprintf("constraints not satisfiable: %s", strings.Join(msgs, "; "))
}

[m1kola]

t turns out the assertion is flaky because the content of the message changes from run to run, only in terms of the order in which the individual constraint messages appear.

I strongly suspect that this is due to how operator-controller builds the problem. For example, here we iterate over a map and create new variables. Map order is random.

[joelanford]

Is it reasonable for deppy to handle this itself, regardless of the way the problem was built?

[m1kola]

My first instinct is to keep Deppy as thin as possible and not involve it in sorting. It feels more like user domain.

It still might be a good idea to make sure that Deppy outputs errors in a certain order. For example, if we can say "Deppy guarantees to output errors in the same order as it receives input variables" we can let Deppy users decide and control ordering. But I haven't looked into what is going on on the Deppy side yet: maybe this is what already happens.

[joelanford]

I think that's reasonable. I think as long as deppy's output is deterministic from its input, it will have met its obligations.

[m1kola]

Let's summarise this issue as:

• We need to ensure deppy's output is deterministic from its input
• If it already is, make sure that there are tests for this or add tests

---

In addition to making the order deterministic, I'd propose that we use ; instead of , as a delimiter because commas are often present an individual constraint string. Semi-colons make it a bit easier to grok the message, IMO.

I created a separate issue #150 for this.

[m1kola]

I did some digging and I can confirm that the order of AppliedConstraints in NotSatisfiable error is non deterministic on Deppy level. So while there was the issue on operator-controller side - we also have on in Deppy.

This can be seen if we remove this piece of code from the Deppy test:

deppy/internal/solver/solve_test.go

Lines 310 to 337 in 0a012d2

	// Failed constraints are sorted in lexically
	// increasing Order of the identifier of the
	// constraint's variable, with ties broken
	// in favor of the constraint that appears
	// earliest in the variable's list of
	// constraints.
	var ns deppy.NotSatisfiable
	if errors.As(err, &ns) {
	sort.SliceStable(ns, func(i, j int) bool {
	if ns[i].Variable.Identifier() != ns[j].Variable.Identifier() {
	return ns[i].Variable.Identifier() < ns[j].Variable.Identifier()
	}
	var x, y int
	for ii, c := range ns[i].Variable.Constraints() {
	if reflect.DeepEqual(c, ns[i].Constraint) {
	x = ii
	break
	}
	}
	for ij, c := range ns[j].Variable.Constraints() {
	if reflect.DeepEqual(c, ns[j].Constraint) {
	y = ij
	break
	}
	}
	return x < y
	})
	}

Order of AppliedConstraint will constantly be changing.

[m1kola]

I think the source of nondeterminism is in this function:

deppy/internal/solver/lit_mapping.go

Lines 144 to 148 in ddaf504

	func (d *litMapping) AssumeConstraints(s inter.S) {
	for m := range d.constraints {
	s.Assume(m)
	}
	}

We iterate over d.constraints which is a map and order is random in Go.