Skip to content
This repository has been archived by the owner on Feb 1, 2020. It is now read-only.

Problem in ConstrainedTerm.evaluateConstraints #2408

Open
kheradmand opened this issue Apr 2, 2018 · 1 comment
Open

Problem in ConstrainedTerm.evaluateConstraints #2408

kheradmand opened this issue Apr 2, 2018 · 1 comment

Comments

@kheradmand
Copy link
Contributor

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 kheradmand changed the title Problem in ConstrainedTerm.evaluateConstraints (possibly a concurrency bug) Problem in ConstrainedTerm.evaluateConstraints Apr 2, 2018
@kheradmand
Copy link
Contributor Author

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.

kheradmand added a commit to kframework/p4-semantics that referenced this issue Apr 4, 2018
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant