Skip to content

Commit

Permalink
pthread functions support
Browse files Browse the repository at this point in the history 
This pull request adds support for pthread_mutex_init, pthread_cond_init, pthread_cond_wait, pthread_cond_signal as well as proper mutex support for static partial order reduction algorithms.
  • Loading branch information
@csanadtelbisz
csanadtelbisz authored Oct 13, 2023
2 parents fdc40cf + 821d623 commit 9e8b5cf
Show file tree
Hide file tree
Showing 5 changed files with 211 additions and 149 deletions.
91 changes: 44 additions & 47 deletions subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,38 +71,50 @@ data class XcfaState<S : ExprState> @JvmOverloads constructor(
"ATOMIC_BEGIN" -> changes.add { it.enterMutex("", a.pid) }
"ATOMIC_END" -> changes.add { it.exitMutex("", a.pid) }
in Regex("mutex_lock\\((.*)\\)") -> changes.add { state ->
state.enterMutex(
label.substring("mutex_lock".length + 1, label.length - 1), a.pid)
state.enterMutex(label.substring("mutex_lock".length + 1, label.length - 1), a.pid)
}

in Regex("mutex_unlock\\((.*)\\)") -> changes.add { state ->
state.exitMutex(
label.substring("mutex_unlock".length + 1, label.length - 1), a.pid)
state.exitMutex(label.substring("mutex_unlock".length + 1, label.length - 1), a.pid)
}

in Regex("start_cond_wait\\((.*)\\)") -> {
val args = label.substring("start_cond_wait".length + 1, label.length - 1).split(",")
changes.add { state -> state.enterMutex(args[0], -1) }
changes.add { state -> state.exitMutex(args[1], a.pid) }
}

in Regex("cond_wait\\((.*)\\)") -> {
val args = label.substring("cond_wait".length + 1, label.length - 1).split(",")
changes.add { state -> state.enterMutex(args[0], a.pid) }
changes.add { state -> state.exitMutex(args[0], a.pid) }
changes.add { state -> state.enterMutex(args[1], a.pid) }
}

in Regex("cond_signal\\((.*)\\)") -> changes.add { state ->
state.exitMutex(label.substring("cond_signal".length + 1, label.length - 1), -1)
}

else -> error("Unknown fence label $label")
}
}.let { false }

is InvokeLabel -> {
val proc = xcfa?.procedures?.find { proc -> proc.name == it.name } ?: error(
"No such method ${it.name}.")
val returnStmt = SequenceLabel(
proc.params.withIndex().filter { it.value.second != ParamDirection.IN }
.map { iVal ->
StmtLabel(Assign(
cast((it.params[iVal.index] as RefExpr<*>).decl as VarDecl<*>,
iVal.value.first.type),
cast(iVal.value.first.ref, iVal.value.first.type)),
metadata = it.metadata)
})
proc.params.withIndex().filter { it.value.second != ParamDirection.IN }.map { iVal ->
StmtLabel(Assign(cast((it.params[iVal.index] as RefExpr<*>).decl as VarDecl<*>,
iVal.value.first.type), cast(iVal.value.first.ref, iVal.value.first.type)),
metadata = it.metadata)
})
changes.add { state ->
state.invokeFunction(a.pid, proc, returnStmt, proc.params.toMap(),
it.tempLookup)
state.invokeFunction(a.pid, proc, returnStmt, proc.params.toMap(), it.tempLookup)
}
false
}

is ReturnLabel -> changes.add { state -> state.returnFromFunction(a.pid) }
.let { true }
is ReturnLabel -> changes.add { state -> state.returnFromFunction(a.pid) }.let { true }

is JoinLabel -> {
changes.add { state -> state.enterMutex("${threadLookup[it.pidVar]}", a.pid) }
Expand All @@ -121,12 +133,10 @@ data class XcfaState<S : ExprState> @JvmOverloads constructor(
}

changes.add { state ->
if (checkNotNull(state.processes[a.pid]).locs.isEmpty()) state.endProcess(
a.pid) else state
if (checkNotNull(state.processes[a.pid]).locs.isEmpty()) state.endProcess(a.pid) else state
}

return Pair(changes.fold(this) { current, change -> change(current) },
a.withLabel(SequenceLabel(newLabels)))
return Pair(changes.fold(this) { current, change -> change(current) }, a.withLabel(SequenceLabel(newLabels)))
}

private fun start(startLabel: StartLabel): XcfaState<S> {
Expand All @@ -151,17 +161,13 @@ data class XcfaState<S : ExprState> @JvmOverloads constructor(
val pid = pidCnt++
val lookup = XcfaProcessState.createLookup(procedure, "T$pid", "")
newThreadLookup[startLabel.pidVar] = pid
newProcesses[pid] = XcfaProcessState(
LinkedList(listOf(procedure.initLoc)),
prefix = "T$pid",
varLookup = LinkedList(listOf(lookup)),
returnStmts = LinkedList(listOf(returnStmt)),
newProcesses[pid] = XcfaProcessState(LinkedList(listOf(procedure.initLoc)), prefix = "T$pid",
varLookup = LinkedList(listOf(lookup)), returnStmts = LinkedList(listOf(returnStmt)),
paramStmts = LinkedList(listOf(Pair(
/* init */
SequenceLabel(paramList.filter { it.value != ParamDirection.OUT }.map {
StmtLabel(Assign(cast(it.key.changeVars(lookup), it.key.type),
cast(it.key.changeVars(tempLookup).ref, it.key.type)),
metadata = EmptyMetaData)
cast(it.key.changeVars(tempLookup).ref, it.key.type)), metadata = EmptyMetaData)
}),
/* deinit */
SequenceLabel(paramList.filter { it.value != ParamDirection.IN }.map {
Expand All @@ -184,11 +190,9 @@ data class XcfaState<S : ExprState> @JvmOverloads constructor(
}

private fun invokeFunction(pid: Int, proc: XcfaProcedure, returnStmt: XcfaLabel,
paramList: Map<VarDecl<*>, ParamDirection>,
tempLookup: Map<VarDecl<*>, VarDecl<*>>): XcfaState<S> {
paramList: Map<VarDecl<*>, ParamDirection>, tempLookup: Map<VarDecl<*>, VarDecl<*>>): XcfaState<S> {
val newProcesses: MutableMap<Int, XcfaProcessState> = LinkedHashMap(processes)
newProcesses[pid] = checkNotNull(
processes[pid]?.enterFunction(proc, returnStmt, paramList, tempLookup))
newProcesses[pid] = checkNotNull(processes[pid]?.enterFunction(proc, returnStmt, paramList, tempLookup))
return copy(processes = newProcesses)
}

Expand Down Expand Up @@ -226,15 +230,10 @@ data class XcfaState<S : ExprState> @JvmOverloads constructor(
}
}

data class XcfaProcessState(
val locs: LinkedList<XcfaLocation>,
val varLookup: LinkedList<Map<VarDecl<*>, VarDecl<*>>>,
data class XcfaProcessState(val locs: LinkedList<XcfaLocation>, val varLookup: LinkedList<Map<VarDecl<*>, VarDecl<*>>>,
val returnStmts: LinkedList<XcfaLabel> = LinkedList(listOf(NopLabel)),
val paramStmts: LinkedList<Pair<XcfaLabel, XcfaLabel>> = LinkedList(
listOf(Pair(NopLabel, NopLabel))),
val paramsInitialized: Boolean = false,
val prefix: String = ""
) {
val paramStmts: LinkedList<Pair<XcfaLabel, XcfaLabel>> = LinkedList(listOf(Pair(NopLabel, NopLabel))),
val paramsInitialized: Boolean = false, val prefix: String = "") {

fun withNewLoc(l: XcfaLocation): XcfaProcessState {
val deque: LinkedList<XcfaLocation> = LinkedList(locs)
Expand All @@ -249,8 +248,7 @@ data class XcfaProcessState(
else -> "${locs.peek()!!} [${locs.size}], initilized=$paramsInitialized"
}

fun enterFunction(xcfaProcedure: XcfaProcedure, returnStmt: XcfaLabel,
paramList: Map<VarDecl<*>, ParamDirection>,
fun enterFunction(xcfaProcedure: XcfaProcedure, returnStmt: XcfaLabel, paramList: Map<VarDecl<*>, ParamDirection>,
tempLookup: Map<VarDecl<*>, VarDecl<*>>): XcfaProcessState {
val deque: LinkedList<XcfaLocation> = LinkedList(locs)
val varLookup: LinkedList<Map<VarDecl<*>, VarDecl<*>>> = LinkedList(varLookup)
Expand All @@ -272,8 +270,8 @@ data class XcfaProcessState(
cast(it.key.changeVars(lookup).ref, it.key.type)), metadata = EmptyMetaData)
}),
))
return copy(locs = deque, varLookup = varLookup, returnStmts = returnStmts,
paramStmts = paramStmts, paramsInitialized = false)
return copy(locs = deque, varLookup = varLookup, returnStmts = returnStmts, paramStmts = paramStmts,
paramsInitialized = false)
}

fun exitFunction(): XcfaProcessState {
Expand All @@ -285,8 +283,7 @@ data class XcfaProcessState(
varLookup.pop()
returnStmts.pop()
paramStmts.pop()
return copy(locs = deque, varLookup = varLookup, returnStmts = returnStmts,
paramStmts = paramStmts)
return copy(locs = deque, varLookup = varLookup, returnStmts = returnStmts, paramStmts = paramStmts)
}

override fun equals(other: Any?): Boolean {
Expand All @@ -310,8 +307,8 @@ data class XcfaProcessState(
companion object {

fun createLookup(proc: XcfaProcedure, threadPrefix: String,
procPrefix: String): Map<VarDecl<*>, VarDecl<*>> =
listOf(proc.params.map { it.first }, proc.vars).flatten().associateWith {
procPrefix: String): Map<VarDecl<*>, VarDecl<*>> = listOf(proc.params.map { it.first }, proc.vars).flatten()
.associateWith {
val sj = StringJoiner("::")
if (threadPrefix != "") sj.add(threadPrefix)
else sj.add("_")
Expand Down
69 changes: 32 additions & 37 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(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,39 +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
Loading

0 comments on commit 9e8b5cf

Please sign in to comment.