Skip to content

Commit

Permalink
join guard fix
Browse files Browse the repository at this point in the history
  • Loading branch information
@csanadtelbisz
csanadtelbisz committed Apr 17, 2024
1 parent 2fd9018 commit 78ced2b
Show file tree
Hide file tree
Showing 3 changed files with 54 additions and 54 deletions.
8 changes: 5 additions & 3 deletions subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/oc/OcTypes.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,12 +41,12 @@ enum class EventType { WRITE, READ }
abstract class Event(
val const: IndexedConstDecl<*>,
val type: EventType,
val guard: List<Expr<BoolType>>,
var guard: Set<Expr<BoolType>>,
val pid: Int,
val clkId: Int
) {

val guardExpr: Expr<BoolType> = guard.toAnd()
val guardExpr: Expr<BoolType> get() = guard.toAnd()
var assignment: Expr<BoolType>? = null
var enabled: Boolean? = null

Expand Down Expand Up @@ -77,7 +77,9 @@ data class Relation<E : Event>(
val declRef: RefExpr<BoolType> = RefExpr.of(decl)
var enabled: Boolean? = null

override fun toString() = "Relation($type, ${from.const.name}[${from.type.toString()[0]}], ${to.const.name}[${to.type.toString()[0]}])"
override fun toString() =
"Relation($type, ${from.const.name}[${from.type.toString()[0]}], ${to.const.name}[${to.type.toString()[0]}])"

fun enabled(valuation: Map<Decl<*>, LitExpr<*>>): Boolean? {
enabled = if (type == RelationType.PO) true else valuation[decl]?.let { (it as BoolLitExpr).value }
return enabled
Expand Down
83 changes: 40 additions & 43 deletions ...jects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,10 @@ package hu.bme.mit.theta.xcfa.analysis.oc

import hu.bme.mit.theta.analysis.algorithm.SafetyChecker
import hu.bme.mit.theta.analysis.algorithm.SafetyResult
import hu.bme.mit.theta.analysis.algorithm.oc.*
import hu.bme.mit.theta.analysis.algorithm.oc.EventType
import hu.bme.mit.theta.analysis.algorithm.oc.OcChecker
import hu.bme.mit.theta.analysis.algorithm.oc.Relation
import hu.bme.mit.theta.analysis.algorithm.oc.RelationType
import hu.bme.mit.theta.analysis.unit.UnitPrec
import hu.bme.mit.theta.common.logging.Logger
import hu.bme.mit.theta.core.decl.*
Expand All @@ -35,12 +38,10 @@ import hu.bme.mit.theta.core.type.inttype.IntExprs.Int
import hu.bme.mit.theta.core.utils.ExprUtils
import hu.bme.mit.theta.core.utils.TypeUtils.cast
import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory
import hu.bme.mit.theta.xcfa.*
import hu.bme.mit.theta.xcfa.analysis.XcfaAction
import hu.bme.mit.theta.xcfa.analysis.XcfaPrec
import hu.bme.mit.theta.xcfa.analysis.XcfaState
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 hu.bme.mit.theta.xcfa.passes.AssumeFalseRemovalPass
import hu.bme.mit.theta.xcfa.passes.AtomicReadsOneWritePass
Expand Down Expand Up @@ -68,10 +69,12 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv
private val rfs = mutableMapOf<VarDecl<*>, MutableList<R>>()

override fun check(prec: XcfaPrec<UnitPrec>?): SafetyResult<XcfaState<*>, XcfaAction> = let {
if (xcfa.initProcedures.size > 1) error("Multiple entry points are not supported by this checker.")
if (xcfa.initProcedures.size > 1) error("Multiple entry points are not supported by OC checker.")

logger.write(Logger.Level.MAINSTEP, "Adding constraints...\n")
if (!addConstraints()) return@let SafetyResult.safe() // no violations
xcfa.initProcedures.forEach { processThread(Thread(it.first)) }
addCrossThreadRelations()
if (!addToSolver()) return@let SafetyResult.safe() // no violations in the model

logger.write(Logger.Level.MAINSTEP, "Start checking...\n")
val status = ocChecker.check(events, pos, rfs)
Expand All @@ -85,25 +88,11 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv
}
}.also { logger.write(Logger.Level.MAINSTEP, "OC checker result: $it\n") }

private fun addConstraints(): Boolean {
val threads = xcfa.initProcedures.map { Thread(it.first) }.toMutableSet()
this.threads.addAll(threads)
while (threads.isNotEmpty()) {
val thread = threads.first()
threads.remove(thread)
val newThreads = processThread(thread)
threads.addAll(newThreads)
this.threads.addAll(newThreads)
}

addCrossThreadRelations()
return addToSolver()
}

private fun processThread(thread: Thread): List<Thread> {
threads.add(thread)
val pid = thread.pid
var last = listOf<E>()
var guard = listOf<Expr<BoolType>>()
var guard = setOf<Expr<BoolType>>()
lateinit var lastWrites: MutableMap<VarDecl<*>, Set<E>>
lateinit var edge: XcfaEdge
var inEdge = false
Expand Down Expand Up @@ -142,7 +131,7 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv
check(current.incoming == current.loc.incomingEdges.size)
check(current.incoming == current.guards.size || current.loc.initial)
check(current.incoming == current.lastWrites.size) // lastEvents intentionally skipped
check(current.incoming == current.pidLookups.size)
check(current.incoming == current.threadLookups.size)
check(current.incoming == current.atomics.size)
check(current.atomics.all { it == current.atomics.first() }) // bad pattern otherwise

Expand All @@ -153,12 +142,10 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv
}

if (current.loc.final) {
current.lastEvents.forEach { final ->
thread.joinEvents.forEach { join -> po(final, join) }
}
thread.finalEvents.addAll(current.lastEvents)
}

val mergedGuard = current.guards.toOrInList()
val mergedGuard = current.guards.toOrInSet()
val assumeConsts = mutableMapOf<VarDecl<*>, MutableList<ConstDecl<*>>>()

for (e in current.loc.outgoingEdges) {
Expand All @@ -168,13 +155,16 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv
// intersection of guards of incoming edges:
guard = mergedGuard
lastWrites = current.lastWrites.merge().toMutableMap()
val pidLookup = current.pidLookups.merge { s1, s2 ->
val threadLookup = current.threadLookups.merge { s1, s2 ->
s1 + s2.filter { (guard2, _) -> s1.none { (guard1, _) -> guard1 == guard2 } }
}.toMutableMap()
var firstLabel = true
atomicEntered = current.atomics.firstOrNull()

edge.getFlatLabels().forEach { label ->
if (label.references.isNotEmpty() || label.dereferences.isNotEmpty()) {
error("References not supported by OC checker.")
}
when (label) {
is StmtLabel -> {
when (val stmt = label.stmt) {
Expand Down Expand Up @@ -217,28 +207,35 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv

is StartLabel -> {
// TODO StartLabel params
if (label.name in thread.startHistory) {
error("Recursive thread start not supported by OC checker.")
}
val procedure = xcfa.procedures.find { it.name == label.name }
?: error("Procedure not found: ${label.name}")
last = newEvent(label.pidVar, EventType.WRITE)
val pidVar = label.pidVar.threadVar(pid)
if (this.threads.any { it.pidVar == pidVar }) {
error("Multi-thread use of pthread_t variables are not supported by this checker.")
error("Using a pthread_t variable in multiple threads is not supported by OC checker.")
}
val newThread = Thread(procedure, guard, pidVar, last.first())
val newHistory = thread.startHistory + thread.procedure.name
val newThread = Thread(procedure, guard, pidVar, last.first(), newHistory)
last.first().assignment = Eq(last.first().const.ref, Int(newThread.pid))
pidLookup[pidVar] = setOf(Pair(guard, newThread.pid))
threads.add(newThread)
threadLookup[pidVar] = setOf(Pair(guard, newThread))
processThread(newThread)
}

is JoinLabel -> {
val guardTemp = guard
val incomingGuard = guard
val lastEvents = mutableListOf<E>()
pidLookup[label.pidVar.threadVar(pid)]?.forEach { (g, pid) ->
guard = g
lastEvents.addAll(newEvent(label.pidVar, EventType.READ))
threads.find { it.pid == pid }?.joinEvents?.add(lastEvents.last())
} ?: error("Thread started in a different thread: not supported by this checker.")
guard = guardTemp
val joinGuards = mutableListOf<Set<Expr<BoolType>>>()
threadLookup[label.pidVar.threadVar(pid)]?.forEach { (g, thread) ->
guard = incomingGuard + g + thread.finalEvents.map { it.guard }.toOrInSet()
val joinEvent = newEvent(label.pidVar, EventType.READ).first()
thread.finalEvents.forEach { final -> po(final, joinEvent) }
lastEvents.add(joinEvent)
joinGuards.add(guard)
} ?: error("Thread started in a different thread: not supported by OC checker.")
guard = joinGuards.toOrInSet()
last = lastEvents
}

Expand All @@ -251,7 +248,7 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv
}

is NopLabel -> {}
else -> error("Unsupported label type by this checker: $label")
else -> error("Unsupported label type by OC checker: $label")
}
firstLabel = false
}
Expand All @@ -261,7 +258,7 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv
searchItem.guards.add(guard)
searchItem.lastEvents.addAll(last)
searchItem.lastWrites.add(lastWrites)
searchItem.pidLookups.add(pidLookup)
searchItem.threadLookups.add(threadLookup)
searchItem.atomics.add(atomicEntered)
searchItem.incoming++
if (searchItem.incoming == searchItem.loc.incomingEdges.size) {
Expand All @@ -274,7 +271,7 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv
for (e in current.loc.outgoingEdges) {
val first = e.getFlatLabels().first()
if (first !is StmtLabel || first.stmt !is AssumeStmt) {
error("Branching with non-assume labels not supported by this checker.")
error("Branching with non-assume labels not supported by OC checker.")
}
}
assumeConsts.forEach { (_, set) ->
Expand All @@ -287,7 +284,7 @@ class XcfaOcChecker(xcfa: XCFA, decisionProcedure: OcDecisionProcedureType, priv
}
}

if (waitList.isNotEmpty()) error("Loops and dangling edges not supported by this checker.")
if (waitList.isNotEmpty()) error("Loops and dangling edges not supported by OC checker.")
return threads
}

Expand Down
17 changes: 9 additions & 8 deletions ...rojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcTypes.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,16 +49,16 @@ internal fun Collection<Expr<BoolType>>.toAnd(): Expr<BoolType> = when (size) {
/**
* Takes the OR of the contained lists mapped to an AND expression. Simplifications are made based on the list sizes.
*/
internal fun Collection<List<Expr<BoolType>>>.toOrInList(): List<Expr<BoolType>> = when (size) {
0 -> listOf()
internal fun Collection<Set<Expr<BoolType>>>.toOrInSet(): Set<Expr<BoolType>> = when (size) {
0 -> setOf()
1 -> first()
else -> listOf(Or(map { it.toAnd() }))
else -> setOf(Or(map { it.toAnd() }))
}

internal class XcfaEvent(
const: IndexedConstDecl<*>,
type: EventType,
guard: List<Expr<BoolType>>,
guard: Set<Expr<BoolType>>,
pid: Int,
val edge: XcfaEdge,
clkId: Int = uniqueId()
Expand All @@ -80,10 +80,11 @@ internal data class Violation(

internal data class Thread(
val procedure: XcfaProcedure,
val guard: List<Expr<BoolType>> = listOf(),
val guard: Set<Expr<BoolType>> = setOf(),
val pidVar: VarDecl<*>? = null,
val startEvent: XcfaEvent? = null,
val joinEvents: MutableSet<XcfaEvent> = mutableSetOf(),
val startHistory: List<String> = listOf(),
val finalEvents: MutableSet<XcfaEvent> = mutableSetOf(),
val pid: Int = uniqueId(),
) {

Expand All @@ -96,10 +97,10 @@ internal data class Thread(

internal data class SearchItem(val loc: XcfaLocation) {

val guards: MutableList<List<Expr<BoolType>>> = mutableListOf()
val guards: MutableList<Set<Expr<BoolType>>> = mutableListOf()
val lastEvents: MutableList<XcfaEvent> = mutableListOf()
val lastWrites: MutableList<Map<VarDecl<*>, Set<XcfaEvent>>> = mutableListOf()
val pidLookups: MutableList<Map<VarDecl<*>, Set<Pair<List<Expr<BoolType>>, Int>>>> = mutableListOf()
val threadLookups: MutableList<Map<VarDecl<*>, Set<Pair<Set<Expr<BoolType>>, Thread>>>> = mutableListOf()
val atomics: MutableList<Boolean?> = mutableListOf()
var incoming: Int = 0
}
Expand Down

0 comments on commit 78ced2b

Please sign in to comment.