kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

Problem in ConstrainedTerm.evaluateConstraints #2408

Open kheradmand opened 6 years ago

kheradmand commented 6 years ago

I can not give a small example here, but sometimes when I use krun, a rule that I expect to apply, does not get normally applied, but when I use a debugger and go step by step, the rule gets applied. I tried to narrow the scope of the problem, the problem seems to be in the function ConstrainedTerm.evaluateConstraints:

public static List<Triple<ConjunctiveFormula, Boolean, Map<scala.collection.immutable.List<Pair<Integer, Integer>>, Term>>> evaluateConstraints(
            ConjunctiveFormula constraint,
            ConjunctiveFormula subjectConstraint,
            ConjunctiveFormula patternConstraint,
            Set<Variable> variables,
            TermContext context) {
        context.setTopConstraint(subjectConstraint);
        List<ConjunctiveFormula> candidates = constraint.getDisjunctiveNormalForm().conjunctions().stream()
                .map(c -> c.addAndSimplify(patternConstraint, context))
                .filter(c -> !c.isFalse())
                .map(ConjunctiveFormula::resolveNonDeterministicLookups)
                .map(ConjunctiveFormula::getDisjunctiveNormalForm)
                .map(DisjunctiveFormula::conjunctions)
                .flatMap(List::stream)
                .map(c -> c.simplify(context))
                .filter(c -> !c.isFalse())
                .collect(Collectors.toList());
        int x = candidates.size(); //added by me
        List<Triple<ConjunctiveFormula, Boolean, Map<scala.collection.immutable.List<Pair<Integer, Integer>>, Term>>> solutions = Lists.newArrayList();
        for (ConjunctiveFormula candidate : candidates) {
            ...
        }
        ....

If I set a breakpoint after int x = candidates.size();, the value of x is 0 but if I put a break point right before that line and then evaluate one step, the value of x becomes 1.

I am not familiar with the code base (or Java 8 streams) but this phenomenon makes me suspect that this is a concurrency bug. Possibily

List<ConjunctiveFormula> candidates = ...

is being evaluated is being evaluated in a separate thread that has data race with the thread executing the rest of the function.

kheradmand commented 6 years ago

It is most probably not a concurrency problem because first of all I don't think there are multiple threads involved here, and second, even adding a long delay does not solve the problem:

public static List<Triple<ConjunctiveFormula, Boolean, Map<scala.collection.immutable.List<Pair<Integer, Integer>>, Term>>> evaluateConstraints(
            ConjunctiveFormula constraint,
            ConjunctiveFormula subjectConstraint,
            ConjunctiveFormula patternConstraint,
            Set<Variable> variables,
            TermContext context) {
        context.setTopConstraint(subjectConstraint);
        List<ConjunctiveFormula> candidates = constraint.getDisjunctiveNormalForm().conjunctions().stream()
                .map(c -> c.addAndSimplify(patternConstraint, context))
                .filter(c -> !c.isFalse())
                .map(ConjunctiveFormula::resolveNonDeterministicLookups)
                .map(ConjunctiveFormula::getDisjunctiveNormalForm)
                .map(DisjunctiveFormula::conjunctions)
                .flatMap(List::stream)
                .map(c -> c.simplify(context))
                .filter(c -> !c.isFalse())
                .collect(Collectors.toList());
        try {
            Thread.sleep(1000);
        } catch (InterruptedException e) {
            e.printStackTrace();
        }
        int x = candidates.size();
        List<Triple<ConjunctiveFormula, Boolean, Map<scala.collection.immutable.List<Pair<Integer, Integer>>, Term>>> solutions = Lists.newArrayList();
        for (ConjunctiveFormula candidate : candidates) {
            ...

I really don't know what the problem may be.