Added low-effort sync

ftsrg · Nov 29, 2024 · e89774e · e89774e
1 parent 0be641c
commit e89774e
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 0 deletions.
diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt
@@ -41,6 +41,7 @@ constructor(
   val mutexes: Map<String, Int> = processes.keys.associateBy { "$it" },
   val threadLookup: Map<VarDecl<*>, Int> = emptyMap(),
   val bottom: Boolean = false,
+  val syncingOn: String? = null,
 ) : ExprState {
 
   constructor(
@@ -172,6 +173,8 @@ constructor(
           is StartLabel -> changes.add { state -> state.start(it) }.let { true }
           is StmtLabel -> true
           is WriteLabel -> error("Read/Write labels not yet supported")
+          is SyncSendLabel -> changes.add { state -> state.enterSync(it) }.let { true }
+          is SyncRecvLabel -> changes.add { state -> state.exitSync(it) }.let { true }
         }
       }
 
@@ -185,6 +188,18 @@ constructor(
     )
   }
 
+  private fun enterSync(syncSendLabel: SyncSendLabel): XcfaState<S> {
+    syncingOn?.also {
+      return copy(bottom = true)
+    }
+    return copy(syncingOn = syncSendLabel.key)
+  }
+
+  private fun exitSync(syncRecvLabel: SyncRecvLabel): XcfaState<S> {
+    syncingOn?.takeIf { it == syncRecvLabel.key } ?: return copy(bottom = true)
+    return copy(syncingOn = null)
+  }
+
   private fun start(startLabel: StartLabel): XcfaState<S> {
     val newProcesses: MutableMap<Int, XcfaProcessState> = LinkedHashMap(processes)
     val newThreadLookup: MutableMap<VarDecl<*>, Int> = LinkedHashMap(threadLookup)

diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaLabel.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/model/XcfaLabel.kt
@@ -240,6 +240,16 @@ constructor(val labels: Set<XcfaLabel>, override val metadata: MetaData = EmptyM
   }
 }
 
+data class SyncSendLabel
+@JvmOverloads
+constructor(val key: String, override val metadata: MetaData = EmptyMetaData) :
+  XcfaLabel(metadata = metadata)
+
+data class SyncRecvLabel
+@JvmOverloads
+constructor(val key: String, override val metadata: MetaData = EmptyMetaData) :
+  XcfaLabel(metadata = metadata)
+
 object NopLabel : XcfaLabel(metadata = EmptyMetaData) {
 
   override fun toStmt(): Stmt {