From 3093b4678c85ce26635143b5c6db30d5d69e0870 Mon Sep 17 00:00:00 2001 From: Grigorii Kirgizov Date: Fri, 17 Jul 2020 01:22:33 +0300 Subject: [PATCH] Implement incremental handling of discarded principal occurrences (MPSCR-65) Matches which discard principal occurrences must be handled specially on incremental execution. Imagine such match inserted in journal before other matches with the same occurrence in head. Because inserted match discards the occurrence, following matches can't match on it. They must be invalidated. (Relevant for MPSCR-62) See tests for substructuralTS. Commit refactors machinery of `dropDiscardingMatchesFor` in ConstraintsProcessing that was incomplete, as revealed by MPSCR-64. Relaxes small memory opt introduced in commit a2675351: Now justifications in Occurrences are not shared with their activating matches. See JustifiedOccurrenceCreator. Introduced machinery requires that Occurrences had their own Evidence (because `dropDiscarding` invalidates by Occurrences). Previously algorithm was invalidating Chunks only by Evidence from rule matches, that's why only RuleMatches had to have unique Evidence, while Occurrences could bear less info. --- .../core/internal/ConstraintsProcessing.kt | 126 ++++++++++++------ .../core/internal/ContinuedActivationQueue.kt | 4 +- .../reactor/core/internal/ControllerImpl.kt | 19 +-- .../reactor/core/internal/MatchJournal.kt | 21 +++ .../reactor/core/internal/MatchJournalImpl.kt | 28 +++- 5 files changed, 142 insertions(+), 56 deletions(-) diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ConstraintsProcessing.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ConstraintsProcessing.kt index 019871a3..c508699b 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ConstraintsProcessing.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ConstraintsProcessing.kt @@ -20,6 +20,8 @@ import jetbrains.mps.logic.reactor.core.* import jetbrains.mps.logic.reactor.evaluation.EvaluationTrace import jetbrains.mps.logic.reactor.program.IncrementalProgramSpec import jetbrains.mps.logic.reactor.evaluation.SessionToken +import jetbrains.mps.logic.reactor.logical.LogicalContext +import jetbrains.mps.logic.reactor.program.Constraint import jetbrains.mps.logic.reactor.program.Rule import jetbrains.mps.logic.reactor.util.Profiler import jetbrains.mps.logic.reactor.util.profile @@ -94,37 +96,44 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di // Remove chunk from the journal it.remove() - // 'Undo' all activated in this chunk occurrences - chunk.activatedLog().forEach { - dispatchingFront = dispatchingFront.forget(it) - } - if (chunk is MatchJournal.MatchChunk) { - trace.invalidate(chunk.match) - invalidatedRulesTags.add(chunk.ruleUniqueTag) + val validOccs = invalidateChunk(chunk, justificationRoots) - dispatchingFront = dispatchingFront.forget(chunk.match as RuleMatchEx) + activationQueue.offerAll(lastValidChunk.toPos(), validOccs) - // Valid head occurrences could match more rules - // without this match, so need to reactivate them. - // E.g. occurrences discarded in this match on - // previous run but revived here can match more rules. - val matchedOccs = chunk.match.allHeads() - val validOccs = matchedOccs.filter { occ -> - !occ.justifiedByAny(justificationRoots) - } - // By definition of Chunk and principal rule, - // all occurrences from the head are principal. - assert(chunk.match.allHeads().all { it.isPrincipal }) - - activationQueue.offerAll(lastValidChunk.toPos(), validOccs.asIterable()) - } } else { lastValidChunk = chunk } } } + private fun invalidateChunk(chunk: MatchJournal.Chunk, invalidJustifications: Collection): Iterable { + // 'Undo' all activated in this chunk occurrences + chunk.activatedLog().forEach { + dispatchingFront = dispatchingFront.forget(it) + } + + val validOccs: Sequence + if (chunk is MatchJournal.MatchChunk) { + trace.invalidate(chunk.match) + invalidatedRulesTags.add(chunk.ruleUniqueTag) + dispatchingFront = dispatchingFront.forget(chunk.match as RuleMatchEx) + + // Valid head occurrences could match more rules + // without this match, so need to reactivate them. + // E.g. occurrences discarded in this match on + // previous run but revived here can match more rules. + validOccs = chunk.match.allHeads().filter { occ -> + !occ.justifiedByAny(invalidJustifications) + } + // By definition of Chunk and principal rule, + // all occurrences from the head are principal. + assert(chunk.match.allHeads().all { it.isPrincipal }) + + } else validOccs = emptySequence() + return validOccs.asIterable() + } + fun addRuleMatches(rules: Iterable) { val activationCandidates = mutableListOf() @@ -207,14 +216,10 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di fun processActivated(controller: Controller, active: Occurrence, parent: MatchJournal.MatchChunk, inStatus: FeedbackStatus) : FeedbackStatus { push() - val activationChunk: MatchJournal.OccChunk? if (!active.stored) { active.stored = true - activationChunk = logActivation(active) + logActivation(active) active.revive(logicalState) - } else { - // defined (not null) & needed only for incremental execution - activationChunk = journalIndex.activatingChunkOf(active) } assert(active.alive) @@ -233,12 +238,6 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di } val outStatus = currentMatches.fold(inStatus) { status, match -> - if (activationChunk != null && !isFront()) { - if (match.discards(active)) { - dropDiscardingMatchesFor(activationChunk, invalidatedRulesTags) - } - } - // TODO: paranoid check. should be isAlive() instead // FIXME: move this check elsewhere if (status.operational && active.stored && match.allStored()) { @@ -255,6 +254,7 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di return outStatus } + @Deprecated("obsolete machinery, superseded by MPSCR-65") private fun dropDiscardingMatchesFor(ancestor: MatchJournal.OccChunk, droppedRuleTags: MutableSet) = this.dropDescendantsWhile(ancestor) { chunk -> if (chunk is MatchJournal.MatchChunk && chunk.match.discards(ancestor.occ)) { @@ -283,15 +283,30 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di } } .also { trace.trigger(match) } - .also { - accept(controller, match) - } - .then { - controller.processBody(match, parent, it) - } + .also { continueReplacedHeads(match, parent) } + .also { accept(controller, match) } + .then { controller.processBody(match, parent, it) } .also { trace.finish(match) } + private fun continueReplacedHeads(match: RuleMatchEx, parent: MatchJournal.MatchChunk) { + if (!isFront() && match.isPrincipal) { + profiler.profile("continueReplaced") { + + val invalidJustifications = match.matchHeadReplaced().filter { it.isPrincipal } + if (invalidJustifications.isNotEmpty()) { + + val pos = currentPos() + dropDescendants(invalidJustifications) { + val validOccs = invalidateChunk(it, invalidJustifications) + activationQueue.offerAll(pos, validOccs) + } + + } + } + } + } + private fun accept(controller: Controller, match: RuleMatchEx) { profiler.profile("logMatch") { @@ -327,6 +342,39 @@ internal class ConstraintsProcessing(private var dispatchingFront: Dispatcher.Di } } + + /** + * Incapsulates logic for deriving [Evidence] and [Justifications] for a new [Occurrence]. + */ + inner class JustifiedOccurrenceCreator { + val savedEvidence: Evidence = evidence() + val savedJustifications: Justifications = justifications() + + fun Constraint.occurrence( + observable: LogicalStateObservable, + arguments: List<*>, + logicalContext: LogicalContext, + ruleUniqueTag: Any? = null + ): Occurrence { + + // By default share justifications (as a small optimization) + var evidence = savedEvidence + var justifications = savedJustifications + + // For principal occurrences create new + if (ispec.isPrincipal(this)) { + evidence = nextEvidence() + justifications = justsCopy(savedJustifications).apply { add(evidence) } + } + + return Occurrence( + observable, this, logicalContext, arguments, + evidence, justifications, ruleUniqueTag + ) + } + } + + private fun MatchJournal.MatchChunk.dependsOnAny(utags: Iterable): Boolean = utags.contains(this.ruleUniqueTag) || utags.any { utag -> dependsOnRule(utag) } diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ContinuedActivationQueue.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ContinuedActivationQueue.kt index a44178bd..b7c9ef82 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ContinuedActivationQueue.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ContinuedActivationQueue.kt @@ -35,7 +35,9 @@ internal class ContinuedActivationQueue( } private fun ExecPos.assertValid() { - assert(continueFrom.chunk.justifiedBy(reactivated) || journalIndex.compare(continueFrom, reactivated.toPos()) >= 0) + val isAncestor = continueFrom.chunk.justifiedBy(reactivated) + val isPredecessor = journalIndex.compare(continueFrom, reactivated.toPos()) >= 0 + assert(isAncestor || isPredecessor) } diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ControllerImpl.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ControllerImpl.kt index af21fa5f..326b47cd 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ControllerImpl.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/ControllerImpl.kt @@ -80,7 +80,7 @@ internal class ControllerImpl ( // FIXME noLogicalContext val context = Context(NORMAL(), noLogicalContext, null, trace) - activateConstraint(constraint, processing.initialChunk(), processing.evidence(), processing.justifications(), context) + activateConstraint(constraint, processing.initialChunk(), processing.JustifiedOccurrenceCreator(), context) return context.currentStatus() } @@ -166,14 +166,13 @@ internal class ControllerImpl ( // fixme: fails in lambdacalc because of reactivated occurrences // (parents ain't tracked correctly in this case) // assert(newParent === processing.parentChunk()) + // todo: remove tracking parent in Controller once above issue is fixed - val currentJustifications = processing.justifications() - val currentEvidence = processing.evidence() + val occCreator = processing.JustifiedOccurrenceCreator() for (item in body) { val itemOk = when (item) { - // Occurrence just inherits evidence and justifications of its activating rule match - is Constraint -> activateConstraint(item, newParent, currentEvidence, currentJustifications, context) + is Constraint -> activateConstraint(item, newParent, occCreator, context) is Predicate -> tellPredicate(item, context) else -> throw IllegalArgumentException("unknown item ${item}") } @@ -229,15 +228,17 @@ internal class ControllerImpl ( return context.currentStatus() } - private fun activateConstraint(constraint: Constraint, parent: MatchJournal.MatchChunk, evidence: Evidence, justifications: Justifications, context: Context) : Boolean { + private fun activateConstraint(constraint: Constraint, parent: MatchJournal.MatchChunk, creator: ConstraintsProcessing.JustifiedOccurrenceCreator, context: Context) : Boolean { val args = supervisor.instantiateArguments(constraint.arguments(), context.logicalContext, context) return context.eval { status -> profiler.profile("activate_${constraint.symbol()}") { - constraint.occurrence(logicalStateObservable(), args, evidence, justifications, context.logicalContext, context.ruleUniqueTag).let { occ -> - trace.activate(occ) - processing.processActivated(this, occ, parent, status) + with(creator) { + constraint.occurrence(logicalStateObservable(), args, context.logicalContext, context.ruleUniqueTag).let { occ -> + trace.activate(occ) + processing.processActivated(this@ControllerImpl, occ, parent, status) + } } } diff --git a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/MatchJournal.kt b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/MatchJournal.kt index 1c570ed7..bdd054fb 100644 --- a/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/MatchJournal.kt +++ b/reactor/Core/src/jetbrains/mps/logic/reactor/core/internal/MatchJournal.kt @@ -82,8 +82,16 @@ interface MatchJournal : MutableIterable, EvidenceSource { * Transitively removes descendants of removed chunks. * Only erases future chunks and leaves journal [currentPos] intact. */ + @Deprecated("obsolete machinery, superseded by [dropDescendants] & MPSCR-65") fun dropDescendantsWhile(ancestor: Chunk, dropIf: (Chunk) -> Boolean) + /** + * Removes [Chunk]s dependent on any of [invalidated], + * applying [forEachDropped] for each removed [Chunk]. + * Only erases future chunks, leaving journal position [currentPos] intact. + */ + fun dropDescendants(invalidated: Collection, forEachDropped: (Chunk) -> Unit) + /** * Replay activated and discarded occurrences logged in journal between current * and provided positions. Advances journal position to specified position. @@ -131,6 +139,11 @@ interface MatchJournal : MutableIterable, EvidenceSource { * Length of the indexed [MatchJournal] */ val size: Int + + // some context functions + infix fun Pos.before(other: Pos): Boolean = compare(this, other) <= 0 + + infix fun Pos.after(other: Pos): Boolean = compare(this, other) >= 0 } /** @@ -243,3 +256,11 @@ private fun Iterable.allOccurrences(): List, forEachDropped: (Chunk) -> Unit) { + if (invalidated.isEmpty()) return + + val start = current + while (posPtr.hasNext()) { + current = posPtr.next() + if (current.justifiedByAny(invalidated)) { + // no need to 'resetOccurrences' because journal position is left intact + posPtr.remove() + forEachDropped(current) + } + } + + // rollback to the start + while (current !== start) { + current = posPtr.previous() + } + // make ptr point right after 'current' in case we changed anything + if (posPtr.hasNext()) posPtr.next() + } + private fun resetOccurrences(occSpecs: List) = // assume occSpecs are ordered in order of processing // so, iterate over reversed list @@ -434,13 +455,6 @@ internal open class MatchJournalImpl( } } -// NB: returns same collection of justifications, not copy -fun MatchJournal.justifications() = this.currentPos().chunk.justifications() -fun MatchJournal.evidence() = this.currentPos().chunk.evidence -// todo: this should be more correct -//fun MatchJournal.justifications() = this.parentChunk().justifications() -//fun MatchJournal.evidence() = this.parentChunk().evidence - // returns new collection of justifications fun RuleMatch.collectJustifications(vararg withEvidence: Evidence): Justifications = justsOf(*withEvidence).also { allJss ->