diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt index 29f55d2bdb..3abddfbfaf 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt @@ -37,14 +37,12 @@ import hu.bme.mit.theta.core.stmt.Stmts import hu.bme.mit.theta.core.type.booltype.BoolExprs.True import hu.bme.mit.theta.core.utils.TypeUtils import hu.bme.mit.theta.solver.Solver +import hu.bme.mit.theta.xcfa.* import hu.bme.mit.theta.xcfa.analysis.XcfaProcessState.Companion.createLookup import hu.bme.mit.theta.xcfa.analysis.coi.ConeOfInfluence -import hu.bme.mit.theta.xcfa.getFlatLabels -import hu.bme.mit.theta.xcfa.getGlobalVars import hu.bme.mit.theta.xcfa.isWritten import hu.bme.mit.theta.xcfa.model.* import hu.bme.mit.theta.xcfa.passes.changeVars -import hu.bme.mit.theta.xcfa.startsAtomic import java.util.* import java.util.function.Predicate @@ -153,15 +151,16 @@ fun getXcfaErrorPredicate( if (process1.key != process2.key) for (edge1 in process1.value.locs.peek().outgoingEdges) for (edge2 in process2.value.locs.peek().outgoingEdges) { - val globalVars1 = edge1.getGlobalVars(xcfa) - val globalVars2 = edge2.getGlobalVars(xcfa) - val isAtomic1 = edge1.startsAtomic() - val isAtomic2 = edge2.startsAtomic() - if (!isAtomic1 || !isAtomic2) { - val intersection = globalVars1.keys intersect globalVars2.keys - if (intersection.any { globalVars1[it].isWritten || globalVars2[it].isWritten }) - return@Predicate true - } + val mutexes1 = s.mutexes.filterValues { it == process1.key }.keys + val mutexes2 = s.mutexes.filterValues { it == process2.key }.keys + val globalVars1 = edge1.getGlobalVarsWithNeededMutexes(xcfa, mutexes1) + val globalVars2 = edge2.getGlobalVarsWithNeededMutexes(xcfa, mutexes2) + for (v1 in globalVars1) + for (v2 in globalVars2) + if (v1.varDecl == v2.varDecl) + if (v1.access.isWritten || v2.access.isWritten) + if ((v1.mutexes intersect v2.mutexes).isEmpty()) + return@Predicate true } false } diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoi.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoi.kt index 820856d87a..6b3238eca4 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoi.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoi.kt @@ -104,7 +104,7 @@ abstract class XcfaCoi(protected val xcfa: XCFA) { protected fun findDirectObservers(edge: XcfaEdge, prec: Prec) { val precVars = prec.usedVars - val writtenVars = edge.getVars().filter { it.value.isWritten && it.key in precVars } + val writtenVars = edge.collectVarsWithAccessType().filter { it.value.isWritten && it.key in precVars } if (writtenVars.isEmpty()) return val toVisit = mutableListOf(edge) @@ -121,7 +121,7 @@ abstract class XcfaCoi(protected val xcfa: XCFA) { source: XcfaEdge, target: XcfaEdge, observableVars: Map, AccessType>, precVars: Collection>, relation: MutableMap> ) { - val vars = target.getVars() + val vars = target.collectVarsWithAccessType() var relevantAction = vars.any { it.value.isWritten && it.key in precVars } if (!relevantAction) { val assumeVars = target.label.collectAssumesVars() diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiMultiThread.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiMultiThread.kt index 4e32bce98d..7774dafb16 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiMultiThread.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiMultiThread.kt @@ -19,7 +19,7 @@ package hu.bme.mit.theta.xcfa.analysis.coi import hu.bme.mit.theta.analysis.LTS import hu.bme.mit.theta.analysis.Prec import hu.bme.mit.theta.xcfa.getFlatLabels -import hu.bme.mit.theta.xcfa.getVars +import hu.bme.mit.theta.xcfa.collectVarsWithAccessType import hu.bme.mit.theta.xcfa.isWritten import hu.bme.mit.theta.xcfa.model.StartLabel import hu.bme.mit.theta.xcfa.model.XCFA @@ -141,7 +141,7 @@ class XcfaCoiMultiThread(xcfa: XCFA) : XcfaCoi(xcfa) { private fun findInterProcessObservers(edge: XcfaEdge, prec: Prec) { val precVars = prec.usedVars - val writtenVars = edge.getVars().filter { it.value.isWritten && it.key in precVars } + val writtenVars = edge.collectVarsWithAccessType().filter { it.value.isWritten && it.key in precVars } if (writtenVars.isEmpty()) return xcfa.procedures.forEach { procedure -> diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaDporLts.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaDporLts.kt index 6a60b9a5ae..88be0f44ed 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaDporLts.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaDporLts.kt @@ -25,7 +25,7 @@ import hu.bme.mit.theta.analysis.waitlist.Waitlist import hu.bme.mit.theta.xcfa.analysis.XcfaAction import hu.bme.mit.theta.xcfa.analysis.XcfaState import hu.bme.mit.theta.xcfa.analysis.getXcfaLts -import hu.bme.mit.theta.xcfa.getGlobalVars +import hu.bme.mit.theta.xcfa.collectIndirectGlobalVarAccesses import hu.bme.mit.theta.xcfa.isWritten import hu.bme.mit.theta.xcfa.model.XCFA import java.util.* @@ -456,8 +456,8 @@ open class XcfaDporLts(private val xcfa: XCFA) : LTS { protected open fun dependent(a: A, b: A): Boolean { if (a.pid == b.pid) return true - val aGlobalVars = a.edge.getGlobalVars(xcfa) - val bGlobalVars = b.edge.getGlobalVars(xcfa) + val aGlobalVars = a.edge.collectIndirectGlobalVarAccesses(xcfa) + val bGlobalVars = b.edge.collectIndirectGlobalVarAccesses(xcfa) // dependent if they access the same variable (at least one write) return (aGlobalVars.keys intersect bGlobalVars.keys).any { aGlobalVars[it].isWritten || bGlobalVars[it].isWritten } } @@ -488,8 +488,8 @@ class XcfaAadporLts(private val xcfa: XCFA) : XcfaDporLts(xcfa) { if (a.pid == b.pid) return true val precVars = prec?.usedVars?.toSet() ?: return super.dependent(a, b) - val aGlobalVars = a.edge.getGlobalVars(xcfa) - val bGlobalVars = b.edge.getGlobalVars(xcfa) + val aGlobalVars = a.edge.collectIndirectGlobalVarAccesses(xcfa) + val bGlobalVars = b.edge.collectIndirectGlobalVarAccesses(xcfa) // dependent if they access the same variable in the precision (at least one write) return (aGlobalVars.keys intersect bGlobalVars.keys intersect precVars).any { aGlobalVars[it].isWritten || bGlobalVars[it].isWritten } } 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 b384f1bc25..c2dac34f9e 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 @@ -19,13 +19,10 @@ 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 +import hu.bme.mit.theta.xcfa.* import hu.bme.mit.theta.xcfa.analysis.XcfaAction import hu.bme.mit.theta.xcfa.analysis.XcfaState import hu.bme.mit.theta.xcfa.analysis.getXcfaLts -import hu.bme.mit.theta.xcfa.collectVars -import hu.bme.mit.theta.xcfa.getFlatLabels -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 @@ -78,7 +75,7 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS, XcfaAction> */ override fun getEnabledActionsFor(state: XcfaState<*>): Set { // Collecting enabled actions - val allEnabledActions = getAllEnabledActionsFor(state) + val allEnabledActions = simpleXcfaLts.getEnabledActionsFor(state) // Calculating the source set starting from every (or some of the) enabled transition; the minimal source set is stored var minimalSourceSet = setOf() @@ -92,15 +89,6 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS, XcfaAction> return minimalSourceSet } - /** - * 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) - /** * Returns the possible starting actions of a source set. * @@ -230,21 +218,11 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS, XcfaAction> */ private fun getUsedSharedObjects(edge: XcfaEdge): Set> { val flatLabels = edge.getFlatLabels() - return if (flatLabels.any(XcfaLabel::isAtomicBegin)) { - getSharedObjectsWithBFS(edge) { it.getFlatLabels().none(XcfaLabel::isAtomicEnd) }.toSet() + val mutexes = flatLabels.filterIsInstance().flatMap { it.acquiredMutexes }.toMutableSet() + return if (mutexes.isEmpty()) { + getDirectlyUsedSharedObjects(edge) } else { - val lock = flatLabels.firstOrNull { - it is FenceLabel && it.labels.any { l -> l.startsWith("mutex_lock") } - } as FenceLabel? - if (lock != null) { - val mutex = lock.labels.first { l -> l.startsWith("mutex_lock") } - .substringAfter('(').substringBefore(')') - getSharedObjectsWithBFS(edge) { - it.getFlatLabels().none { fl -> fl is FenceLabel && "mutex_unlock(${mutex})" in fl.labels } - }.toSet() - } else { - getDirectlyUsedSharedObjects(edge) - } + getSharedObjectsWithBFS(edge) { it.mutexOperations(mutexes) }.toSet() } } @@ -287,21 +265,21 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS, XcfaAction> 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() + val exploredEdges = mutableListOf() + val edgesToExplore = mutableListOf() + edgesToExplore.add(startTransition) + while (edgesToExplore.isNotEmpty()) { + val exploring = edgesToExplore.removeFirst() vars.addAll(getDirectlyUsedSharedObjects(exploring)) if (goFurther.test(exploring)) { - val successiveTransitions = getSuccessiveTransitions(exploring) - for (newTransition in successiveTransitions) { - if (newTransition !in exploredTransitions) { - transitionsToExplore.add(newTransition) + val successiveEdges = getSuccessiveTransitions(exploring) + for (newEdge in successiveEdges) { + if (newEdge !in exploredEdges) { + edgesToExplore.add(newEdge) } } } - exploredTransitions.add(exploring) + exploredEdges.add(exploring) } return vars } @@ -325,8 +303,7 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS, XcfaAction> 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) + outgoingEdges.addAll(xcfa.procedures.first { it.name == startThread.name }.initLoc.outgoingEdges) } } return outgoingEdges diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt index bda578ef56..799d6bfd1b 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt @@ -16,7 +16,6 @@ package hu.bme.mit.theta.xcfa -import com.google.common.collect.Sets import hu.bme.mit.theta.common.dsl.Env import hu.bme.mit.theta.common.dsl.Symbol import hu.bme.mit.theta.common.dsl.SymbolTable @@ -29,13 +28,28 @@ import hu.bme.mit.theta.core.type.booltype.BoolType import hu.bme.mit.theta.core.utils.ExprUtils import hu.bme.mit.theta.core.utils.StmtUtils import hu.bme.mit.theta.xcfa.model.* +import java.util.function.Predicate -fun XCFA.collectVars(): Iterable> = vars.map { it.wrappedVar } - .union(procedures.map { it.vars }.flatten()) +/** + * Get flattened label list (without sequence labels). + */ +fun XcfaEdge.getFlatLabels(): List = label.getFlatLabels() + +fun XcfaLabel.getFlatLabels(): List = when (this) { + is SequenceLabel -> { + val ret = mutableListOf() + labels.forEach { ret.addAll(it.getFlatLabels()) } + ret + } -fun XCFA.collectAssumes(): Iterable> = procedures.map { - it.edges.map { it.label.collectAssumes() }.flatten() + else -> listOf(this) +} + +fun XCFA.collectVars(): Iterable> = vars.map { it.wrappedVar } union procedures.map { it.vars }.flatten() + +fun XCFA.collectAssumes(): Iterable> = procedures.map { procedure -> + procedure.edges.map { it.label.collectAssumes() }.flatten() }.flatten() fun XcfaLabel.collectAssumes(): Iterable> = when (this) { @@ -75,14 +89,15 @@ fun XcfaLabel.collectVars(): Iterable> = when (this) { is InvokeLabel -> params.map { ExprUtils.getVars(it) }.flatten() is JoinLabel -> setOf(pidVar) is ReadLabel -> setOf(global, local) - is StartLabel -> Sets.union(params.map { ExprUtils.getVars(it) }.flatten().toSet(), - setOf(pidVar)) - + is StartLabel -> params.map { ExprUtils.getVars(it) }.flatten().toSet() union setOf(pidVar) is WriteLabel -> setOf(global, local) else -> emptySet() } +// Complex var access requests + typealias AccessType = Pair +private typealias VarAccessMap = Map, AccessType> val AccessType?.isRead get() = this?.first == true val AccessType?.isWritten get() = this?.second == true @@ -92,12 +107,41 @@ fun AccessType?.merge(other: AccessType?) = val WRITE: AccessType get() = Pair(false, true) val READ: AccessType get() = Pair(true, false) -private typealias VarAccessMap = Map, AccessType> - private fun List.mergeAndCollect(): VarAccessMap = this.fold(mapOf()) { acc, next -> (acc.keys + next.keys).associateWith { acc[it].merge(next[it]) } } +/** + * The list of mutexes acquired by the label. + */ +inline val FenceLabel.acquiredMutexes: Set + get() = labels.mapNotNull { + when { + it == "ATOMIC_BEGIN" -> "___atomic_block_mutex___" + it.startsWith("mutex_lock") -> it.substringAfter('(').substringBefore(')') + it.startsWith("cond_wait") -> it.substring("cond_wait".length + 1, it.length - 1).split(",")[1] + else -> null + } + }.toSet() + +/** + * The list of mutexes released by the label. + */ +inline val FenceLabel.releasedMutexes: Set + get() = labels.mapNotNull { + when { + it == "ATOMIC_END" -> "___atomic_block_mutex___" + it.startsWith("mutex_unlock") -> it.substringAfter('(').substringBefore(')') + it.startsWith("start_cond_wait") -> it.substring("start_cond_wait".length + 1, it.length - 1).split(",")[1] + else -> null + } + }.toSet() + +/** + * Returns the list of accessed variables by the edge associated with an AccessType object. + */ +fun XcfaEdge.collectVarsWithAccessType(): VarAccessMap = label.collectVarsWithAccessType() + /** * Returns the list of accessed variables by the label. * The variable is associated with an AccessType object based on whether the variable is read/written by the label. @@ -106,27 +150,17 @@ fun XcfaLabel.collectVarsWithAccessType(): VarAccessMap = when (this) { is StmtLabel -> { when (stmt) { is HavocStmt<*> -> mapOf(stmt.varDecl to WRITE) - is AssignStmt<*> -> StmtUtils.getVars(stmt).associateWith { READ } + mapOf( - stmt.varDecl to WRITE) - + is AssignStmt<*> -> StmtUtils.getVars(stmt).associateWith { READ } + mapOf(stmt.varDecl to WRITE) else -> StmtUtils.getVars(stmt).associateWith { READ } } } - is NondetLabel -> { - labels.map { it.collectVarsWithAccessType() }.mergeAndCollect() - } - - is SequenceLabel -> { - labels.map { it.collectVarsWithAccessType() }.mergeAndCollect() - } - + is NondetLabel -> labels.map { it.collectVarsWithAccessType() }.mergeAndCollect() + is SequenceLabel -> labels.map { it.collectVarsWithAccessType() }.mergeAndCollect() is InvokeLabel -> params.map { ExprUtils.getVars(it) }.flatten().associateWith { READ } is JoinLabel -> mapOf(pidVar to READ) is ReadLabel -> mapOf(global to READ, local to READ) - is StartLabel -> params.map { ExprUtils.getVars(it) }.flatten().associateWith { READ } + mapOf( - pidVar to READ) - + is StartLabel -> params.map { ExprUtils.getVars(it) }.flatten().associateWith { READ } + mapOf(pidVar to READ) is WriteLabel -> mapOf(global to WRITE, local to WRITE) else -> emptyMap() } @@ -134,56 +168,108 @@ fun XcfaLabel.collectVarsWithAccessType(): VarAccessMap = when (this) { /** * Returns the global variables accessed by the label (the variables present in the given argument). */ -private fun XcfaLabel.collectGlobalVars(globalVars: Set>) = +private fun XcfaLabel.collectGlobalVars(globalVars: Set>): VarAccessMap = collectVarsWithAccessType().filter { labelVar -> globalVars.any { it == labelVar.key } } -inline val XcfaLabel.isAtomicBegin - get() = this is FenceLabel && this.labels.contains("ATOMIC_BEGIN") -inline val XcfaLabel.isAtomicEnd get() = this is FenceLabel && this.labels.contains("ATOMIC_END") - /** * Returns the global variables (potentially indirectly) accessed by the edge. - * If the edge starts an atomic block, all variable accesses in the atomic block is returned. + * If the edge starts an atomic block, all variable accesses in the atomic block are returned. * Variables are associated with a pair of boolean values: the first is true if the variable is read and false otherwise. The second is similar for write access. */ -fun XcfaEdge.getGlobalVars(xcfa: XCFA): Map, AccessType> { +fun XcfaEdge.collectIndirectGlobalVarAccesses(xcfa: XCFA): VarAccessMap { val globalVars = xcfa.vars.map(XcfaGlobalVar::wrappedVar).toSet() - var label = this.label - if (label is SequenceLabel && label.labels.size == 1) label = label.labels[0] - if (label.isAtomicBegin || (label is SequenceLabel && label.labels.any { it.isAtomicBegin } && label.labels.none { it.isAtomicEnd })) { - val vars = mutableMapOf, AccessType>() - val processed = mutableSetOf() - val unprocessed = mutableListOf(this) - while (unprocessed.isNotEmpty()) { - val e = unprocessed.removeFirst() - var eLabel = e.label - if (eLabel is SequenceLabel && eLabel.labels.size == 1) eLabel = eLabel.labels[0] - eLabel.collectGlobalVars(globalVars).forEach { (varDecl, accessType) -> - vars[varDecl] = accessType.merge(vars[varDecl]) - } - processed.add(e) - if (!(eLabel.isAtomicEnd || (eLabel is SequenceLabel && eLabel.labels.any { it.isAtomicEnd }))) { - unprocessed.addAll(e.target.outgoingEdges subtract processed) - } - } - return vars + val flatLabels = getFlatLabels() + val mutexes = flatLabels.filterIsInstance().flatMap { it.acquiredMutexes }.toMutableSet() + return if (mutexes.isEmpty()) { + label.collectGlobalVars(globalVars) } else { - return label.collectGlobalVars(globalVars) + collectGlobalVarsWithTraversal(globalVars) { it.mutexOperations(mutexes) } } } /** - * Returns the list of accessed variables by the edge associated with an AccessType object. + * Represents a global variable access: stores the variable declaration, the access type (read/write) and the set of + * mutexes that are needed to perform the variable access. */ -fun XcfaEdge.getVars(): Map, AccessType> = label.collectVarsWithAccessType() +class GlobalVarAccessWithMutexes(val varDecl: VarDecl<*>, val access: AccessType, val mutexes: Set) /** - * Returns true if the edge starts an atomic block. + * Returns the global variable accesses of the edge. + * + * @param xcfa the XCFA that contains the edge + * @param currentMutexes the set of mutexes currently acquired by the process of the edge + * @return the list of global variable accesses (c.f., [GlobalVarAccessWithMutexes]) */ -fun XcfaEdge.startsAtomic(): Boolean { - var label = this.label - if (label is SequenceLabel && label.labels.size == 1) label = label.labels[0] - return label is FenceLabel && label.labels.contains("ATOMIC_BEGIN") +fun XcfaEdge.getGlobalVarsWithNeededMutexes(xcfa: XCFA, currentMutexes: Set): List { + val globalVars = xcfa.vars.map(XcfaGlobalVar::wrappedVar).toSet() + val neededMutexes = currentMutexes.toMutableSet() + val accesses = mutableListOf() + getFlatLabels().forEach { label -> + if (label is FenceLabel) { + neededMutexes.addAll(label.acquiredMutexes) + } else { + val vars = label.collectGlobalVars(globalVars) + accesses.addAll(vars.mapNotNull { (varDecl, accessType) -> + if (accesses.any { it.varDecl == varDecl && (it.access == accessType && it.access == WRITE) }) { + null + } else { + GlobalVarAccessWithMutexes(varDecl, accessType, neededMutexes.toSet()) + } + }) + } + } + return accesses +} + +/** + * Returns global variables encountered in a search starting from the edge. + * + * @param goFurther the predicate that tells whether more edges have to be explored through an edge + * @return the set of encountered shared objects + */ +private fun XcfaEdge.collectGlobalVarsWithTraversal(globalVars: Set>, goFurther: Predicate) + : VarAccessMap { + val vars = mutableMapOf, AccessType>() + val exploredEdges = mutableListOf() + val edgesToExplore = mutableListOf() + edgesToExplore.add(this) + while (edgesToExplore.isNotEmpty()) { + val exploring = edgesToExplore.removeFirst() + exploring.label.collectGlobalVars(globalVars).forEach { (varDecl, access) -> + vars[varDecl] = vars[varDecl].merge(access) + } + if (goFurther.test(exploring)) { + for (newEdge in exploring.target.outgoingEdges) { + if (newEdge !in exploredEdges) { + edgesToExplore.add(newEdge) + } + } + } + exploredEdges.add(exploring) + } + return vars +} + +/** + * Follows the mutex operations of the given edge and updates the given set of mutexes. + * + * @param mutexes the set of mutexes currently acquired + * @return true if the set of mutexes is non-empty after the mutex operations + */ +fun XcfaEdge.mutexOperations(mutexes: MutableSet): Boolean { + val edgeFlatLabels = getFlatLabels() + val acquiredLocks = mutableSetOf() + val releasedLocks = mutableSetOf() + edgeFlatLabels.filterIsInstance().forEach { fence -> + releasedLocks.addAll(fence.releasedMutexes) + acquiredLocks.removeAll(fence.releasedMutexes) + + acquiredLocks.addAll(fence.acquiredMutexes) + releasedLocks.removeAll(fence.acquiredMutexes) + } + mutexes.removeAll(releasedLocks) + mutexes.addAll(acquiredLocks) + return mutexes.isNotEmpty() } fun XCFA.getSymbols(): Pair { @@ -199,25 +285,6 @@ fun XCFA.getSymbols(): Pair { return Pair(scope, env) } -private val atomicBlockInnerLocationsCache: HashMap> = HashMap() - -/** - * Returns XCFA locations that are inner locations of any atomic block (after an edge with an AtomicBegin and before - * an edge with an AtomicEnd). - * - * @param xcfaProcedure the atomic block inner locations of this XCFA procedure will be returned - * @return the list of locations in an atomic block - */ -fun getAtomicBlockInnerLocations(xcfaProcedure: XcfaProcedure): List? { - if (atomicBlockInnerLocationsCache.containsKey(xcfaProcedure)) { - return atomicBlockInnerLocationsCache[xcfaProcedure] - } - val atomicBlockInnerLocations: List = getAtomicBlockInnerLocations( - xcfaProcedure.initLoc) - atomicBlockInnerLocationsCache[xcfaProcedure] = atomicBlockInnerLocations - return atomicBlockInnerLocations -} - /** * Returns XCFA locations that are inner locations of any atomic block (after an edge with an AtomicBegin and before * an edge with an AtomicEnd). @@ -225,55 +292,32 @@ fun getAtomicBlockInnerLocations(xcfaProcedure: XcfaProcedure): List { - return getAtomicBlockInnerLocations(builder.initLoc) -} - -/** - * Get flattened label list (without sequence labels). - */ -fun XcfaEdge.getFlatLabels(): List = label.getFlatLabels() - -fun XcfaLabel.getFlatLabels(): List = when (this) { - is SequenceLabel -> { - val ret = ArrayList() - labels.forEach { ret.addAll(it.getFlatLabels()) } - ret - } - - else -> listOf(this) -} - +fun getAtomicBlockInnerLocations(builder: XcfaProcedureBuilder): List = + getAtomicBlockInnerLocations(builder.initLoc) private fun getAtomicBlockInnerLocations(initialLocation: XcfaLocation): List { - val atomicLocations: MutableList = ArrayList() - val visitedLocations: MutableList = ArrayList() - val locationsToVisit: MutableList = ArrayList() - val isAtomic: HashMap = HashMap() - locationsToVisit.add(initialLocation) - isAtomic[initialLocation] = false - while (!locationsToVisit.isEmpty()) { + val atomicLocations = mutableListOf() + val visitedLocations = mutableListOf() + val locationsToVisit = mutableListOf(initialLocation) + val isAtomic = mutableMapOf(initialLocation to false) + while (locationsToVisit.isNotEmpty()) { val visiting = locationsToVisit.removeAt(0) if (checkNotNull(isAtomic[visiting])) atomicLocations.add(visiting) visitedLocations.add(visiting) for (outEdge in visiting.outgoingEdges) { var isNextAtomic = checkNotNull(isAtomic[visiting]) - if (outEdge.getFlatLabels().stream().anyMatch { label -> - label is FenceLabel && label.labels.contains("ATOMIC_BEGIN") - }) { + if (outEdge.getFlatLabels().any { it is FenceLabel && it.labels.contains("ATOMIC_BEGIN") }) { isNextAtomic = true } - if (outEdge.getFlatLabels().stream().anyMatch { label -> - label is FenceLabel && label.labels.contains("ATOMIC_END") - }) { + if (outEdge.getFlatLabels().any { it is FenceLabel && it.labels.contains("ATOMIC_END") }) { isNextAtomic = false } val target = outEdge.target isAtomic[target] = isNextAtomic - if (atomicLocations.contains(target) && !isNextAtomic) { + if (target in atomicLocations && !isNextAtomic) { atomicLocations.remove(target) } - if (!locationsToVisit.contains(target) && !visitedLocations.contains(target)) { + if (target !in locationsToVisit && target !in visitedLocations) { locationsToVisit.add(outEdge.target) } } diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt index 4f7e8b8f68..64e5a66931 100644 --- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt +++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/LbePass.kt @@ -126,9 +126,6 @@ class LbePass(val parseContext: ParseContext) : ProcedurePass { return builder } - val isPostInlining: Boolean - get() = true - /** * Collapses atomic blocks sequentially. */ @@ -308,7 +305,10 @@ class LbePass(val parseContext: ParseContext) : ProcedurePass { private fun isNotLocal(edge: XcfaEdge): Boolean { return !edge.getFlatLabels().all { label -> !(label is StartLabel || label is JoinLabel) && label.collectVars().all(builder.getVars()::contains) && - !(label is StmtLabel && label.stmt is AssumeStmt && label.stmt.cond is FalseExpr) + !(label is StmtLabel && label.stmt is AssumeStmt && label.stmt.cond is FalseExpr) && + !(label is FenceLabel && label.labels.any { name -> + listOf("ATOMIC_BEGIN", "mutex_lock", "cond_wait").any { name.startsWith(it) } + }) } } } \ No newline at end of file