Skip to content

Commit

Permalink
spor cleanup + checkMutexBlocks checkNotNull fix
Browse files Browse the repository at this point in the history
  • Loading branch information
@csanadtelbisz
csanadtelbisz committed Oct 13, 2023
1 parent 9969165 commit 821d623
Show file tree
Hide file tree
Showing 2 changed files with 77 additions and 68 deletions.
68 changes: 32 additions & 36 deletions ...ects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,24 +31,23 @@ class XcfaAasporLts(xcfa: XCFA, private val ignoredVarRegistry: MutableMap<Decl<
// Collecting enabled actions
val allEnabledActions = getAllEnabledActionsFor(state)

// Calculating the persistent set starting from every (or some of the) enabled transition or from exploredActions if it is not empty
// The minimal persistent set is stored
var minimalPersistentSet = mutableSetOf<XcfaAction>()
val persistentSetFirstActions = if (exploredActions.isEmpty()) {
getPersistentSetFirstActions(state, allEnabledActions)
// Calculating the source set starting from every (or some of the) enabled transition or from exploredActions if it is not empty
// The minimal source set is stored
var minimalSourceSet = mutableSetOf<XcfaAction>()
val sourceSetFirstActions = if (exploredActions.isEmpty()) {
getSourceSetFirstActions(state, allEnabledActions)
} else {
setOf(exploredActions)
}
var finalIgnoredVars = setOf<Decl<out Type>>()

// Calculate persistent sets from all possible starting action set
for (firstActions in persistentSetFirstActions) {
// Variables that have been ignored (if they would be in the precision, more actions have had to be added to the persistent set)
// Calculate source sets from all possible starting action set
for (firstActions in sourceSetFirstActions) {
// Variables that have been ignored (if they would be in the precision, more actions have had to be added to the source set)
val ignoredVars = mutableSetOf<Decl<out Type>>()
val persistentSet = calculatePersistentSet(allEnabledActions, firstActions, prec,
ignoredVars)
if (minimalPersistentSet.isEmpty() || persistentSet.size < minimalPersistentSet.size) {
minimalPersistentSet = persistentSet.toMutableSet()
val sourceSet = calculateSourceSet(allEnabledActions, firstActions, prec, ignoredVars)
if (minimalSourceSet.isEmpty() || sourceSet.size < minimalSourceSet.size) {
minimalSourceSet = sourceSet.toMutableSet()
finalIgnoredVars = ignoredVars
}
}
Expand All @@ -58,28 +57,27 @@ class XcfaAasporLts(xcfa: XCFA, private val ignoredVarRegistry: MutableMap<Decl<
}
checkNotNull(ignoredVarRegistry[ignoredVar]).add(state)
}
minimalPersistentSet.removeAll(exploredActions.toSet())
return minimalPersistentSet
minimalSourceSet.removeAll(exploredActions.toSet())
return minimalSourceSet
}

/**
* Calculates a persistent set of enabled actions starting from a set of particular actions.
* Calculates a source set of enabled actions starting from a set of particular actions.
*
* @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
* @param firstActions the actions that will be added to the source set as the first actions
* @param prec the precision of the current abstraction
* @param ignoredVars variables that have been ignored (if they would be in the precision, more actions have had to be added to the persistent set)
* @return a persistent set of enabled actions in the current abstraction
* @param ignoredVars variables that have been ignored (if they would be in the precision, more actions have had to be added to the source set)
* @return a source set of enabled actions in the current abstraction
*/
private fun calculatePersistentSet(enabledActions: Collection<XcfaAction>,
firstActions: Collection<XcfaAction>, prec: Prec,
ignoredVars: MutableSet<Decl<out Type>>): Set<XcfaAction> {
private fun calculateSourceSet(enabledActions: Collection<XcfaAction>, firstActions: Collection<XcfaAction>,
prec: Prec, ignoredVars: MutableSet<Decl<out Type>>): Set<XcfaAction> {
if (firstActions.any(this::isBackwardAction)) {
return enabledActions.toSet()
}

val persistentSet = firstActions.toMutableSet()
val otherActions = enabledActions.toMutableSet() // actions not in the persistent set
val sourceSet = firstActions.toMutableSet()
val otherActions = enabledActions.toMutableSet() // actions not in the source set
firstActions.forEach(otherActions::remove)
val ignoredVarsByAction = otherActions.associateWith { mutableSetOf<Decl<out Type>>() }

Expand All @@ -88,38 +86,36 @@ class XcfaAasporLts(xcfa: XCFA, private val ignoredVarRegistry: MutableMap<Decl<
addedNewAction = false
val actionsToRemove = mutableSetOf<XcfaAction>()
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)
// for every action that is not in the source set it is checked whether it should be added to the source set
// (because it is dependent with an action already in the source set)
val potentialIgnoredVars = mutableSetOf<Decl<out Type>>()
if (persistentSet.any { persistentSetAction ->
areDependents(persistentSetAction, action, prec, potentialIgnoredVars)
}) {
if (sourceSet.any { areDependents(it, action, prec, potentialIgnoredVars) }) {
if (isBackwardAction(action)) {
return enabledActions.toSet() // see POR algorithm for the reason of removing backward transitions
}
persistentSet.add(action)
sourceSet.add(action)
actionsToRemove.add(action)
addedNewAction = true
} else {
checkNotNull(ignoredVarsByAction[action]).addAll(
potentialIgnoredVars) // the action is not added to the persistent set because we ignore variables in potentialIgnoredVars
// the action is not added to the source set because we ignore variables in potentialIgnoredVars
checkNotNull(ignoredVarsByAction[action]).addAll(potentialIgnoredVars)
}
}
actionsToRemove.forEach(otherActions::remove)
}
otherActions.forEach { action -> ignoredVars.addAll(checkNotNull(ignoredVarsByAction[action])) }
return persistentSet
return sourceSet
}

private fun areDependents(persistentSetAction: XcfaAction, action: XcfaAction, prec: Prec,
private fun areDependents(sourceSetAction: XcfaAction, action: XcfaAction, prec: Prec,
ignoredVariables: MutableSet<Decl<out Type?>>): Boolean {
if (isSameProcess(persistentSetAction, action)) {
if (isSameProcess(sourceSetAction, action)) {
return true
}
val usedByPersistentSetAction = getCachedUsedSharedObjects(getEdgeOf(persistentSetAction))
val usedBySourceSetAction = getCachedUsedSharedObjects(getEdgeOf(sourceSetAction))
val influencedSharedObjects = getInfluencedSharedObjects(getEdgeOf(action))
for (varDecl in influencedSharedObjects) {
if (usedByPersistentSetAction.contains(varDecl)) {
if (usedBySourceSetAction.contains(varDecl)) {
if (varDecl !in prec.usedVars) {
// the actions would be dependent, but we may have a chance to ignore it in the current abstraction
ignoredVariables.add(varDecl)
Expand Down
77 changes: 45 additions & 32 deletions ...ojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,9 @@ import kotlin.random.Random

/**
* LTS with a POR (Partial Order Reduction) algorithm applied as a filter when returning enabled actions.
* The algorithm is similar to the static source-set based POR algorithm described in the following paper:
* Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K. (2017):
* Comparing source sets and persistent sets for partial order reduction
*
* @param xcfa the XCFA of the verified program
*/
Expand Down Expand Up @@ -76,16 +79,16 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS<XcfaState<*>, XcfaAction>
// 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<XcfaAction>()
val persistentSetFirstActions = getPersistentSetFirstActions(state, allEnabledActions)
for (firstActions in persistentSetFirstActions) {
val persistentSet = calculatePersistentSet(allEnabledActions, firstActions)
if (minimalPersistentSet.isEmpty() || persistentSet.size < minimalPersistentSet.size) {
minimalPersistentSet = persistentSet
// Calculating the source set starting from every (or some of the) enabled transition; the minimal source set is stored
var minimalSourceSet = setOf<XcfaAction>()
val sourceSetFirstActions = getSourceSetFirstActions(state, allEnabledActions)
for (firstActions in sourceSetFirstActions) {
val sourceSet = calculateSourceSet(allEnabledActions, firstActions)
if (minimalSourceSet.isEmpty() || sourceSet.size < minimalSourceSet.size) {
minimalSourceSet = sourceSet
}
}
return minimalPersistentSet
return minimalSourceSet
}

/**
Expand All @@ -98,28 +101,38 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS<XcfaState<*>, XcfaAction>
simpleXcfaLts.getEnabledActionsFor(state)

/**
* Returns the possible starting actions of a persistent set.
* Returns the possible starting actions of a source set.
*
* @param allEnabledActions the enabled actions in the present state
* @return the possible starting actions of a persistent set
* @return the possible starting actions of a source set
*/
protected fun getPersistentSetFirstActions(state: XcfaState<*>,
protected fun getSourceSetFirstActions(state: XcfaState<*>,
allEnabledActions: Collection<XcfaAction>): Collection<Collection<XcfaAction>> {
val enabledActionsByProcess = allEnabledActions.groupBy(XcfaAction::pid)
val enabledProcesses = enabledActionsByProcess.keys.toList().shuffled(random)
return enabledProcesses.map { pid ->
val firstProcesses = mutableSetOf(pid)
checkMutexBlocks(state, pid, firstProcesses, enabledActionsByProcess)
firstProcesses.flatMap { checkNotNull(enabledActionsByProcess[it]) }
firstProcesses.flatMap { enabledActionsByProcess[it] ?: emptyList() }
}
}

/**
* Checks whether a process is blocked by a mutex and if it is, it adds the process that blocks it to the set of
* first processes.
*
* @param state the current state
* @param pid the process whose blocking is to be checked
* @param firstProcesses the set of first processes
* @param enabledActionsByProcess the enabled actions grouped by processes
* @return the set of first processes
*/
private fun checkMutexBlocks(state: XcfaState<*>, pid: Int, firstProcesses: MutableSet<Int>,
enabledActionsByProcess: Map<Int, List<XcfaAction>>) {
val processState = checkNotNull(state.processes[pid])
if (!processState.paramsInitialized) return
val disabledOutEdges = processState.locs.peek().outgoingEdges.filter { edge ->
checkNotNull(enabledActionsByProcess[pid]).none { action -> action.target == edge.target }
enabledActionsByProcess[pid]?.none { action -> action.target == edge.target } ?: true
}
disabledOutEdges.forEach { edge ->
edge.getFlatLabels().filterIsInstance<FenceLabel>().forEach { fence ->
Expand All @@ -137,52 +150,52 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS<XcfaState<*>, XcfaAction>
}

/**
* Calculates a persistent set of enabled actions starting from a particular action.
* Calculates a source 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
* @param firstActions the actions that will be added to the source set as the first actions
* @return a source set of enabled actions
*/
private fun calculatePersistentSet(enabledActions: Collection<XcfaAction>,
private fun calculateSourceSet(enabledActions: Collection<XcfaAction>,
firstActions: Collection<XcfaAction>): Set<XcfaAction> {
if (firstActions.any(::isBackwardAction)) {
return enabledActions.toSet()
}
val persistentSet = firstActions.toMutableSet()
val otherActions = (enabledActions.toMutableSet() subtract persistentSet).toMutableSet() // actions not in the persistent set
val sourceSet = firstActions.toMutableSet()
val otherActions = (enabledActions.toMutableSet() subtract sourceSet).toMutableSet() // actions not in the source set
var addedNewAction = true
while (addedNewAction) {
addedNewAction = false
val actionsToRemove = mutableSetOf<XcfaAction>()
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) }) {
// for every action that is not in the source set it is checked whether it should be added to the source set
// (because it is dependent with an action already in the source set)
if (sourceSet.any { areDependents(it, action) }) {
if (isBackwardAction(action)) {
return enabledActions.toSet() // see POR algorithm for the reason of removing backward transitions
}
persistentSet.add(action)
sourceSet.add(action)
actionsToRemove.add(action)
addedNewAction = true
}
}
actionsToRemove.forEach(otherActions::remove)
}
return persistentSet
return sourceSet
}

/**
* Determines whether an action is dependent with another one (based on the notions introduced for the POR
* algorithm) already in the persistent set.
* algorithm) already in the source 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
* @param sourceSetAction the action in the source set
* @param action the other action (not in the source set)
* @return true, if the two actions are dependent in the context of source 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 }
private fun areDependents(sourceSetAction: XcfaAction, action: XcfaAction): Boolean {
val usedBySourceSetAction = getCachedUsedSharedObjects(getEdgeOf(sourceSetAction))
return isSameProcess(sourceSetAction, action) ||
getInfluencedSharedObjects(getEdgeOf(action)).any { it in usedBySourceSetAction }
}

/**
Expand Down

0 comments on commit 821d623

Please sign in to comment.