spor support for mutexes

ftsrg · Oct 13, 2023 · 9969165 · 9969165
1 parent f24d77d
commit 9969165
Show file tree

Hide file tree

Showing 3 changed files with 54 additions and 14 deletions.
diff --git a/...ects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt b/...ects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/por/XcfaAasporLts.kt
@@ -35,7 +35,7 @@ class XcfaAasporLts(xcfa: XCFA, private val ignoredVarRegistry: MutableMap<Decl<
         // The minimal persistent set is stored
         var minimalPersistentSet = mutableSetOf<XcfaAction>()
         val persistentSetFirstActions = if (exploredActions.isEmpty()) {
-            getPersistentSetFirstActions(allEnabledActions)
+            getPersistentSetFirstActions(state, allEnabledActions)
         } else {
             setOf(exploredActions)
         }
@@ -116,8 +116,7 @@ class XcfaAasporLts(xcfa: XCFA, private val ignoredVarRegistry: MutableMap<Decl<
         if (isSameProcess(persistentSetAction, action)) {
             return true
         }
-        val usedByPersistentSetAction = getCachedUsedSharedObjects(
-            getEdgeOf(persistentSetAction))
+        val usedByPersistentSetAction = getCachedUsedSharedObjects(getEdgeOf(persistentSetAction))
         val influencedSharedObjects = getInfluencedSharedObjects(getEdgeOf(action))
         for (varDecl in influencedSharedObjects) {
             if (usedByPersistentSetAction.contains(varDecl)) {

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
@@ -40,7 +40,7 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS<XcfaState<*>, XcfaAction>
 
     companion object {
 
-        private val random: Random = Random.Default
+        var random: Random = Random.Default
         private val simpleXcfaLts = getXcfaLts()
     }
 
@@ -78,7 +78,7 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS<XcfaState<*>, XcfaAction>
 
         // 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(allEnabledActions)
+        val persistentSetFirstActions = getPersistentSetFirstActions(state, allEnabledActions)
         for (firstActions in persistentSetFirstActions) {
             val persistentSet = calculatePersistentSet(allEnabledActions, firstActions)
             if (minimalPersistentSet.isEmpty() || persistentSet.size < minimalPersistentSet.size) {
@@ -103,11 +103,37 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS<XcfaState<*>, XcfaAction>
      * @param allEnabledActions the enabled actions in the present state
      * @return the possible starting actions of a persistent set
      */
-    protected fun getPersistentSetFirstActions(
+    protected fun getPersistentSetFirstActions(state: XcfaState<*>,
         allEnabledActions: Collection<XcfaAction>): Collection<Collection<XcfaAction>> {
         val enabledActionsByProcess = allEnabledActions.groupBy(XcfaAction::pid)
         val enabledProcesses = enabledActionsByProcess.keys.toList().shuffled(random)
-        return enabledProcesses.map { checkNotNull(enabledActionsByProcess[it]) }
+        return enabledProcesses.map { pid ->
+            val firstProcesses = mutableSetOf(pid)
+            checkMutexBlocks(state, pid, firstProcesses, enabledActionsByProcess)
+            firstProcesses.flatMap { checkNotNull(enabledActionsByProcess[it]) }
+        }
+    }
+
+    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 }
+        }
+        disabledOutEdges.forEach { edge ->
+            edge.getFlatLabels().filterIsInstance<FenceLabel>().forEach { fence ->
+                fence.labels.filter { it.startsWith("mutex_lock") }.forEach { lock ->
+                    val mutex = lock.substringAfter('(').substringBefore(')')
+                    state.mutexes[mutex]?.let { pid2 ->
+                        if (pid2 !in firstProcesses) {
+                            firstProcesses.add(pid2)
+                            checkMutexBlocks(state, pid2, firstProcesses, enabledActionsByProcess)
+                        }
+                    }
+                }
+            }
+        }
     }
 
     /**
@@ -188,14 +214,25 @@ open class XcfaSporLts(protected val xcfa: XCFA) : LTS<XcfaState<*>, XcfaAction>
      * @param edge whose global variables are to be returned
      * @return the set of directly or indirectly used global variables
      */
-    private fun getUsedSharedObjects(edge: XcfaEdge): Set<Decl<out Type>> =
-        if (edge.getFlatLabels().any(XcfaLabel::isAtomicBegin)) {
-            getSharedObjectsWithBFS(edge) {
-                it.getFlatLabels().none(XcfaLabel::isAtomicEnd)
-            }.toSet()
+    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()
         } else {
-            getDirectlyUsedSharedObjects(edge)
+            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)
+            }
         }
+    }
 
     /**
      * Same as [getUsedSharedObjects] with an additional cache layer.

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt
@@ -43,6 +43,7 @@ import hu.bme.mit.theta.xcfa.analysis.ErrorDetection
 import hu.bme.mit.theta.xcfa.analysis.XcfaAction
 import hu.bme.mit.theta.xcfa.analysis.XcfaState
 import hu.bme.mit.theta.xcfa.analysis.por.XcfaDporLts
+import hu.bme.mit.theta.xcfa.analysis.por.XcfaSporLts
 import hu.bme.mit.theta.xcfa.cli.utils.XcfaWitnessWriter
 import hu.bme.mit.theta.xcfa.cli.witnesses.XcfaTraceConcretizer
 import hu.bme.mit.theta.xcfa.model.XCFA
@@ -174,7 +175,10 @@ class XcfaCli(private val args: Array<String>) {
 
         // propagating input variables
         LbePass.level = lbeLevel
-        if (randomSeed >= 0) XcfaDporLts.random = Random(randomSeed)
+        if (randomSeed >= 0){
+            XcfaSporLts.random = Random(randomSeed)
+            XcfaDporLts.random = Random(randomSeed)
+        }
         if (argToFile) {
             WebDebuggerLogger.enableWebDebuggerLogger()
             WebDebuggerLogger.getInstance().setTitle(input?.name)