From e89774e4f2dbc4a8269b6577353cce0c7f783994 Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Fri, 29 Nov 2024 11:43:25 +0100
Subject: [PATCH] Added low-effort sync

---
 .../hu/bme/mit/theta/xcfa/analysis/XcfaState.kt   | 15 +++++++++++++++
 .../java/hu/bme/mit/theta/xcfa/model/XcfaLabel.kt | 10 ++++++++++
 2 files changed, 25 insertions(+)

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
index 41b35eccc3..bea0bad1c0 100644
--- 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
index 8e8c01f999..2a8e09b981 100644
--- 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 {