diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SporLts.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SporLts.java deleted file mode 100644 index 21d4546cc7..0000000000 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/SporLts.java +++ /dev/null @@ -1,265 +0,0 @@ -/* - * Copyright 2023 Budapest University of Technology and Economics - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ - -package hu.bme.mit.theta.analysis.algorithm; - -import hu.bme.mit.theta.analysis.Action; -import hu.bme.mit.theta.analysis.LTS; -import hu.bme.mit.theta.analysis.State; -import hu.bme.mit.theta.core.decl.Decl; -import hu.bme.mit.theta.core.type.Type; - -import java.util.*; -import java.util.function.Predicate; - -/** - * LTS with a POR (Partial Order Reduction) algorithm applied as a filter when returning enabled actions. - * - * @param the type of the state - * @param the type of the action (transition in the state space) - * @param the type of the transition in the original formalism - */ -public abstract class SporLts implements LTS { - - /* CACHE COLLECTIONS */ - - /** - * Shared objects (~global variables) used by a transition. - */ - private final HashMap>> usedSharedObjects = new HashMap<>(); - - /** - * Shared objects (~global variables) that are used by the key transition or by transitions reachable from the - * current state via a given transition. - */ - private final HashMap>> influencedSharedObjects = new HashMap<>(); - - /** - * Backward transitions in the transition system (a transition of a loop). - */ - protected final Set backwardTransitions = new LinkedHashSet<>(); - - - /** - * Returns the enabled actions in the ARG from the given state filtered with a POR algorithm. - * - * @param state the state whose enabled actions we would like to know - * @return the enabled actions - */ - @Override - public Set getEnabledActionsFor(S state) { - // Collecting enabled actions - Collection allEnabledActions = getAllEnabledActionsFor(state); - - // Calculating the persistent set starting from every (or some of the) enabled transition; the minimal persistent set is stored - Set minimalPersistentSet = new LinkedHashSet<>(); - Collection> persistentSetFirstActions = getPersistentSetFirstActions(allEnabledActions); - for (Collection firstActions : persistentSetFirstActions) { - Set persistentSet = calculatePersistentSet(allEnabledActions, firstActions); - if (minimalPersistentSet.size() == 0 || persistentSet.size() < minimalPersistentSet.size()) { - minimalPersistentSet = persistentSet; - } - } - - return minimalPersistentSet; - } - - /** - * Calculates a persistent set of enabled actions starting from a particular action. - * - * @param enabledActions the enabled actions in the present state - * @param firstActions the actions that will be added to the persistent set as the first actions - * @return a persistent set of enabled actions - */ - protected Set calculatePersistentSet(Collection enabledActions, Collection firstActions) { - if (firstActions.stream().anyMatch(this::isBackwardAction)) { - return new LinkedHashSet<>(enabledActions); - } - - Set persistentSet = new LinkedHashSet<>(firstActions); - Set otherActions = new LinkedHashSet<>(enabledActions); // actions not in the persistent set - firstActions.forEach(otherActions::remove); - - boolean addedNewAction = true; - while (addedNewAction) { - addedNewAction = false; - Set actionsToRemove = new LinkedHashSet<>(); - for (A action : otherActions) { - // for every action that is not in the persistent set it is checked whether it should be added to the persistent set - // (because it is dependent with an action already in the persistent set) - if (persistentSet.stream().anyMatch(persistentSetAction -> areDependents(persistentSetAction, action))) { - if (isBackwardAction(action)) { - return new LinkedHashSet<>(enabledActions); // see POR algorithm for the reason of removing backward transitions - } - - persistentSet.add(action); - actionsToRemove.add(action); - addedNewAction = true; - } - } - actionsToRemove.forEach(otherActions::remove); - } - - return persistentSet; - } - - /** - * Returns all the enabled actions in a state. - * - * @param state the state whose enabled actions are to be returned - * @return the enabled actions in the state - */ - protected abstract Collection getAllEnabledActionsFor(S state); - - /** - * Returns the actions from where persistent sets will be calculated (a subset of the given enabled actions). - * The default implementation returns all enabled actions. - * - * @param allEnabledActions all the enabled actions in the present state - * @return the actions from where persistent sets will be calculated - */ - protected Collection> getPersistentSetFirstActions(Collection allEnabledActions) { - return List.of(allEnabledActions); - } - - /** - * Determines whether an action is dependent with another one (based on the notions introduced for the POR - * algorithm) already in the persistent set. - * - * @param persistentSetAction the action in the persistent set - * @param action the other action (not in the persistent set) - * @return true, if the two actions are dependent in the context of persistent sets - */ - protected boolean areDependents(A persistentSetAction, A action) { - var usedByPersistentSetAction = getCachedUsedSharedObjects(getTransitionOf(persistentSetAction)); - return isSameProcess(persistentSetAction, action) || - getInfluencedSharedObjects(getTransitionOf(action)).stream().anyMatch(usedByPersistentSetAction::contains); - } - - /** - * Determines whether two actions are in the same process. - * - * @param action1 action 1 - * @param action2 action 2 - * @return true, if the two actions are in the same process - */ - protected abstract boolean isSameProcess(A action1, A action2); - - /** - * Determines whether the given action is a backward action. - * - * @param action the action to be classified as backward action or non-backward action - * @return true, if the action is a backward action - */ - protected boolean isBackwardAction(A action) { - return backwardTransitions.contains(getTransitionOf(action)); - } - - /** - * Get the original transition of an action (from which the action has been created). - * - * @param action whose original transition is to be returned - * @return the original transition - */ - protected abstract T getTransitionOf(A action); - - /** - * Returns the successive transitions of a transition (transitions whose source is the target of the given - * parameter). - * - * @param transition whose successive transitions is to be returned - * @return the successive transitions of the transition given as the parameter - */ - protected abstract Set getSuccessiveTransitions(T transition); - - - /** - * Returns the shared objects (~global variables) that an action uses (it is present in one of its labels). - * - * @param transition whose shared objects are to be returned - * @return the set of used shared objects - */ - protected abstract Set> getDirectlyUsedSharedObjects(T transition); - - /** - * Returns the shared objects (~global variables) that an action uses. - * - * @param transition whose shared objects are to be returned - * @return the set of directly or indirectly used shared objects - */ - protected Set> getUsedSharedObjects(T transition) { - return getDirectlyUsedSharedObjects(transition); - } - - /** - * Same as {@link SporLts#getUsedSharedObjects(T transition)} with an additional cache layer. - * - * @param transition whose shared objects are to be returned - * @return the set of directly or indirectly used shared objects - */ - protected Set> getCachedUsedSharedObjects(T transition) { - if (!usedSharedObjects.containsKey(transition)) { - Set> vars = getUsedSharedObjects(transition); - usedSharedObjects.put(transition, vars); - } - return usedSharedObjects.get(transition); - } - - /** - * Returns the shared objects (~global variables) used by the given transition or by transitions that are reachable - * via the given transition ("influenced shared objects"). - * - * @param transition whose successor transitions' shared objects are to be returned. - * @return the set of influenced shared objects - */ - protected Set> getInfluencedSharedObjects(T transition) { - if (!influencedSharedObjects.containsKey(transition)) { - influencedSharedObjects.put(transition, getSharedObjectsWithBFS(transition, t -> true)); - } - return influencedSharedObjects.get(transition); - } - - /** - * Returns shared objects (~global variables) encountered in a search starting from a given transition. - * - * @param startTransition the start point (transition) of the search - * @param goFurther the predicate that tells whether more transitions have to be explored through this - * transition - * @return the set of encountered shared objects - */ - protected Set> getSharedObjectsWithBFS(T startTransition, Predicate goFurther) { - Set> vars = new LinkedHashSet<>(); - List exploredTransitions = new ArrayList<>(); - List transitionsToExplore = new ArrayList<>(); - transitionsToExplore.add(startTransition); - - while (!transitionsToExplore.isEmpty()) { - T exploring = transitionsToExplore.remove(0); - vars.addAll(getDirectlyUsedSharedObjects(exploring)); - - if (goFurther.test(exploring)) { - Set successiveTransitions = getSuccessiveTransitions(exploring); - for (var newTransition : successiveTransitions) { - if (!exploredTransitions.contains(newTransition)) { - transitionsToExplore.add(newTransition); - } - } - } - exploredTransitions.add(exploring); - } - return vars; - } -} diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt index f5ba5b18fc..64ed3d15e3 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt @@ -23,15 +23,11 @@ import hu.bme.mit.theta.xcfa.analysis.XcfaAction import hu.bme.mit.theta.xcfa.analysis.XcfaState import hu.bme.mit.theta.xcfa.model.XCFA -class XcfaAasporLts(xcfa: XCFA, - private val ignoredVarRegistry: MutableMap, MutableSet>) : +class XcfaAasporLts(xcfa: XCFA, private val ignoredVarRegistry: MutableMap, MutableSet>) : XcfaSporLts(xcfa) { - override fun

getEnabledActionsFor( - state: XcfaState<*>, - exploredActions: Collection, - prec: P - ): Set { + override fun

getEnabledActionsFor(state: XcfaState<*>, exploredActions: Collection, + prec: P): Set { // Collecting enabled actions val allEnabledActions = getAllEnabledActionsFor(state) @@ -121,8 +117,8 @@ class XcfaAasporLts(xcfa: XCFA, return true } val usedByPersistentSetAction = getCachedUsedSharedObjects( - getTransitionOf(persistentSetAction)) - val influencedSharedObjects = getInfluencedSharedObjects(getTransitionOf(action)) + getEdgeOf(persistentSetAction)) + val influencedSharedObjects = getInfluencedSharedObjects(getEdgeOf(action)) for (varDecl in influencedSharedObjects) { if (usedByPersistentSetAction.contains(varDecl)) { if (varDecl !in prec.usedVars) { diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt index cbaba22ba1..cf73181dc8 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt @@ -15,7 +15,7 @@ */ package hu.bme.mit.theta.xcfa.analysis.por -import hu.bme.mit.theta.analysis.algorithm.SporLts +import hu.bme.mit.theta.analysis.LTS import hu.bme.mit.theta.core.decl.Decl import hu.bme.mit.theta.core.decl.VarDecl import hu.bme.mit.theta.core.type.Type @@ -28,9 +28,15 @@ import hu.bme.mit.theta.xcfa.isAtomicBegin import hu.bme.mit.theta.xcfa.isAtomicEnd import hu.bme.mit.theta.xcfa.model.* import java.util.* +import java.util.function.Predicate import kotlin.random.Random -open class XcfaSporLts(protected val xcfa: XCFA) : SporLts, XcfaAction, XcfaEdge>() { +/** + * LTS with a POR (Partial Order Reduction) algorithm applied as a filter when returning enabled actions. + * + * @param xcfa the XCFA of the verified program + */ +open class XcfaSporLts(protected val xcfa: XCFA) : LTS, XcfaAction> { companion object { @@ -38,44 +44,137 @@ open class XcfaSporLts(protected val xcfa: XCFA) : SporLts, XcfaAct private val simpleXcfaLts = getXcfaLts() } + /* CACHE COLLECTIONS */ + + /** + * Shared objects (~global variables) used by a transition. + */ + private val usedSharedObjects: MutableMap>> = mutableMapOf() + + /** + * Shared objects (~global variables) that are used by the key transition or by transitions reachable from the + * current state via a given transition. + */ + private val influencedSharedObjects: MutableMap>> = mutableMapOf() + + /** + * Backward transitions in the transition system (a transition of a loop). + */ + private val backwardTransitions: MutableSet = mutableSetOf() + init { collectBackwardTransitions() } - override fun getAllEnabledActionsFor(state: XcfaState<*>): Collection = + /** + * Returns the enabled actions in the ARG from the given state filtered with a POR algorithm. + * + * @param state the state whose enabled actions we would like to know + * @return the enabled actions + */ + override fun getEnabledActionsFor(state: XcfaState<*>): Set { + // Collecting enabled actions + val allEnabledActions = getAllEnabledActionsFor(state) + + // Calculating the persistent set starting from every (or some of the) enabled transition; the minimal persistent set is stored + var minimalPersistentSet = setOf() + val persistentSetFirstActions = getPersistentSetFirstActions(allEnabledActions) + for (firstActions in persistentSetFirstActions) { + val persistentSet = calculatePersistentSet(allEnabledActions, firstActions) + if (minimalPersistentSet.isEmpty() || persistentSet.size < minimalPersistentSet.size) { + minimalPersistentSet = persistentSet + } + } + return minimalPersistentSet + } + + /** + * Returns all enabled actions in the given state. + * + * @param state the state whose enabled actions we would like to know + * @return the enabled actions + */ + protected fun getAllEnabledActionsFor(state: XcfaState<*>): Collection = simpleXcfaLts.getEnabledActionsFor(state) - override fun getPersistentSetFirstActions( + /** + * Returns the possible starting actions of a persistent set. + * + * @param allEnabledActions the enabled actions in the present state + * @return the possible starting actions of a persistent set + */ + protected fun getPersistentSetFirstActions( allEnabledActions: Collection): Collection> { val enabledActionsByProcess = allEnabledActions.groupBy(XcfaAction::pid) val enabledProcesses = enabledActionsByProcess.keys.toList().shuffled(random) return enabledProcesses.map { checkNotNull(enabledActionsByProcess[it]) } } - override fun isSameProcess(action1: XcfaAction, - action2: XcfaAction) = action1.pid == action2.pid - - override fun getTransitionOf(action: XcfaAction) = action.edge - - override fun getSuccessiveTransitions(edge: XcfaEdge): Set { - val outgoingEdges = edge.target.outgoingEdges.toMutableSet() - val startThreads = edge.getFlatLabels().filterIsInstance().toList() - if (startThreads.isNotEmpty()) { // for start thread labels, the thread procedure must be explored, too! - startThreads.forEach { startThread -> - outgoingEdges.addAll( - xcfa.procedures.first { it.name == startThread.name }.initLoc.outgoingEdges) + /** + * Calculates a persistent set of enabled actions starting from a particular action. + * + * @param enabledActions the enabled actions in the present state + * @param firstActions the actions that will be added to the persistent set as the first actions + * @return a persistent set of enabled actions + */ + private fun calculatePersistentSet(enabledActions: Collection, + firstActions: Collection): Set { + if (firstActions.any(::isBackwardAction)) { + return enabledActions.toSet() + } + val persistentSet = firstActions.toMutableSet() + val otherActions = (enabledActions.toMutableSet() subtract persistentSet).toMutableSet() // actions not in the persistent set + var addedNewAction = true + while (addedNewAction) { + addedNewAction = false + val actionsToRemove = mutableSetOf() + for (action in otherActions) { + // for every action that is not in the persistent set it is checked whether it should be added to the persistent set + // (because it is dependent with an action already in the persistent set) + if (persistentSet.any { persistentSetAction -> areDependents(persistentSetAction, action) }) { + if (isBackwardAction(action)) { + return enabledActions.toSet() // see POR algorithm for the reason of removing backward transitions + } + persistentSet.add(action) + actionsToRemove.add(action) + addedNewAction = true + } } + actionsToRemove.forEach(otherActions::remove) } - return outgoingEdges + return persistentSet } + /** + * Determines whether an action is dependent with another one (based on the notions introduced for the POR + * algorithm) already in the persistent set. + * + * @param persistentSetAction the action in the persistent set + * @param action the other action (not in the persistent set) + * @return true, if the two actions are dependent in the context of persistent sets + */ + private fun areDependents(persistentSetAction: XcfaAction, action: XcfaAction): Boolean { + val usedByPersistentSetAction = getCachedUsedSharedObjects(getEdgeOf(persistentSetAction)) + return isSameProcess(persistentSetAction, action) || + getInfluencedSharedObjects(getEdgeOf(action)).any { it in usedByPersistentSetAction } + } + + /** + * Determines whether two actions are in the same process. + * + * @param action1 the first action + * @param action2 the second action + * @return true, if the two actions are in the same process + */ + protected fun isSameProcess(action1: XcfaAction, action2: XcfaAction) = action1.pid == action2.pid + /** * Returns the global variables that an edge uses (it is present in one of its labels). * * @param edge whose global variables are to be returned * @return the set of used global variables */ - override fun getDirectlyUsedSharedObjects(edge: XcfaEdge): Set> { + private fun getDirectlyUsedSharedObjects(edge: XcfaEdge): Set> { val globalVars = xcfa.vars.map(XcfaGlobalVar::wrappedVar) return edge.getFlatLabels().flatMap { label -> label.collectVars().filter { it in globalVars } @@ -89,7 +188,7 @@ open class XcfaSporLts(protected val xcfa: XCFA) : SporLts, XcfaAct * @param edge whose global variables are to be returned * @return the set of directly or indirectly used global variables */ - override fun getUsedSharedObjects(edge: XcfaEdge): Set?> = + private fun getUsedSharedObjects(edge: XcfaEdge): Set> = if (edge.getFlatLabels().any(XcfaLabel::isAtomicBegin)) { getSharedObjectsWithBFS(edge) { it.getFlatLabels().none(XcfaLabel::isAtomicEnd) @@ -98,6 +197,98 @@ open class XcfaSporLts(protected val xcfa: XCFA) : SporLts, XcfaAct getDirectlyUsedSharedObjects(edge) } + /** + * Same as [getUsedSharedObjects] with an additional cache layer. + * + * @param edge whose shared objects are to be returned + * @return the set of directly or indirectly used shared objects + */ + protected fun getCachedUsedSharedObjects(edge: XcfaEdge): Set> { + if (!usedSharedObjects.containsKey(edge)) { + val vars = getUsedSharedObjects(edge) + usedSharedObjects[edge] = vars + } + return usedSharedObjects[edge]!! + } + + /** + * Returns the shared objects (~global variables) used by the given transition or by transitions that are reachable + * via the given transition ("influenced shared objects"). + * + * @param edge whose successor transitions' shared objects are to be returned. + * @return the set of influenced shared objects + */ + protected fun getInfluencedSharedObjects(edge: XcfaEdge): Set> { + if (!influencedSharedObjects.containsKey(edge)) { + influencedSharedObjects[edge] = getSharedObjectsWithBFS(edge) { true } + } + return influencedSharedObjects[edge]!! + } + + /** + * Returns shared objects (~global variables) encountered in a search starting from a given transition. + * + * @param startTransition the start point (transition) of the search + * @param goFurther the predicate that tells whether more transitions have to be explored through this + * transition + * @return the set of encountered shared objects + */ + private fun getSharedObjectsWithBFS(startTransition: XcfaEdge, + goFurther: Predicate): Set> { + val vars = mutableSetOf>() + val exploredTransitions = mutableListOf() + val transitionsToExplore = mutableListOf() + transitionsToExplore.add(startTransition) + while (transitionsToExplore.isNotEmpty()) { + val exploring = transitionsToExplore.removeFirst() + vars.addAll(getDirectlyUsedSharedObjects(exploring)) + if (goFurther.test(exploring)) { + val successiveTransitions = getSuccessiveTransitions(exploring) + for (newTransition in successiveTransitions) { + if (newTransition !in exploredTransitions) { + transitionsToExplore.add(newTransition) + } + } + } + exploredTransitions.add(exploring) + } + return vars + } + + /** + * Returns the xcfa edge of the given action. + * + * @param action the action whose edge is to be returned + * @return the edge of the action + */ + protected fun getEdgeOf(action: XcfaAction) = action.edge + + /** + * Returns the outgoing edges of the target of the given edge. + * + * @param edge the edge whose target's outgoing edges are to be returned + * @return the outgoing edges of the target of the edge + */ + private fun getSuccessiveTransitions(edge: XcfaEdge): Set { + val outgoingEdges = edge.target.outgoingEdges.toMutableSet() + val startThreads = edge.getFlatLabels().filterIsInstance().toList() + if (startThreads.isNotEmpty()) { // for start thread labels, the thread procedure must be explored, too! + startThreads.forEach { startThread -> + outgoingEdges.addAll( + xcfa.procedures.first { it.name == startThread.name }.initLoc.outgoingEdges) + } + } + return outgoingEdges + } + + /** + * Determines whether the given action is a backward action. + * + * @param action the action to be classified as backward action or non-backward action + * @return true, if the action is a backward action + */ + protected fun isBackwardAction(action: XcfaAction): Boolean = backwardTransitions.contains(getEdgeOf(action)) + /** * Collects backward edges of the given XCFA. */