Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

pthread functions support #228

Merged
merged 5 commits into from
Oct 13, 2023
Merged

pthread functions support #228

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
36f27f1
pthread_cond_wait, pthread_cond_init
csanadtelbisz Oct 12, 2023
8837515
start cond wait
csanadtelbisz Oct 12, 2023
f24d77d
Merge branch 'xcfa-refactor' into xcfa-pthread-functions
csanadtelbisz Oct 13, 2023
9969165
spor support for mutexes
csanadtelbisz Oct 13, 2023
821d623
spor cleanup + checkMutexBlocks checkNotNull fix
csanadtelbisz Oct 13, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
91 changes: 44 additions & 47 deletions subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt
View file
Open in desktop
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
Open in desktop
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