From 99691655b8f6202c7229b93b0a66467da57f1cf6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Csan=C3=A1d=20Telbisz?= Date: Fri, 13 Oct 2023 19:24:00 +0200 Subject: [PATCH] spor support for mutexes --- .../theta/xcfa/analysis/por/XcfaAasporLts.kt | 5 +- .../theta/xcfa/analysis/por/XcfaSporLts.kt | 57 +++++++++++++++---- .../java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt | 6 +- 3 files changed, 54 insertions(+), 14 deletions(-) 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 64ed3d15e3..376fc4855e 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 @@ -35,7 +35,7 @@ class XcfaAasporLts(xcfa: XCFA, private val ignoredVarRegistry: MutableMap() 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, 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, XcfaAction> // 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) + 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, 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): Collection> { 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, + enabledActionsByProcess: Map>) { + 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().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, 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> = - if (edge.getFlatLabels().any(XcfaLabel::isAtomicBegin)) { - getSharedObjectsWithBFS(edge) { - it.getFlatLabels().none(XcfaLabel::isAtomicEnd) - }.toSet() + private fun getUsedSharedObjects(edge: XcfaEdge): Set> { + 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 index 244e1e5548..e4ff9e4b8d 100644 --- 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) { // 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)