mutex handling fixes

ftsrg · Nov 2, 2023 · 7fd3216 · 7fd3216
1 parent 5163050
commit 7fd3216
Show file tree

Hide file tree

Showing 7 changed files with 196 additions and 176 deletions.
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
@@ -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
@@ -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<VarDecl<*>, AccessType>,
         precVars: Collection<VarDecl<*>>, relation: MutableMap<XcfaEdge, MutableSet<XcfaEdge>>
     ) {
-        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/...xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/coi/XcfaCoiMultiThread.kt b/...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/...ojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaDporLts.kt b/...ojects/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<S, A> {
     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/...ojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaSporLts.kt b/...ojects/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<XcfaState<*>, XcfaAction>
      */
     override fun getEnabledActionsFor(state: XcfaState<*>): Set<XcfaAction> {
         // 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<XcfaAction>()
@@ -92,15 +89,6 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS<XcfaState<*>, 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<XcfaAction> =
-        simpleXcfaLts.getEnabledActionsFor(state)
-
     /**
      * Returns the possible starting actions of a source set.
      *
@@ -230,21 +218,11 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS<XcfaState<*>, XcfaAction>
      */
     private fun getUsedSharedObjects(edge: XcfaEdge): Set<Decl<out Type>> {
         val flatLabels = edge.getFlatLabels()
-        return if (flatLabels.any(XcfaLabel::isAtomicBegin)) {
-            getSharedObjectsWithBFS(edge) { it.getFlatLabels().none(XcfaLabel::isAtomicEnd) }.toSet()
+        val mutexes = flatLabels.filterIsInstance<FenceLabel>().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<XcfaState<*>, XcfaAction>
     private fun getSharedObjectsWithBFS(startTransition: XcfaEdge,
         goFurther: Predicate<XcfaEdge>): Set<Decl<out Type>> {
         val vars = mutableSetOf<Decl<out Type>>()
-        val exploredTransitions = mutableListOf<XcfaEdge>()
-        val transitionsToExplore = mutableListOf<XcfaEdge>()
-        transitionsToExplore.add(startTransition)
-        while (transitionsToExplore.isNotEmpty()) {
-            val exploring = transitionsToExplore.removeFirst()
+        val exploredEdges = mutableListOf<XcfaEdge>()
+        val edgesToExplore = mutableListOf<XcfaEdge>()
+        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<XcfaState<*>, XcfaAction>
         val startThreads = edge.getFlatLabels().filterIsInstance<StartLabel>().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