From 1d05f0fefa2e1acf5a35f90365df4b7ba4bdd858 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 12 Oct 2023 13:00:52 +0300
Subject: [PATCH 01/34] Add hacky atomic protection privatization

---
 src/analyses/basePriv.ml                        | 16 ++++++++++++----
 src/analyses/mutexAnalysis.ml                   |  4 ++--
 tests/regression/29-svcomp/16-atomic_priv.c     |  2 +-
 tests/regression/29-svcomp/18-atomic_fun_priv.c |  2 +-
 4 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index 0154924a1c..82bdebe617 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -687,22 +687,27 @@ struct
 
   let startstate () = P.empty ()
 
-  let read_global ask getg (st: BaseComponents (D).t) x =
+  let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x =
     if P.mem x st.priv then
       CPA.find x st.cpa
+    else if ask.f MustBeAtomic then
+      VD.join (CPA.find x st.cpa) (getg (V.unprotected x))
     else if is_unprotected ask x then
       getg (V.unprotected x) (* CPA unnecessary because all values in GUnprot anyway *)
     else
       VD.join (CPA.find x st.cpa) (getg (V.protected x))
 
-  let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v =
+  let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v =
     if not invariant then (
-      sideg (V.unprotected x) v;
+      if not (ask.f MustBeAtomic) then
+        sideg (V.unprotected x) v;
       if !earlyglobs then (* earlyglobs workaround for 13/60 *)
         sideg (V.protected x) v
         (* Unlock after invariant will still side effect refined value (if protected) from CPA, because cannot distinguish from non-invariant write since W is implicit. *)
     );
-    if is_unprotected ask x then
+    if ask.f MustBeAtomic then
+      {st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv}
+    else if is_unprotected ask x then
       st
     else
       {st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv}
@@ -710,6 +715,7 @@ struct
   let lock ask getg st m = st
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
+    let atomic = LockDomain.Addr.equal m (LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var) in
     (* TODO: what about G_m globals in cpa that weren't actually written? *)
     CPA.fold (fun x v (st: BaseComponents (D).t) ->
         if is_protected_by ask m x then ( (* is_in_Gm *)
@@ -718,6 +724,8 @@ struct
              then inner unlock shouldn't yet publish. *)
           if not Param.check_read_unprotected || is_unprotected_without ask ~write:false x m then
             sideg (V.protected x) v;
+          if atomic then
+            sideg (V.unprotected x) v;
 
           if is_unprotected_without ask x m then (* is_in_V' *)
             {st with cpa = CPA.remove x st.cpa; priv = P.remove x st.priv}
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index ee050f55ca..702b3b4224 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -229,9 +229,9 @@ struct
       let mutex_lockset = Lockset.export_locks @@ Lockset.singleton (mutex, true) in
       let protecting = protecting ~write protection v in
       (* TODO: unsound in 29/24, why did we do this before? *)
-      (* if LockDomain.Addr.equal mutex verifier_atomic then
+      if LockDomain.Addr.equal mutex (LockDomain.Addr.of_var LF.verifier_atomic_var) then
         true
-      else *)
+      else
       Mutexes.leq mutex_lockset protecting
     | Queries.MustLockset ->
       let held_locks = Lockset.export_locks (Lockset.filter snd ls) in
diff --git a/tests/regression/29-svcomp/16-atomic_priv.c b/tests/regression/29-svcomp/16-atomic_priv.c
index 92e1896f58..103769cc33 100644
--- a/tests/regression/29-svcomp/16-atomic_priv.c
+++ b/tests/regression/29-svcomp/16-atomic_priv.c
@@ -21,7 +21,7 @@ void *t_fun(void *arg) {
 int main(void) {
   pthread_t id;
   pthread_create(&id, NULL, t_fun, NULL);
-  __goblint_check(myglobal == 5); // TODO
+  __goblint_check(myglobal == 5);
   __VERIFIER_atomic_begin();
   __goblint_check(myglobal == 5);
   __VERIFIER_atomic_end();
diff --git a/tests/regression/29-svcomp/18-atomic_fun_priv.c b/tests/regression/29-svcomp/18-atomic_fun_priv.c
index 0449f9af0d..cb7e790ebd 100644
--- a/tests/regression/29-svcomp/18-atomic_fun_priv.c
+++ b/tests/regression/29-svcomp/18-atomic_fun_priv.c
@@ -21,7 +21,7 @@ void *t_fun(void *arg) {
 int main(void) {
   pthread_t id;
   pthread_create(&id, NULL, t_fun, NULL);
-  __goblint_check(myglobal == 5); // TODO
+  __goblint_check(myglobal == 5);
   __VERIFIER_atomic_begin();
   __goblint_check(myglobal == 5);
   __VERIFIER_atomic_end();

From b60e836e65eb0f875f9b5d005e086cc4c9c4ed06 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 12 Oct 2023 16:48:09 +0300
Subject: [PATCH 02/34] Add hacky atomic relation mutex-meet privatization

---
 src/analyses/apron/relationPriv.apron.ml      | 88 ++++++++++++++-----
 tests/regression/46-apron2/58-atomic_priv.c   | 30 +++++++
 .../regression/46-apron2/59-atomic_fun_priv.c | 30 +++++++
 .../46-apron2/60-atomic_priv_sound.c          | 28 ++++++
 .../46-apron2/61-atomic_priv_sound2.c         | 43 +++++++++
 .../46-apron2/62-atomic_priv_sound3.c         | 23 +++++
 6 files changed, 218 insertions(+), 24 deletions(-)
 create mode 100644 tests/regression/46-apron2/58-atomic_priv.c
 create mode 100644 tests/regression/46-apron2/59-atomic_fun_priv.c
 create mode 100644 tests/regression/46-apron2/60-atomic_priv_sound.c
 create mode 100644 tests/regression/46-apron2/61-atomic_priv_sound2.c
 create mode 100644 tests/regression/46-apron2/62-atomic_priv_sound3.c

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index b386af162b..abdbb2f791 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -483,47 +483,69 @@ struct
     let get_mutex_inits' = RD.keep_vars get_mutex_inits [g_var] in
     RD.join get_mutex_global_g get_mutex_inits'
 
-  let read_global ask getg (st: relation_components_t) g x: RD.t =
+  let read_global (ask: Q.ask) getg (st: relation_components_t) g x: RD.t =
+    let atomic = ask.f MustBeAtomic in
     let rel = st.rel in
     (* lock *)
-    let rel = RD.meet rel (get_mutex_global_g_with_mutex_inits ask getg g) in
+    let rel =
+      if atomic && RD.mem_var rel (AV.global g) then
+        rel
+      else
+        RD.meet rel (get_mutex_global_g_with_mutex_inits ask getg g)
+    in
     (* read *)
     let g_var = AV.global g in
     let x_var = AV.local x in
     let rel_local = RD.add_vars rel [g_var] in
     let rel_local = RD.assign_var rel_local x_var g_var in
     (* unlock *)
-    let rel_local' =
-      if is_unprotected ask g then
-        RD.remove_vars rel_local [g_var]
-      else
-        rel_local
-    in
-    rel_local'
+    if not atomic then (
+      let rel_local' =
+        if is_unprotected ask g then
+          RD.remove_vars rel_local [g_var]
+        else
+          rel_local
+      in
+      rel_local'
+    )
+    else
+      rel_local
 
-  let write_global ?(invariant=false) ask getg sideg (st: relation_components_t) g x: relation_components_t =
+  let write_global ?(invariant=false) (ask: Q.ask) getg sideg (st: relation_components_t) g x: relation_components_t =
+    let atomic = ask.f MustBeAtomic in
     let rel = st.rel in
     (* lock *)
-    let rel = RD.meet rel (get_mutex_global_g_with_mutex_inits ask getg g) in
+    let rel =
+      if atomic && RD.mem_var rel (AV.global g) then
+        rel
+      else
+        RD.meet rel (get_mutex_global_g_with_mutex_inits ask getg g)
+    in
     (* write *)
     let g_var = AV.global g in
     let x_var = AV.local x in
     let rel_local = RD.add_vars rel [g_var] in
     let rel_local = RD.assign_var rel_local g_var x_var in
     (* unlock *)
+    if not (ask.f MustBeAtomic) then (
     let rel_side = RD.keep_vars rel_local [g_var] in
-    sideg (V.global g) rel_side;
-    let rel_local' =
-      if is_unprotected ask g then
-        RD.remove_vars rel_local [g_var]
-      else
-        rel_local
-    in
-    {st with rel = rel_local'}
+      sideg (V.global g) rel_side;
+      let rel_local' =
+        if is_unprotected ask g then
+          RD.remove_vars rel_local [g_var]
+        else
+          rel_local
+      in
+      {st with rel = rel_local'}
+    )
+    else
+      {st with rel = rel_local}
+
 
   let lock ask getg (st: relation_components_t) m =
+    let atomic = LockDomain.Addr.equal m (LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var) in
     (* TODO: somehow actually unneeded here? *)
-    if Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+    if not atomic && Locksets.(not (Lockset.mem m (current_lockset ask))) then (
       let rel = st.rel in
       let get_m = get_m_with_mutex_inits ask getg m in
       (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
@@ -535,11 +557,29 @@ struct
       st (* sound w.r.t. recursive lock *)
 
   let unlock ask getg sideg (st: relation_components_t) m: relation_components_t =
+    let atomic = LockDomain.Addr.equal m (LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var) in
     let rel = st.rel in
-    let rel_side = keep_only_protected_globals ask m rel in
-    sideg (V.mutex m) rel_side;
-    let rel_local = remove_globals_unprotected_after_unlock ask m rel in
-    {st with rel = rel_local}
+    if not atomic then (
+      let rel_side = keep_only_protected_globals ask m rel in
+      sideg (V.mutex m) rel_side;
+      let rel_local = remove_globals_unprotected_after_unlock ask m rel in
+      {st with rel = rel_local}
+    )
+    else (
+      List.iter (fun var ->
+          match AV.find_metadata var with
+          | Some (Global g) -> sideg (V.global g) (RD.keep_vars rel [AV.global g])
+          | _ -> ()
+        ) (RD.vars rel);
+      let rel_local =
+        let newly_unprot var = match AV.find_metadata var with
+          | Some (Global g) -> is_unprotected ask g
+          | _ -> false
+        in
+        RD.remove_filter rel newly_unprot
+      in
+      {st with rel = rel_local}
+    )
 
   let thread_join ?(force=false) ask getg exp st = st
   let thread_return ask getg sideg tid st = st
diff --git a/tests/regression/46-apron2/58-atomic_priv.c b/tests/regression/46-apron2/58-atomic_priv.c
new file mode 100644
index 0000000000..e8d474357b
--- /dev/null
+++ b/tests/regression/46-apron2/58-atomic_priv.c
@@ -0,0 +1,30 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.base.privatization none
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int myglobal = 5;
+
+void *t_fun(void *arg) {
+  __VERIFIER_atomic_begin();
+  __goblint_check(myglobal == 5);
+  myglobal++;
+  __goblint_check(myglobal == 6);
+  myglobal--;
+  __goblint_check(myglobal == 5);
+  __VERIFIER_atomic_end();
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  __goblint_check(myglobal == 5);
+  __VERIFIER_atomic_begin();
+  __goblint_check(myglobal == 5);
+  __VERIFIER_atomic_end();
+  pthread_join (id, NULL);
+  return 0;
+}
diff --git a/tests/regression/46-apron2/59-atomic_fun_priv.c b/tests/regression/46-apron2/59-atomic_fun_priv.c
new file mode 100644
index 0000000000..21df5d380f
--- /dev/null
+++ b/tests/regression/46-apron2/59-atomic_fun_priv.c
@@ -0,0 +1,30 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.base.privatization none
+#include <pthread.h>
+#include <goblint.h>
+
+int myglobal = 5;
+
+// atomic by function name prefix
+void __VERIFIER_atomic_fun() {
+  __goblint_check(myglobal == 5);
+  myglobal++;
+  __goblint_check(myglobal == 6);
+  myglobal--;
+  __goblint_check(myglobal == 5);
+}
+
+void *t_fun(void *arg) {
+  __VERIFIER_atomic_fun();
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  __goblint_check(myglobal == 5);
+  __VERIFIER_atomic_begin();
+  __goblint_check(myglobal == 5);
+  __VERIFIER_atomic_end();
+  pthread_join (id, NULL);
+  return 0;
+}
diff --git a/tests/regression/46-apron2/60-atomic_priv_sound.c b/tests/regression/46-apron2/60-atomic_priv_sound.c
new file mode 100644
index 0000000000..79103337c7
--- /dev/null
+++ b/tests/regression/46-apron2/60-atomic_priv_sound.c
@@ -0,0 +1,28 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.base.privatization none
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int myglobal = 5;
+
+void *t_fun(void *arg) {
+  __VERIFIER_atomic_begin();
+  __goblint_check(myglobal == 5); // TODO
+  myglobal++;
+  __goblint_check(myglobal == 6); // TODO
+  __VERIFIER_atomic_end();
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  __goblint_check(myglobal == 5); // UNKNOWN!
+  __VERIFIER_atomic_begin();
+  __goblint_check(myglobal == 5); // UNKNOWN!
+  __VERIFIER_atomic_end();
+  pthread_join (id, NULL);
+  return 0;
+}
diff --git a/tests/regression/46-apron2/61-atomic_priv_sound2.c b/tests/regression/46-apron2/61-atomic_priv_sound2.c
new file mode 100644
index 0000000000..c9ecb90a1e
--- /dev/null
+++ b/tests/regression/46-apron2/61-atomic_priv_sound2.c
@@ -0,0 +1,43 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.base.privatization none
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int myglobal = 0;
+int myglobal2 = 0;
+int myglobal3 = 0;
+
+void *t_fun(void *arg) {
+  __VERIFIER_atomic_begin();
+  myglobal2++;
+  __VERIFIER_atomic_end();
+  __VERIFIER_atomic_begin();
+  myglobal++;
+  __VERIFIER_atomic_end();
+  return NULL;
+}
+
+void *t2_fun(void *arg) {
+  __VERIFIER_atomic_begin();
+  myglobal3++;
+  __VERIFIER_atomic_end();
+  __VERIFIER_atomic_begin();
+  myglobal++;
+  __VERIFIER_atomic_end();
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id, id2;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_create(&id2, NULL, t2_fun, NULL);
+  __goblint_check(myglobal == 2); // UNKNOWN!
+  __VERIFIER_atomic_begin();
+  __goblint_check(myglobal == 2); // UNKNOWN!
+  __VERIFIER_atomic_end();
+  pthread_join (id, NULL);
+  pthread_join (id2, NULL);
+  return 0;
+}
diff --git a/tests/regression/46-apron2/62-atomic_priv_sound3.c b/tests/regression/46-apron2/62-atomic_priv_sound3.c
new file mode 100644
index 0000000000..7967507b65
--- /dev/null
+++ b/tests/regression/46-apron2/62-atomic_priv_sound3.c
@@ -0,0 +1,23 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.base.privatization none
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int myglobal = 5;
+
+void *t_fun(void *arg) {
+  myglobal++;
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  __VERIFIER_atomic_begin();
+  __goblint_check(myglobal == 5); // UNKNOWN!
+  __VERIFIER_atomic_end();
+  pthread_join (id, NULL);
+  return 0;
+}

From a5f4bff22323ddd8ce0a39f6cdc0621f445f8d32 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 13 Oct 2023 15:10:21 +0300
Subject: [PATCH 03/34] Use relational unprotected invariant for mutex-meet

---
 src/analyses/apron/relationPriv.apron.ml      | 39 ++++++++++++++-----
 .../regression/46-apron2/63-atomic_relation.c | 33 ++++++++++++++++
 2 files changed, 62 insertions(+), 10 deletions(-)
 create mode 100644 tests/regression/46-apron2/63-atomic_relation.c

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index abdbb2f791..0584333365 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -470,6 +470,8 @@ struct
 
   let startstate () = ()
 
+  let atomic_mutex = LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var
+
   let get_m_with_mutex_inits ask getg m =
     let get_m = getg (V.mutex m) in
     let get_mutex_inits = getg V.mutex_inits in
@@ -477,11 +479,17 @@ struct
     RD.join get_m get_mutex_inits'
 
   let get_mutex_global_g_with_mutex_inits ask getg g =
-    let get_mutex_global_g = getg (V.global g) in
+    let get_mutex_global_g = getg (V.mutex atomic_mutex) in
     let get_mutex_inits = getg V.mutex_inits in
     let g_var = AV.global g in
+    let get_mutex_global_g' = RD.keep_vars get_mutex_global_g [g_var] in
     let get_mutex_inits' = RD.keep_vars get_mutex_inits [g_var] in
-    RD.join get_mutex_global_g get_mutex_inits'
+    RD.join get_mutex_global_g' get_mutex_inits'
+
+  let get_mutex_global_g_with_mutex_inits' ask getg =
+    let get_mutex_global_g = getg (V.mutex atomic_mutex) in
+    let get_mutex_inits = getg V.mutex_inits in
+    RD.join get_mutex_global_g get_mutex_inits
 
   let read_global (ask: Q.ask) getg (st: relation_components_t) g x: RD.t =
     let atomic = ask.f MustBeAtomic in
@@ -490,6 +498,8 @@ struct
     let rel =
       if atomic && RD.mem_var rel (AV.global g) then
         rel
+      else if atomic then
+        RD.meet rel (get_mutex_global_g_with_mutex_inits' ask getg)
       else
         RD.meet rel (get_mutex_global_g_with_mutex_inits ask getg g)
     in
@@ -518,6 +528,8 @@ struct
     let rel =
       if atomic && RD.mem_var rel (AV.global g) then
         rel
+      else if atomic then
+        RD.meet rel (get_mutex_global_g_with_mutex_inits' ask getg)
       else
         RD.meet rel (get_mutex_global_g_with_mutex_inits ask getg g)
     in
@@ -527,9 +539,9 @@ struct
     let rel_local = RD.add_vars rel [g_var] in
     let rel_local = RD.assign_var rel_local g_var x_var in
     (* unlock *)
-    if not (ask.f MustBeAtomic) then (
-    let rel_side = RD.keep_vars rel_local [g_var] in
-      sideg (V.global g) rel_side;
+    if not atomic then (
+      let rel_side = RD.keep_vars rel_local [g_var] in
+      sideg (V.mutex atomic_mutex) rel_side;
       let rel_local' =
         if is_unprotected ask g then
           RD.remove_vars rel_local [g_var]
@@ -543,7 +555,7 @@ struct
 
 
   let lock ask getg (st: relation_components_t) m =
-    let atomic = LockDomain.Addr.equal m (LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var) in
+    let atomic = LockDomain.Addr.equal m (atomic_mutex) in
     (* TODO: somehow actually unneeded here? *)
     if not atomic && Locksets.(not (Lockset.mem m (current_lockset ask))) then (
       let rel = st.rel in
@@ -557,7 +569,7 @@ struct
       st (* sound w.r.t. recursive lock *)
 
   let unlock ask getg sideg (st: relation_components_t) m: relation_components_t =
-    let atomic = LockDomain.Addr.equal m (LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var) in
+    let atomic = LockDomain.Addr.equal m (atomic_mutex) in
     let rel = st.rel in
     if not atomic then (
       let rel_side = keep_only_protected_globals ask m rel in
@@ -566,11 +578,18 @@ struct
       {st with rel = rel_local}
     )
     else (
-      List.iter (fun var ->
+      (* List.iter (fun var ->
           match AV.find_metadata var with
-          | Some (Global g) -> sideg (V.global g) (RD.keep_vars rel [AV.global g])
+          | Some (Global g) -> sideg (V.mutex atomic_mutex) (RD.keep_vars rel [AV.global g])
           | _ -> ()
-        ) (RD.vars rel);
+        ) (RD.vars rel); *)
+      let rel_side = RD.keep_filter rel (fun var ->
+          match AV.find_metadata var with
+          | Some (Global g) -> true
+          | _ -> false
+        )
+      in
+      sideg (V.mutex atomic_mutex) rel_side;
       let rel_local =
         let newly_unprot var = match AV.find_metadata var with
           | Some (Global g) -> is_unprotected ask g
diff --git a/tests/regression/46-apron2/63-atomic_relation.c b/tests/regression/46-apron2/63-atomic_relation.c
new file mode 100644
index 0000000000..7c72c9d723
--- /dev/null
+++ b/tests/regression/46-apron2/63-atomic_relation.c
@@ -0,0 +1,33 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int g = 0;
+int h = 0;
+
+pthread_mutex_t m = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  __VERIFIER_atomic_begin();
+  // pthread_mutex_lock(&m);
+  g++;
+  h++;
+  __VERIFIER_atomic_end();
+  // pthread_mutex_unlock(&m);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  __VERIFIER_atomic_begin();
+  // pthread_mutex_lock(&m);
+  __goblint_check(g == h);
+  __VERIFIER_atomic_end(); // TODO: remove g, h from local state; currently remain because protected by __VERIFIER_atomic
+  // pthread_mutex_unlock(&m);
+  pthread_join (id, NULL);
+  return 0;
+}

From f8468941ffb6535880ffc54783dc745069a0e9bb Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 13 Oct 2023 17:17:46 +0300
Subject: [PATCH 04/34] Fix relational mutex-meet atomic unlock

---
 src/analyses/apron/relationPriv.apron.ml        | 2 +-
 tests/regression/46-apron2/63-atomic_relation.c | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index 0584333365..7efca6ac04 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -592,7 +592,7 @@ struct
       sideg (V.mutex atomic_mutex) rel_side;
       let rel_local =
         let newly_unprot var = match AV.find_metadata var with
-          | Some (Global g) -> is_unprotected ask g
+          | Some (Global g) -> is_unprotected_without ask g atomic_mutex
           | _ -> false
         in
         RD.remove_filter rel newly_unprot
diff --git a/tests/regression/46-apron2/63-atomic_relation.c b/tests/regression/46-apron2/63-atomic_relation.c
index 7c72c9d723..4169b1e447 100644
--- a/tests/regression/46-apron2/63-atomic_relation.c
+++ b/tests/regression/46-apron2/63-atomic_relation.c
@@ -26,7 +26,7 @@ int main(void) {
   __VERIFIER_atomic_begin();
   // pthread_mutex_lock(&m);
   __goblint_check(g == h);
-  __VERIFIER_atomic_end(); // TODO: remove g, h from local state; currently remain because protected by __VERIFIER_atomic
+  __VERIFIER_atomic_end();
   // pthread_mutex_unlock(&m);
   pthread_join (id, NULL);
   return 0;

From f27b0983fbb667528c3939da5d5299350b11c286 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 13 Oct 2023 17:28:53 +0300
Subject: [PATCH 05/34] Add Freiburg case_distinction_with_ghosts example

---
 .../64-case_distinction_with_ghosts.c         | 39 +++++++++++++++++++
 1 file changed, 39 insertions(+)
 create mode 100644 tests/regression/46-apron2/64-case_distinction_with_ghosts.c

diff --git a/tests/regression/46-apron2/64-case_distinction_with_ghosts.c b/tests/regression/46-apron2/64-case_distinction_with_ghosts.c
new file mode 100644
index 0000000000..06df245afd
--- /dev/null
+++ b/tests/regression/46-apron2/64-case_distinction_with_ghosts.c
@@ -0,0 +1,39 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+#include <pthread.h>
+#include <assert.h>
+
+extern int  __VERIFIER_nondet_int();
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int x = 0;
+int g = 0;
+
+void* inc()
+{
+  int n = __VERIFIER_nondet_int();
+
+  while (x < n) {
+    __VERIFIER_atomic_begin();
+    x++;
+    __VERIFIER_atomic_end();
+
+    __VERIFIER_atomic_begin();
+    assert(g != 1 || x >= 42);
+    __VERIFIER_atomic_end();
+  }
+
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+  pthread_create(&tid, 0, inc, 0);
+  __VERIFIER_atomic_begin();
+  g = 1; x = 42;
+  __VERIFIER_atomic_end();
+
+  assert(x >= 42);
+  return 0;
+}

From 4e7312b45d3b0956db71756a5d5e45d5bb22ccfd Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 13 Oct 2023 17:40:47 +0300
Subject: [PATCH 06/34] Add simpler case_distinction tests

---
 .../64-case_distinction_with_ghosts.c         |  4 +--
 .../65-case_distinction_with_ghosts-2.c       | 30 +++++++++++++++++++
 .../66-case_distinction_with_ghosts-3.c       | 30 +++++++++++++++++++
 3 files changed, 62 insertions(+), 2 deletions(-)
 create mode 100644 tests/regression/46-apron2/65-case_distinction_with_ghosts-2.c
 create mode 100644 tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c

diff --git a/tests/regression/46-apron2/64-case_distinction_with_ghosts.c b/tests/regression/46-apron2/64-case_distinction_with_ghosts.c
index 06df245afd..633c1192c9 100644
--- a/tests/regression/46-apron2/64-case_distinction_with_ghosts.c
+++ b/tests/regression/46-apron2/64-case_distinction_with_ghosts.c
@@ -19,7 +19,7 @@ void* inc()
     __VERIFIER_atomic_end();
 
     __VERIFIER_atomic_begin();
-    assert(g != 1 || x >= 42);
+    assert(g != 1 || x >= 42); // TODO
     __VERIFIER_atomic_end();
   }
 
@@ -34,6 +34,6 @@ int main()
   g = 1; x = 42;
   __VERIFIER_atomic_end();
 
-  assert(x >= 42);
+  assert(x >= 42); // TODO
   return 0;
 }
diff --git a/tests/regression/46-apron2/65-case_distinction_with_ghosts-2.c b/tests/regression/46-apron2/65-case_distinction_with_ghosts-2.c
new file mode 100644
index 0000000000..89371e74fa
--- /dev/null
+++ b/tests/regression/46-apron2/65-case_distinction_with_ghosts-2.c
@@ -0,0 +1,30 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+#include <pthread.h>
+#include <assert.h>
+
+extern int  __VERIFIER_nondet_int();
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int x = 0;
+int g = 0;
+
+void* inc()
+{
+  __VERIFIER_atomic_begin();
+  assert(g != 1 || x >= 42); // TODO
+  __VERIFIER_atomic_end();
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+  pthread_create(&tid, 0, inc, 0);
+  __VERIFIER_atomic_begin();
+  g = 1; x = 42;
+  __VERIFIER_atomic_end();
+
+  assert(x >= 42); // TODO
+  return 0;
+}
diff --git a/tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c b/tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c
new file mode 100644
index 0000000000..6fc2700299
--- /dev/null
+++ b/tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c
@@ -0,0 +1,30 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+#include <pthread.h>
+#include <assert.h>
+
+extern int  __VERIFIER_nondet_int();
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int x = 0;
+int g = 0;
+
+void* inc()
+{
+  // x = 10; // TODO: what is this?
+
+  __VERIFIER_atomic_begin();
+  assert(g != 1 || x >= 42); // TODO
+  __VERIFIER_atomic_end();
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+  pthread_create(&tid, 0, inc, 0);
+  __VERIFIER_atomic_begin();
+  g = 1; x = 42;
+  __VERIFIER_atomic_end();
+  return 0;
+}

From 4c541403006dfd48311435362e2707e42262e608 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 20 Oct 2023 11:56:56 +0300
Subject: [PATCH 07/34] Add Freiburg nondet_inc_with_ghosts examples

---
 .../46-apron2/67-nondet_inc_with_ghosts.c     | 43 +++++++++++++++++++
 .../46-apron2/68-nondet_inc_with_ghosts-2.c   | 38 ++++++++++++++++
 .../46-apron2/69-nondet_inc_with_ghosts-3.c   | 34 +++++++++++++++
 3 files changed, 115 insertions(+)
 create mode 100644 tests/regression/46-apron2/67-nondet_inc_with_ghosts.c
 create mode 100644 tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c
 create mode 100644 tests/regression/46-apron2/69-nondet_inc_with_ghosts-3.c

diff --git a/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c b/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c
new file mode 100644
index 0000000000..cfbab7f922
--- /dev/null
+++ b/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c
@@ -0,0 +1,43 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+#include <pthread.h>
+#include <assert.h>
+
+extern int  __VERIFIER_nondet_int();
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int x = 0;
+int g = 0;
+
+void* inc()
+{
+  int n = __VERIFIER_nondet_int();
+
+  while (x < n) {
+    __VERIFIER_atomic_begin();
+    x++;
+    __VERIFIER_atomic_end();
+
+    __VERIFIER_atomic_begin();
+    assert(x >= g); // TODO
+    __VERIFIER_atomic_end();
+  }
+
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+  pthread_create(&tid, 0, inc, 0);
+
+  int val = __VERIFIER_nondet_int();
+  __VERIFIER_atomic_begin();
+  g = val; x = val;
+  __VERIFIER_atomic_end();
+
+  __VERIFIER_atomic_begin(); // TODO: atomic needed?
+  assert(x >= val); // TODO
+  __VERIFIER_atomic_end();
+  return 0;
+}
diff --git a/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c b/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c
new file mode 100644
index 0000000000..3d41428a59
--- /dev/null
+++ b/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c
@@ -0,0 +1,38 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+#include <pthread.h>
+#include <assert.h>
+
+extern int  __VERIFIER_nondet_int();
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int x = 0;
+int g = 0;
+
+void* inc()
+{
+  __VERIFIER_atomic_begin();
+  x++;
+  __VERIFIER_atomic_end();
+
+  __VERIFIER_atomic_begin();
+  assert(x >= g); // TODO
+  __VERIFIER_atomic_end();
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+  pthread_create(&tid, 0, inc, 0);
+
+  int val = __VERIFIER_nondet_int();
+  __VERIFIER_atomic_begin();
+  g = val; x = val;
+  __VERIFIER_atomic_end();
+
+  __VERIFIER_atomic_begin(); // TODO: atomic needed?
+  assert(x >= val); // TODO
+  __VERIFIER_atomic_end();
+  return 0;
+}
diff --git a/tests/regression/46-apron2/69-nondet_inc_with_ghosts-3.c b/tests/regression/46-apron2/69-nondet_inc_with_ghosts-3.c
new file mode 100644
index 0000000000..0519dbda00
--- /dev/null
+++ b/tests/regression/46-apron2/69-nondet_inc_with_ghosts-3.c
@@ -0,0 +1,34 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+#include <pthread.h>
+#include <assert.h>
+
+extern int  __VERIFIER_nondet_int();
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int x = 0;
+int g = 0;
+
+void* inc()
+{
+  __VERIFIER_atomic_begin();
+  assert(x >= g);
+  __VERIFIER_atomic_end();
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+  pthread_create(&tid, 0, inc, 0);
+
+  int val = __VERIFIER_nondet_int();
+  __VERIFIER_atomic_begin();
+  g = val; x = val;
+  __VERIFIER_atomic_end();
+
+  __VERIFIER_atomic_begin(); // TODO: atomic needed?
+  assert(x >= val); // TODO
+  __VERIFIER_atomic_end();
+  return 0;
+}

From e1e0813d0b9f4dcd214ef0dcd9ef1815854dc1e1 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 20 Oct 2023 12:07:29 +0300
Subject: [PATCH 08/34] Use threshold widening in Freiburg
 nondet_inc_with_ghosts

---
 tests/regression/46-apron2/67-nondet_inc_with_ghosts.c   | 4 ++--
 tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c b/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c
index cfbab7f922..2fc073db05 100644
--- a/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c
+++ b/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none --enable ana.apron.threshold_widening
 #include <pthread.h>
 #include <assert.h>
 
@@ -19,7 +19,7 @@ void* inc()
     __VERIFIER_atomic_end();
 
     __VERIFIER_atomic_begin();
-    assert(x >= g); // TODO
+    assert(x >= g);
     __VERIFIER_atomic_end();
   }
 
diff --git a/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c b/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c
index 3d41428a59..380821add9 100644
--- a/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c
+++ b/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none --enable ana.apron.threshold_widening
 #include <pthread.h>
 #include <assert.h>
 
@@ -16,7 +16,7 @@ void* inc()
   __VERIFIER_atomic_end();
 
   __VERIFIER_atomic_begin();
-  assert(x >= g); // TODO
+  assert(x >= g);
   __VERIFIER_atomic_end();
   return 0;
 }

From bd533c0ea0f1724796fe9c539d92e7883a77a5ef Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 20 Oct 2023 18:18:30 +0300
Subject: [PATCH 09/34] Use relational unprotected invariant for mutex-meet-tid

---
 src/analyses/apron/relationPriv.apron.ml | 129 +++++++++++++++++------
 1 file changed, 94 insertions(+), 35 deletions(-)

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index 7efca6ac04..da7d4a1a3d 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -950,8 +950,10 @@ struct
     if M.tracing then M.traceu "relationpriv" "-> %a\n" LRD.pretty r;
     r
 
+  let atomic_mutex = LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var
+
   let get_mutex_global_g_with_mutex_inits inits ask getg g =
-    let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.global g) in
+    let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.mutex atomic_mutex) in
     if M.tracing then M.traceli "relationpriv" "get_mutex_global_g_with_mutex_inits %a\n  get=%a\n" CilType.Varinfo.pretty g LRD.pretty get_mutex_global_g;
     let r =
       if not inits then
@@ -965,60 +967,95 @@ struct
     if M.tracing then M.traceu "relationpriv" "-> %a\n" LRD.pretty r;
     r
 
-  let read_global ask getg (st: relation_components_t) g x: RD.t =
+  let get_mutex_global_g_with_mutex_inits' inits ask getg =
+    let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.mutex atomic_mutex) in
+    if not inits then
+      get_mutex_global_g
+    else
+      let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
+      LRD.join get_mutex_global_g get_mutex_inits
+
+  let read_global (ask: Q.ask) getg (st: relation_components_t) g x: RD.t =
+    let atomic = ask.f MustBeAtomic in
     let _,lmust,l = st.priv in
     let rel = st.rel in
     let lm = LLock.global g in
     (* lock *)
-    let tmp = get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g in
     let local_m = BatOption.default (LRD.bot ()) (L.find_opt lm l) in
     (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
-    let rel = Cluster.lock rel local_m tmp in
+    let rel =
+      if atomic && RD.mem_var rel (AV.global g) then
+        rel
+      else if atomic then
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits' (not (LMust.mem lm lmust)) ask getg)
+      else
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g)
+    in
     (* read *)
     let g_var = AV.global g in
     let x_var = AV.local x in
     let rel_local = RD.add_vars rel [g_var] in
     let rel_local = RD.assign_var rel_local x_var g_var in
     (* unlock *)
-    let rel_local' =
-      if is_unprotected ask g then
-        RD.remove_vars rel_local [g_var]
-      else
-        rel_local
-    in
-    rel_local'
+    if not atomic then (
+      let rel_local' =
+        if is_unprotected ask g then
+          RD.remove_vars rel_local [g_var]
+        else
+          rel_local
+      in
+      rel_local'
+    )
+    else
+      rel_local
 
   let write_global ?(invariant=false) (ask:Q.ask) getg sideg (st: relation_components_t) g x: relation_components_t =
+    let atomic = ask.f MustBeAtomic in
     let w,lmust,l = st.priv in
     let lm = LLock.global g in
     let rel = st.rel in
     (* lock *)
-    let tmp = get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g in
     let local_m = BatOption.default (LRD.bot ()) (L.find_opt lm l) in
     (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
-    let rel = Cluster.lock rel local_m tmp in
+    let rel =
+      if atomic && RD.mem_var rel (AV.global g) then
+        rel
+      else if atomic then
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits' (not (LMust.mem lm lmust)) ask getg)
+      else
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g)
+    in
     (* write *)
     let g_var = AV.global g in
     let x_var = AV.local x in
     let rel_local = RD.add_vars rel [g_var] in
     let rel_local = RD.assign_var rel_local g_var x_var in
     (* unlock *)
-    let rel_side = RD.keep_vars rel_local [g_var] in
-    let rel_side = Cluster.unlock (W.singleton g) rel_side in
-    let tid = ThreadId.get_current ask in
-    let sidev = GMutex.singleton tid rel_side in
-    sideg (V.global g) (G.create_global sidev);
-    let l' = L.add lm rel_side l in
-    let rel_local' =
-      if is_unprotected ask g then
-        RD.remove_vars rel_local [g_var]
-      else
-        rel_local
-    in
-    {rel = rel_local'; priv = (W.add g w,LMust.add lm lmust,l')}
+    if not atomic then (
+      let rel_side = RD.keep_vars rel_local [g_var] in
+      let rel_side = Cluster.unlock (W.singleton g) rel_side in
+      let tid = ThreadId.get_current ask in
+      let sidev = GMutex.singleton tid rel_side in
+      sideg (V.mutex atomic_mutex) (G.create_global sidev);
+      let l' = L.add lm rel_side l in
+      let rel_local' =
+        if is_unprotected ask g then
+          RD.remove_vars rel_local [g_var]
+        else
+          rel_local
+      in
+      {rel = rel_local'; priv = (W.add g w,LMust.add lm lmust,l')}
+    )
+    else (
+      (* let rel_side = RD.keep_vars rel_local [g_var] in
+      let rel_side = Cluster.unlock (W.singleton g) rel_side in
+      let l' = L.add lm rel_side l in *)
+      {rel = rel_local; priv = (W.add g w,LMust.add lm lmust,l)}
+    )
 
   let lock ask getg (st: relation_components_t) m =
-    if Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+    let atomic = LockDomain.Addr.equal m (atomic_mutex) in
+    if not atomic && Locksets.(not (Lockset.mem m (current_lockset ask))) then (
       let rel = st.rel in
       let _,lmust,l = st.priv in
       let lm = LLock.mutex m in
@@ -1032,23 +1069,45 @@ struct
     else
       st (* sound w.r.t. recursive lock *)
 
+  let keep_only_globals ask m oct =
+    let protected var = match AV.find_metadata var with
+      | Some (Global g) -> true
+      | _ -> false
+    in
+    RD.keep_filter oct protected
+
   let unlock ask getg sideg (st: relation_components_t) m: relation_components_t =
+    let atomic = LockDomain.Addr.equal m (atomic_mutex) in
     let rel = st.rel in
     let w,lmust,l = st.priv in
-    let rel_local = remove_globals_unprotected_after_unlock ask m rel in
-    let w' = W.filter (fun v -> not (is_unprotected_without ask v m)) w in
-    let side_needed = W.exists (fun v -> is_protected_by ask m v) w in
-    if not side_needed then
-      {rel = rel_local; priv = (w',lmust,l)}
-    else
-      let rel_side = keep_only_protected_globals ask m rel in
+    if not atomic then (
+      let rel_local = remove_globals_unprotected_after_unlock ask m rel in
+      let w' = W.filter (fun v -> not (is_unprotected_without ask v m)) w in
+      let side_needed = W.exists (fun v -> is_protected_by ask m v) w in
+      if not side_needed then
+        {rel = rel_local; priv = (w',lmust,l)}
+      else
+        let rel_side = keep_only_protected_globals ask m rel in
+        let rel_side = Cluster.unlock w rel_side in
+        let tid = ThreadId.get_current ask in
+        let sidev = GMutex.singleton tid rel_side in
+        sideg (V.mutex m) (G.create_mutex sidev);
+        let lm = LLock.mutex m in
+        let l' = L.add lm rel_side l in
+        {rel = rel_local; priv = (w',LMust.add lm lmust,l')}
+    )
+    else (
+      let rel_local = remove_globals_unprotected_after_unlock ask m rel in
+      let w' = W.filter (fun v -> not (is_unprotected_without ask v m)) w in
+      let rel_side = keep_only_globals ask m rel in
       let rel_side = Cluster.unlock w rel_side in
       let tid = ThreadId.get_current ask in
       let sidev = GMutex.singleton tid rel_side in
-      sideg (V.mutex m) (G.create_mutex sidev);
+      sideg (V.mutex atomic_mutex) (G.create_mutex sidev);
       let lm = LLock.mutex m in
       let l' = L.add lm rel_side l in
       {rel = rel_local; priv = (w',LMust.add lm lmust,l')}
+    )
 
   let thread_join ?(force=false) (ask:Q.ask) getg exp (st: relation_components_t) =
     let w,lmust,l = st.priv in

From fa1f6fac2e7ef7dce797bc10de8794dcd4d2e775 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 27 Nov 2023 17:15:33 +0200
Subject: [PATCH 10/34] Use strengthening in 36-apron/98-loc

---
 tests/regression/36-apron/98-loc.c | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tests/regression/36-apron/98-loc.c b/tests/regression/36-apron/98-loc.c
index 28be43a096..f9721fb579 100644
--- a/tests/regression/36-apron/98-loc.c
+++ b/tests/regression/36-apron/98-loc.c
@@ -1,4 +1,5 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --set ana.relation.privatization mutex-meet-tid --enable ana.thread.include-node
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --set ana.relation.privatization mutex-meet-tid --enable ana.thread.include-node --enable ana.apron.strengthening
+// strengthening needed with relational unprotected invariant in mutex-meet-tid
 #include <pthread.h>
 #include <goblint.h>
 

From 21a4a98faacab7061f680926195b0d60bf7459ba Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 28 Nov 2023 12:48:09 +0200
Subject: [PATCH 11/34] Try to make two Mukerjee tests more precise with
 strengthening

---
 tests/regression/52-apron-mukherjee/02-mukherjee_sigma.c  | 2 +-
 tests/regression/52-apron-mukherjee/18-mukherjee_qw2004.c | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/regression/52-apron-mukherjee/02-mukherjee_sigma.c b/tests/regression/52-apron-mukherjee/02-mukherjee_sigma.c
index 333dc64c48..c42f4e42cd 100644
--- a/tests/regression/52-apron-mukherjee/02-mukherjee_sigma.c
+++ b/tests/regression/52-apron-mukherjee/02-mukherjee_sigma.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --set ana.relation.privatization mutex-meet-tid
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --set ana.relation.privatization mutex-meet-tid --enable ana.apron.strengthening
 
 #include <stdlib.h>
 #include <pthread.h>
diff --git a/tests/regression/52-apron-mukherjee/18-mukherjee_qw2004.c b/tests/regression/52-apron-mukherjee/18-mukherjee_qw2004.c
index 9f3f94beb1..09d2a1177f 100644
--- a/tests/regression/52-apron-mukherjee/18-mukherjee_qw2004.c
+++ b/tests/regression/52-apron-mukherjee/18-mukherjee_qw2004.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --enable ana.apron.threshold_widening --set ana.relation.privatization mutex-meet-tid
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --enable ana.apron.threshold_widening --set ana.relation.privatization mutex-meet-tid --enable ana.apron.strengthening
 
 #include <pthread.h>
 #include <goblint.h>

From b3af7989b45b31e8fc6cd85c77a8d0a3b5a7fbdb Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 28 Nov 2023 12:48:29 +0200
Subject: [PATCH 12/34] Fix unsoundness in per-mutex-tid which is revealed by
 strengthening

---
 src/analyses/apron/relationPriv.apron.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index da7d4a1a3d..5a5dffc606 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -954,6 +954,7 @@ struct
 
   let get_mutex_global_g_with_mutex_inits inits ask getg g =
     let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.mutex atomic_mutex) in
+    let get_mutex_global_g = Cluster.keep_global g get_mutex_global_g in
     if M.tracing then M.traceli "relationpriv" "get_mutex_global_g_with_mutex_inits %a\n  get=%a\n" CilType.Varinfo.pretty g LRD.pretty get_mutex_global_g;
     let r =
       if not inits then

From f2b2a3929178ef09f5c1170c2e9b47b9aac6945f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 29 Nov 2023 14:36:30 +0200
Subject: [PATCH 13/34] Split relational mutex-meet-tid unprotected invariant
 by global

---
 src/analyses/apron/relationPriv.apron.ml | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index 5a5dffc606..c96642ffdd 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -953,7 +953,7 @@ struct
   let atomic_mutex = LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var
 
   let get_mutex_global_g_with_mutex_inits inits ask getg g =
-    let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.mutex atomic_mutex) in
+    let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.global g) in
     let get_mutex_global_g = Cluster.keep_global g get_mutex_global_g in
     if M.tracing then M.traceli "relationpriv" "get_mutex_global_g_with_mutex_inits %a\n  get=%a\n" CilType.Varinfo.pretty g LRD.pretty get_mutex_global_g;
     let r =
@@ -968,8 +968,8 @@ struct
     if M.tracing then M.traceu "relationpriv" "-> %a\n" LRD.pretty r;
     r
 
-  let get_mutex_global_g_with_mutex_inits' inits ask getg =
-    let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.mutex atomic_mutex) in
+  let get_mutex_global_g_with_mutex_inits' inits ask getg g =
+    let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.global g) in
     if not inits then
       get_mutex_global_g
     else
@@ -988,7 +988,7 @@ struct
       if atomic && RD.mem_var rel (AV.global g) then
         rel
       else if atomic then
-        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits' (not (LMust.mem lm lmust)) ask getg)
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits' (not (LMust.mem lm lmust)) ask getg g)
       else
         Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g)
     in
@@ -1022,7 +1022,7 @@ struct
       if atomic && RD.mem_var rel (AV.global g) then
         rel
       else if atomic then
-        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits' (not (LMust.mem lm lmust)) ask getg)
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits' (not (LMust.mem lm lmust)) ask getg g)
       else
         Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g)
     in
@@ -1037,7 +1037,7 @@ struct
       let rel_side = Cluster.unlock (W.singleton g) rel_side in
       let tid = ThreadId.get_current ask in
       let sidev = GMutex.singleton tid rel_side in
-      sideg (V.mutex atomic_mutex) (G.create_global sidev);
+      sideg (V.global g) (G.create_global sidev);
       let l' = L.add lm rel_side l in
       let rel_local' =
         if is_unprotected ask g then
@@ -1104,7 +1104,9 @@ struct
       let rel_side = Cluster.unlock w rel_side in
       let tid = ThreadId.get_current ask in
       let sidev = GMutex.singleton tid rel_side in
-      sideg (V.mutex atomic_mutex) (G.create_mutex sidev);
+      W.iter (fun g ->
+          sideg (V.global g) (G.create_mutex sidev)
+        ) w;
       let lm = LLock.mutex m in
       let l' = L.add lm rel_side l in
       {rel = rel_local; priv = (w',LMust.add lm lmust,l')}

From e4c575b3073bdb642d230b650129c73a06c78bf8 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 29 Nov 2023 14:36:38 +0200
Subject: [PATCH 14/34] Revert "Use strengthening in 36-apron/98-loc"

This reverts commit fa1f6fac2e7ef7dce797bc10de8794dcd4d2e775.
---
 tests/regression/36-apron/98-loc.c | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/tests/regression/36-apron/98-loc.c b/tests/regression/36-apron/98-loc.c
index f9721fb579..28be43a096 100644
--- a/tests/regression/36-apron/98-loc.c
+++ b/tests/regression/36-apron/98-loc.c
@@ -1,5 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --set ana.relation.privatization mutex-meet-tid --enable ana.thread.include-node --enable ana.apron.strengthening
-// strengthening needed with relational unprotected invariant in mutex-meet-tid
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --set ana.relation.privatization mutex-meet-tid --enable ana.thread.include-node
 #include <pthread.h>
 #include <goblint.h>
 

From a3f531b643f6c6c393b4319d39038e6b50fd7724 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 29 Nov 2023 14:37:03 +0200
Subject: [PATCH 15/34] Revert "Try to make two Mukerjee tests more precise
 with strengthening"

This reverts commit 21a4a98faacab7061f680926195b0d60bf7459ba.
---
 tests/regression/52-apron-mukherjee/02-mukherjee_sigma.c  | 2 +-
 tests/regression/52-apron-mukherjee/18-mukherjee_qw2004.c | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/regression/52-apron-mukherjee/02-mukherjee_sigma.c b/tests/regression/52-apron-mukherjee/02-mukherjee_sigma.c
index c42f4e42cd..333dc64c48 100644
--- a/tests/regression/52-apron-mukherjee/02-mukherjee_sigma.c
+++ b/tests/regression/52-apron-mukherjee/02-mukherjee_sigma.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --set ana.relation.privatization mutex-meet-tid --enable ana.apron.strengthening
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --set ana.relation.privatization mutex-meet-tid
 
 #include <stdlib.h>
 #include <pthread.h>
diff --git a/tests/regression/52-apron-mukherjee/18-mukherjee_qw2004.c b/tests/regression/52-apron-mukherjee/18-mukherjee_qw2004.c
index 09d2a1177f..9f3f94beb1 100644
--- a/tests/regression/52-apron-mukherjee/18-mukherjee_qw2004.c
+++ b/tests/regression/52-apron-mukherjee/18-mukherjee_qw2004.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --enable ana.apron.threshold_widening --set ana.relation.privatization mutex-meet-tid --enable ana.apron.strengthening
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --enable ana.apron.threshold_widening --set ana.relation.privatization mutex-meet-tid
 
 #include <pthread.h>
 #include <goblint.h>

From 73c06902398facb3be473d3cfad1634e4cf3e5db Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 29 Nov 2023 15:56:35 +0200
Subject: [PATCH 16/34] Add missing relationpriv tracing

---
 src/analyses/apron/relationPriv.apron.ml | 44 ++++++++++++++++++++++++
 1 file changed, 44 insertions(+)

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index c96642ffdd..d036353990 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -1318,6 +1318,50 @@ struct
     let r = sync ask getg sideg st reason in
     if M.tracing then M.traceu "relationpriv" "-> %a\n" RelComponents.pretty r;
     r
+
+  let escape node ask getg sideg st vs =
+    if M.tracing then M.traceli "relationpriv" "escape\n";
+    if M.tracing then M.trace "relationpriv" "st: %a\n" RelComponents.pretty st;
+    let getg x =
+      let r = getg x in
+      if M.tracing then M.trace "relationpriv" "getg %a -> %a\n" V.pretty x G.pretty r;
+      r
+    in
+    let sideg x v =
+      if M.tracing then M.trace "relationpriv" "sideg %a %a\n" V.pretty x G.pretty v;
+      sideg x v
+    in
+    let r = escape node ask getg sideg st vs in
+    if M.tracing then M.traceu "relationpriv" "-> %a\n" RelComponents.pretty r;
+    r
+
+  let thread_join ?force ask getg e st =
+    if M.tracing then M.traceli "relationpriv" "thread_join\n";
+    if M.tracing then M.trace "relationpriv" "st: %a\n" RelComponents.pretty st;
+    let getg x =
+      let r = getg x in
+      if M.tracing then M.trace "relationpriv" "getg %a -> %a\n" V.pretty x G.pretty r;
+      r
+    in
+    let r = thread_join ?force ask getg e st in
+    if M.tracing then M.traceu "relationpriv" "-> %a\n" RelComponents.pretty r;
+    r
+
+  let thread_return ask getg sideg tid st =
+    if M.tracing then M.traceli "relationpriv" "thread_return\n";
+    if M.tracing then M.trace "relationpriv" "st: %a\n" RelComponents.pretty st;
+    let getg x =
+      let r = getg x in
+      if M.tracing then M.trace "relationpriv" "getg %a -> %a\n" V.pretty x G.pretty r;
+      r
+    in
+    let sideg x v =
+      if M.tracing then M.trace "relationpriv" "sideg %a %a\n" V.pretty x G.pretty v;
+      sideg x v
+    in
+    let r = thread_return ask getg sideg tid st in
+    if M.tracing then M.traceu "relationpriv" "-> %a\n" RelComponents.pretty r;
+    r
 end
 
 

From 9680cc58c804796a7c050d61c8324e757d5161f8 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 29 Nov 2023 15:57:46 +0200
Subject: [PATCH 17/34] Fix relational mutex-meet-tid atomic unlock

Atomic mutex should not be added to L, but all written variables.
---
 src/analyses/apron/relationPriv.apron.ml | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index d036353990..7a8c7dd6a5 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -1051,7 +1051,7 @@ struct
       (* let rel_side = RD.keep_vars rel_local [g_var] in
       let rel_side = Cluster.unlock (W.singleton g) rel_side in
       let l' = L.add lm rel_side l in *)
-      {rel = rel_local; priv = (W.add g w,LMust.add lm lmust,l)}
+      {rel = rel_local; priv = (W.add g w,lmust,l)}
     )
 
   let lock ask getg (st: relation_components_t) m =
@@ -1104,12 +1104,13 @@ struct
       let rel_side = Cluster.unlock w rel_side in
       let tid = ThreadId.get_current ask in
       let sidev = GMutex.singleton tid rel_side in
-      W.iter (fun g ->
-          sideg (V.global g) (G.create_mutex sidev)
-        ) w;
-      let lm = LLock.mutex m in
-      let l' = L.add lm rel_side l in
-      {rel = rel_local; priv = (w',LMust.add lm lmust,l')}
+      let (lmust', l') = W.fold (fun g (lmust, l) ->
+          sideg (V.global g) (G.create_mutex sidev);
+          let lm = LLock.global g in
+          (LMust.add lm lmust, L.add lm rel_side l)
+        ) w (lmust, l)
+      in
+      {rel = rel_local; priv = (w',lmust',l')}
     )
 
   let thread_join ?(force=false) (ask:Q.ask) getg exp (st: relation_components_t) =

From 69dd7884a3a06130c8cfd2f7099ec990499911dd Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 29 Nov 2023 15:58:05 +0200
Subject: [PATCH 18/34] Add nondet_inc_with_ghosts with globalization

---
 .../70-nondet_inc_with_ghosts-globalize.c     | 49 +++++++++++++++++++
 1 file changed, 49 insertions(+)
 create mode 100644 tests/regression/46-apron2/70-nondet_inc_with_ghosts-globalize.c

diff --git a/tests/regression/46-apron2/70-nondet_inc_with_ghosts-globalize.c b/tests/regression/46-apron2/70-nondet_inc_with_ghosts-globalize.c
new file mode 100644
index 0000000000..8a52ffae32
--- /dev/null
+++ b/tests/regression/46-apron2/70-nondet_inc_with_ghosts-globalize.c
@@ -0,0 +1,49 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid --set sem.int.signed_overflow assume_none --enable ana.apron.threshold_widening --set ana.path_sens[+] threadflag --enable ana.apron.strengthening
+#include <pthread.h>
+#include <assert.h>
+
+extern int  __VERIFIER_nondet_int();
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int x = 0;
+int g = 0;
+
+void* inc()
+{
+  int n = __VERIFIER_nondet_int();
+
+  while (x < n) {
+    __VERIFIER_atomic_begin();
+    x++;
+    __VERIFIER_atomic_end();
+
+    __VERIFIER_atomic_begin();
+    assert(x >= g);
+    __VERIFIER_atomic_end();
+  }
+
+  return 0;
+}
+
+void* dummy()
+{
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+  pthread_create(&tid, 0, inc, 0);
+
+  int val = __VERIFIER_nondet_int();
+  __VERIFIER_atomic_begin();
+  pthread_create(&tid, 0, dummy, &val); // globalize val by escaping
+  g = val; x = val;
+  __VERIFIER_atomic_end();
+
+  __VERIFIER_atomic_begin(); // TODO: atomic needed?
+  assert(x >= val);
+  __VERIFIER_atomic_end();
+  return 0;
+}

From f47e5967890e6f92d7aa8cf6c071025615acb5ef Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 13 Dec 2023 13:09:39 +0200
Subject: [PATCH 19/34] Add mutex_with_ghosts Freiburg example with variants

---
 tests/regression/13-privatized/74-mutex.c     | 42 ++++++++++++
 tests/regression/46-apron2/71-mutex.c         | 42 ++++++++++++
 .../46-apron2/72-mutex_with_ghosts.c          | 65 ++++++++++++++++++
 .../46-apron2/73-mutex_with_ghosts-2.c        | 67 ++++++++++++++++++
 .../46-apron2/74-mutex_with_ghosts-3.c        | 68 +++++++++++++++++++
 5 files changed, 284 insertions(+)
 create mode 100644 tests/regression/13-privatized/74-mutex.c
 create mode 100644 tests/regression/46-apron2/71-mutex.c
 create mode 100644 tests/regression/46-apron2/72-mutex_with_ghosts.c
 create mode 100644 tests/regression/46-apron2/73-mutex_with_ghosts-2.c
 create mode 100644 tests/regression/46-apron2/74-mutex_with_ghosts-3.c

diff --git a/tests/regression/13-privatized/74-mutex.c b/tests/regression/13-privatized/74-mutex.c
new file mode 100644
index 0000000000..8ed9448b7b
--- /dev/null
+++ b/tests/regression/13-privatized/74-mutex.c
@@ -0,0 +1,42 @@
+// PARAM: --enable ana.sv-comp.functions
+/*-----------------------------------------------------------------------------
+ * mutex.c - Concurrent program using locking to access a shared variable
+ *-----------------------------------------------------------------------------
+ * Author: Frank Schüssele
+ *   Date: 2023-07-11
+ *---------------------------------------------------------------------------*/
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int used;
+pthread_mutex_t m;
+
+void* producer()
+{
+  while (1) {
+    pthread_mutex_lock(&m);
+    used++;
+    used--;
+    pthread_mutex_unlock(&m);
+  }
+
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+
+  pthread_mutex_init(&m, 0);
+  pthread_create(&tid, 0, producer, 0);
+
+  pthread_mutex_lock(&m);
+  __goblint_check(used == 0);
+  pthread_mutex_unlock(&m);
+
+  pthread_mutex_destroy(&m);
+  return 0;
+}
diff --git a/tests/regression/46-apron2/71-mutex.c b/tests/regression/46-apron2/71-mutex.c
new file mode 100644
index 0000000000..abcdda8c49
--- /dev/null
+++ b/tests/regression/46-apron2/71-mutex.c
@@ -0,0 +1,42 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.base.privatization none
+/*-----------------------------------------------------------------------------
+ * mutex.c - Concurrent program using locking to access a shared variable
+ *-----------------------------------------------------------------------------
+ * Author: Frank Schüssele
+ *   Date: 2023-07-11
+ *---------------------------------------------------------------------------*/
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int used;
+pthread_mutex_t m;
+
+void* producer()
+{
+  while (1) {
+    pthread_mutex_lock(&m);
+    used++;
+    used--;
+    pthread_mutex_unlock(&m);
+  }
+
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+
+  pthread_mutex_init(&m, 0);
+  pthread_create(&tid, 0, producer, 0);
+
+  pthread_mutex_lock(&m);
+  __goblint_check(used == 0);
+  pthread_mutex_unlock(&m);
+
+  pthread_mutex_destroy(&m);
+  return 0;
+}
diff --git a/tests/regression/46-apron2/72-mutex_with_ghosts.c b/tests/regression/46-apron2/72-mutex_with_ghosts.c
new file mode 100644
index 0000000000..8695a6133a
--- /dev/null
+++ b/tests/regression/46-apron2/72-mutex_with_ghosts.c
@@ -0,0 +1,65 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+/*-----------------------------------------------------------------------------
+ * mutex_with_ghosts.c - Annotated concurrent program with ghost variables for
+ *                       witness validation using locking to access a shared
+ *                       variable
+ *-----------------------------------------------------------------------------
+ * Author: Frank Schüssele
+ *   Date: 2023-07-11
+ *---------------------------------------------------------------------------*/
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int used;
+int g = 0;
+pthread_mutex_t m;
+
+void* producer()
+{
+  while (1) {
+    __VERIFIER_atomic_begin();
+    g = 1;
+    pthread_mutex_lock(&m);
+    __VERIFIER_atomic_end();
+
+    used++;
+    used--;
+
+    __VERIFIER_atomic_begin();
+    g = 0;
+    pthread_mutex_unlock(&m);
+    __VERIFIER_atomic_end();
+  }
+
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+
+  pthread_mutex_init(&m, 0);
+  pthread_create(&tid, 0, producer, 0);
+
+  __VERIFIER_atomic_begin();
+  __goblint_check(g == 1 || used == 0); // TODO (unprotected invariant precision loss?)
+  __VERIFIER_atomic_end();
+
+  __VERIFIER_atomic_begin();
+  g = 1;
+  pthread_mutex_lock(&m);
+  __VERIFIER_atomic_end();
+
+  __goblint_check(used == 0); // TODO (read/refine? of used above makes used write-unprotected)
+
+  __VERIFIER_atomic_begin();
+  g = 0;
+  pthread_mutex_unlock(&m);
+  __VERIFIER_atomic_end();
+
+  pthread_mutex_destroy(&m);
+  return 0;
+}
diff --git a/tests/regression/46-apron2/73-mutex_with_ghosts-2.c b/tests/regression/46-apron2/73-mutex_with_ghosts-2.c
new file mode 100644
index 0000000000..48ae9a5263
--- /dev/null
+++ b/tests/regression/46-apron2/73-mutex_with_ghosts-2.c
@@ -0,0 +1,67 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+/*-----------------------------------------------------------------------------
+ * mutex_with_ghosts.c - Annotated concurrent program with ghost variables for
+ *                       witness validation using locking to access a shared
+ *                       variable
+ *-----------------------------------------------------------------------------
+ * Author: Frank Schüssele
+ *   Date: 2023-07-11
+ *---------------------------------------------------------------------------*/
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int used;
+int g = 0;
+pthread_mutex_t m;
+
+void* producer()
+{
+  while (1) {
+    __VERIFIER_atomic_begin();
+    g = 1;
+    pthread_mutex_lock(&m);
+    __VERIFIER_atomic_end();
+
+    used++;
+    used--;
+
+    __VERIFIER_atomic_begin();
+    g = 0;
+    pthread_mutex_unlock(&m);
+    __VERIFIER_atomic_end();
+  }
+
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+
+  pthread_mutex_init(&m, 0);
+  pthread_create(&tid, 0, producer, 0);
+
+  __VERIFIER_atomic_begin();
+  int g2 = g;
+  int used2 = used;
+  __goblint_check(g2 == 1 || used2 == 0); // TODO (unprotected invariant precision loss?)
+  __VERIFIER_atomic_end();
+
+  __VERIFIER_atomic_begin();
+  g = 1;
+  pthread_mutex_lock(&m);
+  __VERIFIER_atomic_end();
+
+  __goblint_check(used == 0);
+
+  __VERIFIER_atomic_begin();
+  g = 0;
+  pthread_mutex_unlock(&m);
+  __VERIFIER_atomic_end();
+
+  pthread_mutex_destroy(&m);
+  return 0;
+}
diff --git a/tests/regression/46-apron2/74-mutex_with_ghosts-3.c b/tests/regression/46-apron2/74-mutex_with_ghosts-3.c
new file mode 100644
index 0000000000..9ce8a3a5e0
--- /dev/null
+++ b/tests/regression/46-apron2/74-mutex_with_ghosts-3.c
@@ -0,0 +1,68 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid --set ana.path_sens[+] threadflag --set sem.int.signed_overflow assume_none --enable ana.apron.strengthening
+/*-----------------------------------------------------------------------------
+ * mutex_with_ghosts.c - Annotated concurrent program with ghost variables for
+ *                       witness validation using locking to access a shared
+ *                       variable
+ *-----------------------------------------------------------------------------
+ * Author: Frank Schüssele
+ *   Date: 2023-07-11
+ *---------------------------------------------------------------------------*/
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int used;
+int g = 0;
+pthread_mutex_t m;
+
+void* producer()
+{
+  while (1) {
+    __VERIFIER_atomic_begin();
+    g = 1;
+    pthread_mutex_lock(&m);
+    __VERIFIER_atomic_end();
+
+    used++;
+    used--;
+
+    __VERIFIER_atomic_begin();
+    g = 0;
+    pthread_mutex_unlock(&m);
+    __VERIFIER_atomic_end();
+  }
+
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+
+  pthread_mutex_init(&m, 0);
+  pthread_create(&tid, 0, producer, 0);
+
+  __VERIFIER_atomic_begin();
+  int g2 = g;
+  int used2 = used;
+  __goblint_check(used2 == 0); // UNKNOWN! (currently unsound)
+  __goblint_check(g2 == 1 || used2 == 0);
+  __VERIFIER_atomic_end();
+
+  __VERIFIER_atomic_begin();
+  g = 1;
+  pthread_mutex_lock(&m);
+  __VERIFIER_atomic_end();
+
+  __goblint_check(used == 0);
+
+  __VERIFIER_atomic_begin();
+  g = 0;
+  pthread_mutex_unlock(&m);
+  __VERIFIER_atomic_end();
+
+  pthread_mutex_destroy(&m);
+  return 0;
+}

From 392bc5b5d85623608e56dbd91691196762f33436 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 14 Dec 2023 13:45:47 +0200
Subject: [PATCH 20/34] Revert "Split relational mutex-meet-tid unprotected
 invariant by global"

This reverts commit f2b2a3929178ef09f5c1170c2e9b47b9aac6945f.
---
 src/analyses/apron/relationPriv.apron.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index 7a8c7dd6a5..cdea217081 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -953,7 +953,7 @@ struct
   let atomic_mutex = LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var
 
   let get_mutex_global_g_with_mutex_inits inits ask getg g =
-    let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.global g) in
+    let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.mutex atomic_mutex) in
     let get_mutex_global_g = Cluster.keep_global g get_mutex_global_g in
     if M.tracing then M.traceli "relationpriv" "get_mutex_global_g_with_mutex_inits %a\n  get=%a\n" CilType.Varinfo.pretty g LRD.pretty get_mutex_global_g;
     let r =
@@ -968,8 +968,8 @@ struct
     if M.tracing then M.traceu "relationpriv" "-> %a\n" LRD.pretty r;
     r
 
-  let get_mutex_global_g_with_mutex_inits' inits ask getg g =
-    let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.global g) in
+  let get_mutex_global_g_with_mutex_inits' inits ask getg =
+    let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.mutex atomic_mutex) in
     if not inits then
       get_mutex_global_g
     else
@@ -988,7 +988,7 @@ struct
       if atomic && RD.mem_var rel (AV.global g) then
         rel
       else if atomic then
-        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits' (not (LMust.mem lm lmust)) ask getg g)
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits' (not (LMust.mem lm lmust)) ask getg)
       else
         Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g)
     in
@@ -1022,7 +1022,7 @@ struct
       if atomic && RD.mem_var rel (AV.global g) then
         rel
       else if atomic then
-        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits' (not (LMust.mem lm lmust)) ask getg g)
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits' (not (LMust.mem lm lmust)) ask getg)
       else
         Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g)
     in
@@ -1037,7 +1037,7 @@ struct
       let rel_side = Cluster.unlock (W.singleton g) rel_side in
       let tid = ThreadId.get_current ask in
       let sidev = GMutex.singleton tid rel_side in
-      sideg (V.global g) (G.create_global sidev);
+      sideg (V.mutex atomic_mutex) (G.create_global sidev);
       let l' = L.add lm rel_side l in
       let rel_local' =
         if is_unprotected ask g then
@@ -1104,8 +1104,8 @@ struct
       let rel_side = Cluster.unlock w rel_side in
       let tid = ThreadId.get_current ask in
       let sidev = GMutex.singleton tid rel_side in
+      sideg (V.mutex atomic_mutex) (G.create_mutex sidev);
       let (lmust', l') = W.fold (fun g (lmust, l) ->
-          sideg (V.global g) (G.create_mutex sidev);
           let lm = LLock.global g in
           (LMust.add lm lmust, L.add lm rel_side l)
         ) w (lmust, l)

From 28bc7387487e5fd040371bfcd4ce24aa7fcf037c Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 14 Dec 2023 13:53:24 +0200
Subject: [PATCH 21/34] Update mutex_with_ghosts tests with mutex-meet-tid

---
 .../46-apron2/74-mutex_with_ghosts-3.c        |  4 +-
 .../46-apron2/74-mutex_with_ghosts-4.c        | 68 +++++++++++++++++++
 2 files changed, 70 insertions(+), 2 deletions(-)
 create mode 100644 tests/regression/46-apron2/74-mutex_with_ghosts-4.c

diff --git a/tests/regression/46-apron2/74-mutex_with_ghosts-3.c b/tests/regression/46-apron2/74-mutex_with_ghosts-3.c
index 9ce8a3a5e0..d0c426481b 100644
--- a/tests/regression/46-apron2/74-mutex_with_ghosts-3.c
+++ b/tests/regression/46-apron2/74-mutex_with_ghosts-3.c
@@ -47,8 +47,8 @@ int main()
   __VERIFIER_atomic_begin();
   int g2 = g;
   int used2 = used;
-  __goblint_check(used2 == 0); // UNKNOWN! (currently unsound)
-  __goblint_check(g2 == 1 || used2 == 0);
+  __goblint_check(used2 == 0); // UNKNOWN!
+  __goblint_check(g2 == 1 || used2 == 0); // TODO (unprotected invariant precision loss?)
   __VERIFIER_atomic_end();
 
   __VERIFIER_atomic_begin();
diff --git a/tests/regression/46-apron2/74-mutex_with_ghosts-4.c b/tests/regression/46-apron2/74-mutex_with_ghosts-4.c
new file mode 100644
index 0000000000..10b601a740
--- /dev/null
+++ b/tests/regression/46-apron2/74-mutex_with_ghosts-4.c
@@ -0,0 +1,68 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid-cluster12 --set ana.path_sens[+] threadflag --set sem.int.signed_overflow assume_none --enable ana.apron.strengthening
+/*-----------------------------------------------------------------------------
+ * mutex_with_ghosts.c - Annotated concurrent program with ghost variables for
+ *                       witness validation using locking to access a shared
+ *                       variable
+ *-----------------------------------------------------------------------------
+ * Author: Frank Schüssele
+ *   Date: 2023-07-11
+ *---------------------------------------------------------------------------*/
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int used;
+int g = 0;
+pthread_mutex_t m;
+
+void* producer()
+{
+  while (1) {
+    __VERIFIER_atomic_begin();
+    g = 1;
+    pthread_mutex_lock(&m);
+    __VERIFIER_atomic_end();
+
+    used++;
+    used--;
+
+    __VERIFIER_atomic_begin();
+    g = 0;
+    pthread_mutex_unlock(&m);
+    __VERIFIER_atomic_end();
+  }
+
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+
+  pthread_mutex_init(&m, 0);
+  pthread_create(&tid, 0, producer, 0);
+
+  __VERIFIER_atomic_begin();
+  int g2 = g;
+  int used2 = used;
+  __goblint_check(used2 == 0); // UNKNOWN! (currently unsound)
+  __goblint_check(g2 == 1 || used2 == 0); // TODO (unprotected invariant precision loss?)
+  __VERIFIER_atomic_end();
+
+  __VERIFIER_atomic_begin();
+  g = 1;
+  pthread_mutex_lock(&m);
+  __VERIFIER_atomic_end();
+
+  __goblint_check(used == 0);
+
+  __VERIFIER_atomic_begin();
+  g = 0;
+  pthread_mutex_unlock(&m);
+  __VERIFIER_atomic_end();
+
+  pthread_mutex_destroy(&m);
+  return 0;
+}

From a322785a7156c100887c8290ac890a59395807d4 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 14 Dec 2023 13:54:08 +0200
Subject: [PATCH 22/34] Add names to mutex-meet-tid components

---
 src/analyses/commonPriv.ml | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 88181000b9..63ba7abd54 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -113,7 +113,11 @@ end
 
 module Locksets =
 struct
-  module Lock = LockDomain.Addr
+  module Lock =
+  struct
+    include LockDomain.Addr
+    let name () = "lock"
+  end
 
   module Lockset = SetDomain.ToppedSet (Lock) (struct let topname = "All locks" end)
 
@@ -183,7 +187,7 @@ struct
 
   module LLock =
   struct
-    include Printable.Either (Locksets.Lock) (CilType.Varinfo)
+    include Printable.Either (Locksets.Lock) (struct include CilType.Varinfo let name () = "global" end)
     let mutex m = `Left m
     let global x = `Right x
   end
@@ -195,7 +199,11 @@ struct
   end
 
   (* Map from locks to last written values thread-locally *)
-  module L = MapDomain.MapBot_LiftTop (LLock) (LD)
+  module L =
+  struct
+    include MapDomain.MapBot_LiftTop (LLock) (LD)
+    let name () = "L"
+  end
   module GMutex = MapDomain.MapBot_LiftTop (ThreadIdDomain.ThreadLifted) (LD)
   module GThread = Lattice.Prod (LMust) (L)
 

From 43552fa6edfd2205dd7f8781aea0f2198510d481 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 15 Dec 2023 13:01:33 +0200
Subject: [PATCH 23/34] Fix duplicate test ID

---
 .../{74-mutex_with_ghosts-4.c => 75-mutex_with_ghosts-4.c}        | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename tests/regression/46-apron2/{74-mutex_with_ghosts-4.c => 75-mutex_with_ghosts-4.c} (100%)

diff --git a/tests/regression/46-apron2/74-mutex_with_ghosts-4.c b/tests/regression/46-apron2/75-mutex_with_ghosts-4.c
similarity index 100%
rename from tests/regression/46-apron2/74-mutex_with_ghosts-4.c
rename to tests/regression/46-apron2/75-mutex_with_ghosts-4.c

From f754362c61302119850cd97fe777678ebfc565b8 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 11 Jan 2024 16:01:20 +0200
Subject: [PATCH 24/34] Separate base privatization with atomic support

---
 src/analyses/basePriv.ml                        | 16 ++++++++++------
 src/analyses/commonPriv.ml                      |  6 ++++++
 src/common/util/options.schema.json             |  2 +-
 tests/regression/29-svcomp/16-atomic_priv.c     |  2 +-
 tests/regression/29-svcomp/18-atomic_fun_priv.c |  2 +-
 5 files changed, 19 insertions(+), 9 deletions(-)

diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index 069a3698dd..6aad979aab 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -640,6 +640,8 @@ module type PerGlobalPrivParam =
 sig
   (** Whether to also check unprotectedness by reads for extra precision. *)
   val check_read_unprotected: bool
+
+  include AtomicParam
 end
 
 (** Protection-Based Reading. *)
@@ -690,7 +692,7 @@ struct
   let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x =
     if P.mem x st.priv then
       CPA.find x st.cpa
-    else if ask.f MustBeAtomic then
+    else if Param.handle_atomic && ask.f MustBeAtomic then
       VD.join (CPA.find x st.cpa) (getg (V.unprotected x))
     else if is_unprotected ask x then
       getg (V.unprotected x) (* CPA unnecessary because all values in GUnprot anyway *)
@@ -699,13 +701,13 @@ struct
 
   let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v =
     if not invariant then (
-      if not (ask.f MustBeAtomic) then
+      if not (Param.handle_atomic && ask.f MustBeAtomic) then
         sideg (V.unprotected x) v;
       if !earlyglobs then (* earlyglobs workaround for 13/60 *)
         sideg (V.protected x) v
         (* Unlock after invariant will still side effect refined value (if protected) from CPA, because cannot distinguish from non-invariant write since W is implicit. *)
     );
-    if ask.f MustBeAtomic then
+    if Param.handle_atomic && ask.f MustBeAtomic then
       {st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv}
     else if is_unprotected ask x then
       st
@@ -715,7 +717,7 @@ struct
   let lock ask getg st m = st
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
-    let atomic = LockDomain.Addr.equal m (LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var) in
+    let atomic = Param.handle_atomic && LockDomain.Addr.equal m (LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var) in
     (* TODO: what about G_m globals in cpa that weren't actually written? *)
     CPA.fold (fun x v (st: BaseComponents (D).t) ->
         if is_protected_by ask m x then ( (* is_in_Gm *)
@@ -1804,8 +1806,10 @@ let priv_module: (module S) Lazy.t =
         | "mutex-oplus" -> (module PerMutexOplusPriv)
         | "mutex-meet" -> (module PerMutexMeetPriv)
         | "mutex-meet-tid" -> (module PerMutexMeetTIDPriv)
-        | "protection" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false end))
-        | "protection-read" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true end))
+        | "protection" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = false end))
+        | "protection-atomic" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = true end))
+        | "protection-read" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = false end))
+        | "protection-read-atomic" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = true end))
         | "mine" -> (module MinePriv)
         | "mine-nothread" -> (module MineNoThreadPriv)
         | "mine-W" -> (module MineWPriv (struct let side_effect_global_init = true end))
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 63ba7abd54..5294c7dd50 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -9,6 +9,12 @@ module Q = Queries
 module IdxDom = ValueDomain.IndexDomain
 module VD     = BaseDomain.VD
 
+module type AtomicParam =
+sig
+  val handle_atomic: bool
+  (** Whether to handle SV-COMP atomic blocks. *)
+end
+
 module ConfCheck =
 struct
   module RequireMutexActivatedInit =
diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json
index 7c921c4f53..bb4fa194df 100644
--- a/src/common/util/options.schema.json
+++ b/src/common/util/options.schema.json
@@ -767,7 +767,7 @@
               "description":
                 "Which privatization to use? none/mutex-oplus/mutex-meet/mutex-meet-tid/protection/protection-read/mine/mine-nothread/mine-W/mine-W-noinit/lock/write/write+lock",
               "type": "string",
-              "enum": ["none", "mutex-oplus", "mutex-meet", "protection", "protection-read", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "write", "write+lock","mutex-meet-tid"],
+              "enum": ["none", "mutex-oplus", "mutex-meet", "protection", "protection-atomic", "protection-read", "protection-read-atomic", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "write", "write+lock","mutex-meet-tid"],
               "default": "protection-read"
             },
             "priv": {
diff --git a/tests/regression/29-svcomp/16-atomic_priv.c b/tests/regression/29-svcomp/16-atomic_priv.c
index 103769cc33..2f39c0ee3a 100644
--- a/tests/regression/29-svcomp/16-atomic_priv.c
+++ b/tests/regression/29-svcomp/16-atomic_priv.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions
+// PARAM: --enable ana.sv-comp.functions --set ana.base.privatization protection-atomic
 #include <pthread.h>
 #include <goblint.h>
 
diff --git a/tests/regression/29-svcomp/18-atomic_fun_priv.c b/tests/regression/29-svcomp/18-atomic_fun_priv.c
index cb7e790ebd..13c03ffb48 100644
--- a/tests/regression/29-svcomp/18-atomic_fun_priv.c
+++ b/tests/regression/29-svcomp/18-atomic_fun_priv.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions
+// PARAM: --enable ana.sv-comp.functions --set ana.base.privatization protection-atomic
 #include <pthread.h>
 #include <goblint.h>
 

From 105fd3a963388983f3fd56a7e199ed98d89351ed Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 11 Jan 2024 16:22:37 +0200
Subject: [PATCH 25/34] Separate relation mutex-meet with atomic support

---
 src/analyses/apron/relationPriv.apron.ml      | 37 ++++++++++++-------
 src/common/util/options.schema.json           |  2 +-
 tests/regression/46-apron2/58-atomic_priv.c   |  2 +-
 .../regression/46-apron2/59-atomic_fun_priv.c |  2 +-
 .../46-apron2/60-atomic_priv_sound.c          |  2 +-
 .../46-apron2/61-atomic_priv_sound2.c         |  2 +-
 .../46-apron2/62-atomic_priv_sound3.c         |  2 +-
 .../regression/46-apron2/63-atomic_relation.c |  2 +-
 .../64-case_distinction_with_ghosts.c         |  2 +-
 .../65-case_distinction_with_ghosts-2.c       |  2 +-
 .../66-case_distinction_with_ghosts-3.c       |  2 +-
 .../46-apron2/67-nondet_inc_with_ghosts.c     |  2 +-
 .../46-apron2/68-nondet_inc_with_ghosts-2.c   |  2 +-
 .../46-apron2/69-nondet_inc_with_ghosts-3.c   |  2 +-
 tests/regression/46-apron2/71-mutex.c         |  2 +-
 .../46-apron2/72-mutex_with_ghosts.c          |  2 +-
 .../46-apron2/73-mutex_with_ghosts-2.c        |  2 +-
 17 files changed, 39 insertions(+), 30 deletions(-)

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index cdea217081..cab7b9285a 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -452,7 +452,7 @@ struct
 end
 
 (** Per-mutex meet. *)
-module PerMutexMeetPriv : S = functor (RD: RelationDomain.RD) ->
+module PerMutexMeetPriv (Param: AtomicParam) : S = functor (RD: RelationDomain.RD) ->
 struct
   open CommonPerMutex(RD)
   include MutexGlobals
@@ -479,27 +479,32 @@ struct
     RD.join get_m get_mutex_inits'
 
   let get_mutex_global_g_with_mutex_inits ask getg g =
-    let get_mutex_global_g = getg (V.mutex atomic_mutex) in
-    let get_mutex_inits = getg V.mutex_inits in
     let g_var = AV.global g in
-    let get_mutex_global_g' = RD.keep_vars get_mutex_global_g [g_var] in
+    let get_mutex_global_g =
+      if Param.handle_atomic then (
+        RD.keep_vars (getg (V.mutex atomic_mutex)) [g_var]
+      )
+      else
+        getg (V.global g)
+    in
+    let get_mutex_inits = getg V.mutex_inits in
     let get_mutex_inits' = RD.keep_vars get_mutex_inits [g_var] in
-    RD.join get_mutex_global_g' get_mutex_inits'
+    RD.join get_mutex_global_g get_mutex_inits'
 
-  let get_mutex_global_g_with_mutex_inits' ask getg =
+  let get_mutex_global_g_with_mutex_inits_atomic ask getg =
     let get_mutex_global_g = getg (V.mutex atomic_mutex) in
     let get_mutex_inits = getg V.mutex_inits in
     RD.join get_mutex_global_g get_mutex_inits
 
   let read_global (ask: Q.ask) getg (st: relation_components_t) g x: RD.t =
-    let atomic = ask.f MustBeAtomic in
+    let atomic = Param.handle_atomic && ask.f MustBeAtomic in
     let rel = st.rel in
     (* lock *)
     let rel =
       if atomic && RD.mem_var rel (AV.global g) then
         rel
       else if atomic then
-        RD.meet rel (get_mutex_global_g_with_mutex_inits' ask getg)
+        RD.meet rel (get_mutex_global_g_with_mutex_inits_atomic ask getg)
       else
         RD.meet rel (get_mutex_global_g_with_mutex_inits ask getg g)
     in
@@ -522,14 +527,14 @@ struct
       rel_local
 
   let write_global ?(invariant=false) (ask: Q.ask) getg sideg (st: relation_components_t) g x: relation_components_t =
-    let atomic = ask.f MustBeAtomic in
+    let atomic = Param.handle_atomic && ask.f MustBeAtomic in
     let rel = st.rel in
     (* lock *)
     let rel =
       if atomic && RD.mem_var rel (AV.global g) then
         rel
       else if atomic then
-        RD.meet rel (get_mutex_global_g_with_mutex_inits' ask getg)
+        RD.meet rel (get_mutex_global_g_with_mutex_inits_atomic ask getg)
       else
         RD.meet rel (get_mutex_global_g_with_mutex_inits ask getg g)
     in
@@ -541,7 +546,10 @@ struct
     (* unlock *)
     if not atomic then (
       let rel_side = RD.keep_vars rel_local [g_var] in
-      sideg (V.mutex atomic_mutex) rel_side;
+      if Param.handle_atomic then
+        sideg (V.mutex atomic_mutex) rel_side
+      else
+        sideg (V.global g) rel_side;
       let rel_local' =
         if is_unprotected ask g then
           RD.remove_vars rel_local [g_var]
@@ -555,7 +563,7 @@ struct
 
 
   let lock ask getg (st: relation_components_t) m =
-    let atomic = LockDomain.Addr.equal m (atomic_mutex) in
+    let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in
     (* TODO: somehow actually unneeded here? *)
     if not atomic && Locksets.(not (Lockset.mem m (current_lockset ask))) then (
       let rel = st.rel in
@@ -569,7 +577,7 @@ struct
       st (* sound w.r.t. recursive lock *)
 
   let unlock ask getg sideg (st: relation_components_t) m: relation_components_t =
-    let atomic = LockDomain.Addr.equal m (atomic_mutex) in
+    let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in
     let rel = st.rel in
     if not atomic then (
       let rel_side = keep_only_protected_globals ask m rel in
@@ -1373,7 +1381,8 @@ let priv_module: (module S) Lazy.t =
          | "top" -> (module Top : S)
          | "protection" -> (module ProtectionBasedPriv (struct let path_sensitive = false end))
          | "protection-path" -> (module ProtectionBasedPriv (struct let path_sensitive = true end))
-         | "mutex-meet" -> (module PerMutexMeetPriv)
+         | "mutex-meet" -> (module PerMutexMeetPriv (struct let handle_atomic = false end))
+         | "mutex-meet-atomic" -> (module PerMutexMeetPriv (struct let handle_atomic = true end))
          | "mutex-meet-tid" -> (module PerMutexMeetPrivTID (NoCluster))
          | "mutex-meet-tid-cluster12" -> (module PerMutexMeetPrivTID (DownwardClosedCluster (Clustering12)))
          | "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (ArbitraryCluster (Clustering2)))
diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json
index bb4fa194df..aacccf64a9 100644
--- a/src/common/util/options.schema.json
+++ b/src/common/util/options.schema.json
@@ -921,7 +921,7 @@
               "description":
                 "Which relation privatization to use? top/protection/protection-path/mutex-meet/mutex-meet-tid/mutex-meet-tid-cluster12/mutex-meet-tid-cluster2/mutex-meet-tid-cluster-max/mutex-meet-tid-cluster-power",
               "type": "string",
-              "enum": ["top", "protection", "protection-path", "mutex-meet", "mutex-meet-tid", "mutex-meet-tid-cluster12", "mutex-meet-tid-cluster2", "mutex-meet-tid-cluster-max", "mutex-meet-tid-cluster-power"],
+              "enum": ["top", "protection", "protection-path", "mutex-meet", "mutex-meet-atomic", "mutex-meet-tid", "mutex-meet-tid-cluster12", "mutex-meet-tid-cluster2", "mutex-meet-tid-cluster-max", "mutex-meet-tid-cluster-power"],
               "default": "mutex-meet"
             },
             "priv": {
diff --git a/tests/regression/46-apron2/58-atomic_priv.c b/tests/regression/46-apron2/58-atomic_priv.c
index e8d474357b..f7c56ac515 100644
--- a/tests/regression/46-apron2/58-atomic_priv.c
+++ b/tests/regression/46-apron2/58-atomic_priv.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.base.privatization none
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none
 #include <pthread.h>
 #include <goblint.h>
 
diff --git a/tests/regression/46-apron2/59-atomic_fun_priv.c b/tests/regression/46-apron2/59-atomic_fun_priv.c
index 21df5d380f..24b3405d8f 100644
--- a/tests/regression/46-apron2/59-atomic_fun_priv.c
+++ b/tests/regression/46-apron2/59-atomic_fun_priv.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.base.privatization none
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none
 #include <pthread.h>
 #include <goblint.h>
 
diff --git a/tests/regression/46-apron2/60-atomic_priv_sound.c b/tests/regression/46-apron2/60-atomic_priv_sound.c
index 79103337c7..87ea674727 100644
--- a/tests/regression/46-apron2/60-atomic_priv_sound.c
+++ b/tests/regression/46-apron2/60-atomic_priv_sound.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.base.privatization none
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none
 #include <pthread.h>
 #include <goblint.h>
 
diff --git a/tests/regression/46-apron2/61-atomic_priv_sound2.c b/tests/regression/46-apron2/61-atomic_priv_sound2.c
index c9ecb90a1e..393e56a026 100644
--- a/tests/regression/46-apron2/61-atomic_priv_sound2.c
+++ b/tests/regression/46-apron2/61-atomic_priv_sound2.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.base.privatization none
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none
 #include <pthread.h>
 #include <goblint.h>
 
diff --git a/tests/regression/46-apron2/62-atomic_priv_sound3.c b/tests/regression/46-apron2/62-atomic_priv_sound3.c
index 7967507b65..1a8ee32581 100644
--- a/tests/regression/46-apron2/62-atomic_priv_sound3.c
+++ b/tests/regression/46-apron2/62-atomic_priv_sound3.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.base.privatization none
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none
 #include <pthread.h>
 #include <goblint.h>
 
diff --git a/tests/regression/46-apron2/63-atomic_relation.c b/tests/regression/46-apron2/63-atomic_relation.c
index 4169b1e447..d3ab987ae6 100644
--- a/tests/regression/46-apron2/63-atomic_relation.c
+++ b/tests/regression/46-apron2/63-atomic_relation.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none
 #include <pthread.h>
 #include <goblint.h>
 
diff --git a/tests/regression/46-apron2/64-case_distinction_with_ghosts.c b/tests/regression/46-apron2/64-case_distinction_with_ghosts.c
index 633c1192c9..b319f3e4b1 100644
--- a/tests/regression/46-apron2/64-case_distinction_with_ghosts.c
+++ b/tests/regression/46-apron2/64-case_distinction_with_ghosts.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none
 #include <pthread.h>
 #include <assert.h>
 
diff --git a/tests/regression/46-apron2/65-case_distinction_with_ghosts-2.c b/tests/regression/46-apron2/65-case_distinction_with_ghosts-2.c
index 89371e74fa..223734e395 100644
--- a/tests/regression/46-apron2/65-case_distinction_with_ghosts-2.c
+++ b/tests/regression/46-apron2/65-case_distinction_with_ghosts-2.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none
 #include <pthread.h>
 #include <assert.h>
 
diff --git a/tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c b/tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c
index 6fc2700299..e130c68fa1 100644
--- a/tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c
+++ b/tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none
 #include <pthread.h>
 #include <assert.h>
 
diff --git a/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c b/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c
index 2fc073db05..a7227e3793 100644
--- a/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c
+++ b/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none --enable ana.apron.threshold_widening
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none --enable ana.apron.threshold_widening
 #include <pthread.h>
 #include <assert.h>
 
diff --git a/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c b/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c
index 380821add9..e5a281ec0c 100644
--- a/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c
+++ b/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none --enable ana.apron.threshold_widening
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none --enable ana.apron.threshold_widening
 #include <pthread.h>
 #include <assert.h>
 
diff --git a/tests/regression/46-apron2/69-nondet_inc_with_ghosts-3.c b/tests/regression/46-apron2/69-nondet_inc_with_ghosts-3.c
index 0519dbda00..b6f4f69858 100644
--- a/tests/regression/46-apron2/69-nondet_inc_with_ghosts-3.c
+++ b/tests/regression/46-apron2/69-nondet_inc_with_ghosts-3.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none
 #include <pthread.h>
 #include <assert.h>
 
diff --git a/tests/regression/46-apron2/71-mutex.c b/tests/regression/46-apron2/71-mutex.c
index abcdda8c49..99148c4d77 100644
--- a/tests/regression/46-apron2/71-mutex.c
+++ b/tests/regression/46-apron2/71-mutex.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.base.privatization none
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none
 /*-----------------------------------------------------------------------------
  * mutex.c - Concurrent program using locking to access a shared variable
  *-----------------------------------------------------------------------------
diff --git a/tests/regression/46-apron2/72-mutex_with_ghosts.c b/tests/regression/46-apron2/72-mutex_with_ghosts.c
index 8695a6133a..ccd6eab93f 100644
--- a/tests/regression/46-apron2/72-mutex_with_ghosts.c
+++ b/tests/regression/46-apron2/72-mutex_with_ghosts.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none
 /*-----------------------------------------------------------------------------
  * mutex_with_ghosts.c - Annotated concurrent program with ghost variables for
  *                       witness validation using locking to access a shared
diff --git a/tests/regression/46-apron2/73-mutex_with_ghosts-2.c b/tests/regression/46-apron2/73-mutex_with_ghosts-2.c
index 48ae9a5263..84a18faa20 100644
--- a/tests/regression/46-apron2/73-mutex_with_ghosts-2.c
+++ b/tests/regression/46-apron2/73-mutex_with_ghosts-2.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none
 /*-----------------------------------------------------------------------------
  * mutex_with_ghosts.c - Annotated concurrent program with ghost variables for
  *                       witness validation using locking to access a shared

From d4a1fe41b6bc3f258150d14971b976acc383b2fe Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 11 Jan 2024 16:33:55 +0200
Subject: [PATCH 26/34] Separate relation mutex-meet-tid with atomic support

---
 src/analyses/apron/relationPriv.apron.ml      | 44 ++++++++++++-------
 src/analyses/commonPriv.ml                    |  5 +++
 src/common/util/options.schema.json           |  2 +-
 .../70-nondet_inc_with_ghosts-globalize.c     |  3 +-
 .../46-apron2/74-mutex_with_ghosts-3.c        |  2 +-
 .../46-apron2/75-mutex_with_ghosts-4.c        |  3 +-
 6 files changed, 38 insertions(+), 21 deletions(-)

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index cab7b9285a..ce60b34312 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -911,7 +911,7 @@ struct
 end
 
 (** Per-mutex meet with TIDs. *)
-module PerMutexMeetPrivTID (Cluster: ClusterArg): S  = functor (RD: RelationDomain.RD) ->
+module PerMutexMeetPrivTID (Param: AtomicParam) (Cluster: ClusterArg): S  = functor (RD: RelationDomain.RD) ->
 struct
   open CommonPerMutex(RD)
   include MutexGlobals
@@ -961,8 +961,14 @@ struct
   let atomic_mutex = LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var
 
   let get_mutex_global_g_with_mutex_inits inits ask getg g =
-    let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.mutex atomic_mutex) in
-    let get_mutex_global_g = Cluster.keep_global g get_mutex_global_g in
+    let get_mutex_global_g =
+      if Param.handle_atomic then (
+        get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.mutex atomic_mutex)
+        |> Cluster.keep_global g
+      )
+      else
+        get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.global g)
+    in
     if M.tracing then M.traceli "relationpriv" "get_mutex_global_g_with_mutex_inits %a\n  get=%a\n" CilType.Varinfo.pretty g LRD.pretty get_mutex_global_g;
     let r =
       if not inits then
@@ -976,7 +982,7 @@ struct
     if M.tracing then M.traceu "relationpriv" "-> %a\n" LRD.pretty r;
     r
 
-  let get_mutex_global_g_with_mutex_inits' inits ask getg =
+  let get_mutex_global_g_with_mutex_inits_atomic inits ask getg =
     let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.mutex atomic_mutex) in
     if not inits then
       get_mutex_global_g
@@ -985,7 +991,7 @@ struct
       LRD.join get_mutex_global_g get_mutex_inits
 
   let read_global (ask: Q.ask) getg (st: relation_components_t) g x: RD.t =
-    let atomic = ask.f MustBeAtomic in
+    let atomic = Param.handle_atomic && ask.f MustBeAtomic in
     let _,lmust,l = st.priv in
     let rel = st.rel in
     let lm = LLock.global g in
@@ -996,7 +1002,7 @@ struct
       if atomic && RD.mem_var rel (AV.global g) then
         rel
       else if atomic then
-        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits' (not (LMust.mem lm lmust)) ask getg)
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits_atomic (not (LMust.mem lm lmust)) ask getg)
       else
         Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g)
     in
@@ -1019,7 +1025,7 @@ struct
       rel_local
 
   let write_global ?(invariant=false) (ask:Q.ask) getg sideg (st: relation_components_t) g x: relation_components_t =
-    let atomic = ask.f MustBeAtomic in
+    let atomic = Param.handle_atomic && ask.f MustBeAtomic in
     let w,lmust,l = st.priv in
     let lm = LLock.global g in
     let rel = st.rel in
@@ -1030,7 +1036,7 @@ struct
       if atomic && RD.mem_var rel (AV.global g) then
         rel
       else if atomic then
-        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits' (not (LMust.mem lm lmust)) ask getg)
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits_atomic (not (LMust.mem lm lmust)) ask getg)
       else
         Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g)
     in
@@ -1045,7 +1051,10 @@ struct
       let rel_side = Cluster.unlock (W.singleton g) rel_side in
       let tid = ThreadId.get_current ask in
       let sidev = GMutex.singleton tid rel_side in
-      sideg (V.mutex atomic_mutex) (G.create_global sidev);
+      if Param.handle_atomic then
+        sideg (V.mutex atomic_mutex) (G.create_global sidev)
+      else
+        sideg (V.global g) (G.create_global sidev);
       let l' = L.add lm rel_side l in
       let rel_local' =
         if is_unprotected ask g then
@@ -1063,7 +1072,7 @@ struct
     )
 
   let lock ask getg (st: relation_components_t) m =
-    let atomic = LockDomain.Addr.equal m (atomic_mutex) in
+    let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in
     if not atomic && Locksets.(not (Lockset.mem m (current_lockset ask))) then (
       let rel = st.rel in
       let _,lmust,l = st.priv in
@@ -1086,7 +1095,7 @@ struct
     RD.keep_filter oct protected
 
   let unlock ask getg sideg (st: relation_components_t) m: relation_components_t =
-    let atomic = LockDomain.Addr.equal m (atomic_mutex) in
+    let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in
     let rel = st.rel in
     let w,lmust,l = st.priv in
     if not atomic then (
@@ -1381,13 +1390,14 @@ let priv_module: (module S) Lazy.t =
          | "top" -> (module Top : S)
          | "protection" -> (module ProtectionBasedPriv (struct let path_sensitive = false end))
          | "protection-path" -> (module ProtectionBasedPriv (struct let path_sensitive = true end))
-         | "mutex-meet" -> (module PerMutexMeetPriv (struct let handle_atomic = false end))
+         | "mutex-meet" -> (module PerMutexMeetPriv (NoAtomic))
          | "mutex-meet-atomic" -> (module PerMutexMeetPriv (struct let handle_atomic = true end))
-         | "mutex-meet-tid" -> (module PerMutexMeetPrivTID (NoCluster))
-         | "mutex-meet-tid-cluster12" -> (module PerMutexMeetPrivTID (DownwardClosedCluster (Clustering12)))
-         | "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (ArbitraryCluster (Clustering2)))
-         | "mutex-meet-tid-cluster-max" -> (module PerMutexMeetPrivTID (ArbitraryCluster (ClusteringMax)))
-         | "mutex-meet-tid-cluster-power" -> (module PerMutexMeetPrivTID (DownwardClosedCluster (ClusteringPower)))
+         | "mutex-meet-tid" -> (module PerMutexMeetPrivTID (NoAtomic) (NoCluster))
+         | "mutex-meet-tid-atomic" -> (module PerMutexMeetPrivTID (struct let handle_atomic = true end) (NoCluster))
+         | "mutex-meet-tid-cluster12" -> (module PerMutexMeetPrivTID (NoAtomic) (DownwardClosedCluster (Clustering12)))
+         | "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (NoAtomic) (ArbitraryCluster (Clustering2)))
+         | "mutex-meet-tid-cluster-max" -> (module PerMutexMeetPrivTID (NoAtomic) (ArbitraryCluster (ClusteringMax)))
+         | "mutex-meet-tid-cluster-power" -> (module PerMutexMeetPrivTID (NoAtomic) (DownwardClosedCluster (ClusteringPower)))
          | _ -> failwith "ana.relation.privatization: illegal value"
       )
     in
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 5294c7dd50..4a71e64bd1 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -15,6 +15,11 @@ sig
   (** Whether to handle SV-COMP atomic blocks. *)
 end
 
+module NoAtomic: AtomicParam =
+struct
+  let handle_atomic = false
+end
+
 module ConfCheck =
 struct
   module RequireMutexActivatedInit =
diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json
index aacccf64a9..3b20561358 100644
--- a/src/common/util/options.schema.json
+++ b/src/common/util/options.schema.json
@@ -921,7 +921,7 @@
               "description":
                 "Which relation privatization to use? top/protection/protection-path/mutex-meet/mutex-meet-tid/mutex-meet-tid-cluster12/mutex-meet-tid-cluster2/mutex-meet-tid-cluster-max/mutex-meet-tid-cluster-power",
               "type": "string",
-              "enum": ["top", "protection", "protection-path", "mutex-meet", "mutex-meet-atomic", "mutex-meet-tid", "mutex-meet-tid-cluster12", "mutex-meet-tid-cluster2", "mutex-meet-tid-cluster-max", "mutex-meet-tid-cluster-power"],
+              "enum": ["top", "protection", "protection-path", "mutex-meet", "mutex-meet-atomic", "mutex-meet-tid", "mutex-meet-tid-atomic", "mutex-meet-tid-cluster12", "mutex-meet-tid-cluster2", "mutex-meet-tid-cluster-max", "mutex-meet-tid-cluster-power"],
               "default": "mutex-meet"
             },
             "priv": {
diff --git a/tests/regression/46-apron2/70-nondet_inc_with_ghosts-globalize.c b/tests/regression/46-apron2/70-nondet_inc_with_ghosts-globalize.c
index 8a52ffae32..2e01b017b8 100644
--- a/tests/regression/46-apron2/70-nondet_inc_with_ghosts-globalize.c
+++ b/tests/regression/46-apron2/70-nondet_inc_with_ghosts-globalize.c
@@ -1,4 +1,5 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid --set sem.int.signed_overflow assume_none --enable ana.apron.threshold_widening --set ana.path_sens[+] threadflag --enable ana.apron.strengthening
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid-atomic --set sem.int.signed_overflow assume_none --enable ana.apron.threshold_widening --set ana.path_sens[+] threadflag --enable ana.apron.strengthening
+// TODO: -atomic unneeded?
 #include <pthread.h>
 #include <assert.h>
 
diff --git a/tests/regression/46-apron2/74-mutex_with_ghosts-3.c b/tests/regression/46-apron2/74-mutex_with_ghosts-3.c
index d0c426481b..a1c83950b5 100644
--- a/tests/regression/46-apron2/74-mutex_with_ghosts-3.c
+++ b/tests/regression/46-apron2/74-mutex_with_ghosts-3.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid --set ana.path_sens[+] threadflag --set sem.int.signed_overflow assume_none --enable ana.apron.strengthening
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid-atomic --set ana.path_sens[+] threadflag --set sem.int.signed_overflow assume_none --enable ana.apron.strengthening
 /*-----------------------------------------------------------------------------
  * mutex_with_ghosts.c - Annotated concurrent program with ghost variables for
  *                       witness validation using locking to access a shared
diff --git a/tests/regression/46-apron2/75-mutex_with_ghosts-4.c b/tests/regression/46-apron2/75-mutex_with_ghosts-4.c
index 10b601a740..ff544708e1 100644
--- a/tests/regression/46-apron2/75-mutex_with_ghosts-4.c
+++ b/tests/regression/46-apron2/75-mutex_with_ghosts-4.c
@@ -1,4 +1,5 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid-cluster12 --set ana.path_sens[+] threadflag --set sem.int.signed_overflow assume_none --enable ana.apron.strengthening
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid-atomic --set ana.path_sens[+] threadflag --set sem.int.signed_overflow assume_none --enable ana.apron.strengthening
+// TODO: unsound with cluster12
 /*-----------------------------------------------------------------------------
  * mutex_with_ghosts.c - Annotated concurrent program with ghost variables for
  *                       witness validation using locking to access a shared

From b12b6e83f70cda82af11c0065c3631228180b59e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 11 Jan 2024 16:44:27 +0200
Subject: [PATCH 27/34] Delete duplicate priv-atomic tests

---
 .../66-case_distinction_with_ghosts-3.c       | 30 --------
 .../46-apron2/74-mutex_with_ghosts-3.c        |  1 +
 .../46-apron2/75-mutex_with_ghosts-4.c        | 69 -------------------
 3 files changed, 1 insertion(+), 99 deletions(-)
 delete mode 100644 tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c
 delete mode 100644 tests/regression/46-apron2/75-mutex_with_ghosts-4.c

diff --git a/tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c b/tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c
deleted file mode 100644
index e130c68fa1..0000000000
--- a/tests/regression/46-apron2/66-case_distinction_with_ghosts-3.c
+++ /dev/null
@@ -1,30 +0,0 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none
-#include <pthread.h>
-#include <assert.h>
-
-extern int  __VERIFIER_nondet_int();
-extern void __VERIFIER_atomic_begin();
-extern void __VERIFIER_atomic_end();
-
-int x = 0;
-int g = 0;
-
-void* inc()
-{
-  // x = 10; // TODO: what is this?
-
-  __VERIFIER_atomic_begin();
-  assert(g != 1 || x >= 42); // TODO
-  __VERIFIER_atomic_end();
-  return 0;
-}
-
-int main()
-{
-  pthread_t tid;
-  pthread_create(&tid, 0, inc, 0);
-  __VERIFIER_atomic_begin();
-  g = 1; x = 42;
-  __VERIFIER_atomic_end();
-  return 0;
-}
diff --git a/tests/regression/46-apron2/74-mutex_with_ghosts-3.c b/tests/regression/46-apron2/74-mutex_with_ghosts-3.c
index a1c83950b5..e7da4cb5bc 100644
--- a/tests/regression/46-apron2/74-mutex_with_ghosts-3.c
+++ b/tests/regression/46-apron2/74-mutex_with_ghosts-3.c
@@ -1,4 +1,5 @@
 // PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid-atomic --set ana.path_sens[+] threadflag --set sem.int.signed_overflow assume_none --enable ana.apron.strengthening
+// TODO: unsound with cluster12
 /*-----------------------------------------------------------------------------
  * mutex_with_ghosts.c - Annotated concurrent program with ghost variables for
  *                       witness validation using locking to access a shared
diff --git a/tests/regression/46-apron2/75-mutex_with_ghosts-4.c b/tests/regression/46-apron2/75-mutex_with_ghosts-4.c
deleted file mode 100644
index ff544708e1..0000000000
--- a/tests/regression/46-apron2/75-mutex_with_ghosts-4.c
+++ /dev/null
@@ -1,69 +0,0 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid-atomic --set ana.path_sens[+] threadflag --set sem.int.signed_overflow assume_none --enable ana.apron.strengthening
-// TODO: unsound with cluster12
-/*-----------------------------------------------------------------------------
- * mutex_with_ghosts.c - Annotated concurrent program with ghost variables for
- *                       witness validation using locking to access a shared
- *                       variable
- *-----------------------------------------------------------------------------
- * Author: Frank Schüssele
- *   Date: 2023-07-11
- *---------------------------------------------------------------------------*/
-#include <pthread.h>
-#include <goblint.h>
-
-extern void __VERIFIER_atomic_begin();
-extern void __VERIFIER_atomic_end();
-
-int used;
-int g = 0;
-pthread_mutex_t m;
-
-void* producer()
-{
-  while (1) {
-    __VERIFIER_atomic_begin();
-    g = 1;
-    pthread_mutex_lock(&m);
-    __VERIFIER_atomic_end();
-
-    used++;
-    used--;
-
-    __VERIFIER_atomic_begin();
-    g = 0;
-    pthread_mutex_unlock(&m);
-    __VERIFIER_atomic_end();
-  }
-
-  return 0;
-}
-
-int main()
-{
-  pthread_t tid;
-
-  pthread_mutex_init(&m, 0);
-  pthread_create(&tid, 0, producer, 0);
-
-  __VERIFIER_atomic_begin();
-  int g2 = g;
-  int used2 = used;
-  __goblint_check(used2 == 0); // UNKNOWN! (currently unsound)
-  __goblint_check(g2 == 1 || used2 == 0); // TODO (unprotected invariant precision loss?)
-  __VERIFIER_atomic_end();
-
-  __VERIFIER_atomic_begin();
-  g = 1;
-  pthread_mutex_lock(&m);
-  __VERIFIER_atomic_end();
-
-  __goblint_check(used == 0);
-
-  __VERIFIER_atomic_begin();
-  g = 0;
-  pthread_mutex_unlock(&m);
-  __VERIFIER_atomic_end();
-
-  pthread_mutex_destroy(&m);
-  return 0;
-}

From 92eac6da41e6889ec718c1898870069e3905058e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 11 Jan 2024 16:53:28 +0200
Subject: [PATCH 28/34] Add __goblint_globalize special function

---
 docs/user-guide/annotating.md                             | 1 +
 lib/goblint/runtime/include/goblint.h                     | 1 +
 src/analyses/libraryDesc.ml                               | 1 +
 src/analyses/libraryFunctions.ml                          | 1 +
 src/analyses/threadEscape.ml                              | 3 +++
 .../46-apron2/70-nondet_inc_with_ghosts-globalize.c       | 8 ++------
 6 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/docs/user-guide/annotating.md b/docs/user-guide/annotating.md
index cdfb892ffe..af632e60ed 100644
--- a/docs/user-guide/annotating.md
+++ b/docs/user-guide/annotating.md
@@ -66,3 +66,4 @@ Include `goblint.h` when using these.
 * `__goblint_assume_join(id)` is like `pthread_join(id, NULL)`, but considers the given thread IDs must-joined even if Goblint cannot, e.g. due to non-uniqueness.
   Notably, this annotation can be used after a threads joining loop to make the assumption that the loop correctly joined all those threads.
   _Misuse of this annotation can cause unsoundness._
+* `__goblint_globalize(ptr)` forces data pointed to by `ptr` to be treated as global by simulating it escaping the thread.
diff --git a/lib/goblint/runtime/include/goblint.h b/lib/goblint/runtime/include/goblint.h
index af87035d33..8b32bf6ccb 100644
--- a/lib/goblint/runtime/include/goblint.h
+++ b/lib/goblint/runtime/include/goblint.h
@@ -3,6 +3,7 @@ void __goblint_assume(int exp);
 void __goblint_assert(int exp);
 
 void __goblint_assume_join(/* pthread_t thread */); // undeclared argument to avoid pthread.h interfering with Linux kernel headers
+void __goblint_globalize(void *ptr);
 
 void __goblint_split_begin(int exp);
 void __goblint_split_end(int exp);
diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml
index 4997b306a9..9117281e13 100644
--- a/src/analyses/libraryDesc.ml
+++ b/src/analyses/libraryDesc.ml
@@ -56,6 +56,7 @@ type special =
   | ThreadCreate of { thread: Cil.exp; start_routine: Cil.exp; arg: Cil.exp; }
   | ThreadJoin of { thread: Cil.exp; ret_var: Cil.exp; }
   | ThreadExit of { ret_val: Cil.exp; }
+  | Globalize of Cil.exp
   | Signal of Cil.exp
   | Broadcast of Cil.exp
   | MutexAttrSetType of { attr:Cil.exp; typ: Cil.exp; }
diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 8152e5b886..de3ff82ead 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -743,6 +743,7 @@ let goblint_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__goblint_check", special [__ "exp" []] @@ fun exp -> Assert { exp; check = true; refine = false });
     ("__goblint_assume", special [__ "exp" []] @@ fun exp -> Assert { exp; check = false; refine = true });
     ("__goblint_assert", special [__ "exp" []] @@ fun exp -> Assert { exp; check = true; refine = get_bool "sem.assert.refine" });
+    ("__goblint_globalize", special [__ "ptr" []] @@ fun ptr -> Globalize ptr);
     ("__goblint_split_begin", unknown [drop "exp" []]);
     ("__goblint_split_end", unknown [drop "exp" []]);
     ("__goblint_bounded", special [__ "exp"[]] @@ fun exp -> Bounded { exp });
diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml
index 21a8b69c93..6942e29bd7 100644
--- a/src/analyses/threadEscape.ml
+++ b/src/analyses/threadEscape.ml
@@ -142,6 +142,9 @@ struct
   let special ctx (lval: lval option) (f:varinfo) (args:exp list) : D.t =
     let desc = LibraryFunctions.find f in
     match desc.special args, f.vname, args with
+    | Globalize ptr, _, _ ->
+      let escaped = escape_rval ctx ptr in
+      D.join ctx.local escaped
     | _, "pthread_setspecific" , [key; pt_value] ->
       let escaped = escape_rval ctx pt_value in
       D.join ctx.local escaped
diff --git a/tests/regression/46-apron2/70-nondet_inc_with_ghosts-globalize.c b/tests/regression/46-apron2/70-nondet_inc_with_ghosts-globalize.c
index 2e01b017b8..07d90808ed 100644
--- a/tests/regression/46-apron2/70-nondet_inc_with_ghosts-globalize.c
+++ b/tests/regression/46-apron2/70-nondet_inc_with_ghosts-globalize.c
@@ -2,6 +2,7 @@
 // TODO: -atomic unneeded?
 #include <pthread.h>
 #include <assert.h>
+#include <goblint.h>
 
 extern int  __VERIFIER_nondet_int();
 extern void __VERIFIER_atomic_begin();
@@ -27,11 +28,6 @@ void* inc()
   return 0;
 }
 
-void* dummy()
-{
-  return 0;
-}
-
 int main()
 {
   pthread_t tid;
@@ -39,7 +35,7 @@ int main()
 
   int val = __VERIFIER_nondet_int();
   __VERIFIER_atomic_begin();
-  pthread_create(&tid, 0, dummy, &val); // globalize val by escaping
+  __goblint_globalize(&val);
   g = val; x = val;
   __VERIFIER_atomic_end();
 

From 696a35ff9a232bb48353e6ddefeca5398e92d6a2 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 11 Jan 2024 16:58:11 +0200
Subject: [PATCH 29/34] Comment out atomic mutex protecting everything again

---
 src/analyses/mutexAnalysis.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 702b3b4224..a0f4304b54 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -229,9 +229,9 @@ struct
       let mutex_lockset = Lockset.export_locks @@ Lockset.singleton (mutex, true) in
       let protecting = protecting ~write protection v in
       (* TODO: unsound in 29/24, why did we do this before? *)
-      if LockDomain.Addr.equal mutex (LockDomain.Addr.of_var LF.verifier_atomic_var) then
+      (* if LockDomain.Addr.equal mutex (LockDomain.Addr.of_var LF.verifier_atomic_var) then
         true
-      else
+      else *)
       Mutexes.leq mutex_lockset protecting
     | Queries.MustLockset ->
       let held_locks = Lockset.export_locks (Lockset.filter snd ls) in

From 45555adf6c347b1917e8de169533cf64787cfee3 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 25 Jan 2024 13:18:56 +0200
Subject: [PATCH 30/34] Add case_distinction_with_ghosts variant where reads
 publish to unprotected

---
 .../75-case_distinction_with_ghosts-3.c       | 31 +++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 tests/regression/46-apron2/75-case_distinction_with_ghosts-3.c

diff --git a/tests/regression/46-apron2/75-case_distinction_with_ghosts-3.c b/tests/regression/46-apron2/75-case_distinction_with_ghosts-3.c
new file mode 100644
index 0000000000..0d33bf1281
--- /dev/null
+++ b/tests/regression/46-apron2/75-case_distinction_with_ghosts-3.c
@@ -0,0 +1,31 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid-atomic --set sem.int.signed_overflow assume_none --set ana.path_sens[+] threadflag
+#include <pthread.h>
+#include <assert.h>
+
+extern int  __VERIFIER_nondet_int();
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int x = 0;
+int g = 0;
+
+void* inc()
+{
+  __VERIFIER_atomic_begin();
+  int x2 = x;
+  int g2 = g;
+  __VERIFIER_atomic_end();
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+  pthread_create(&tid, 0, inc, 0);
+  __VERIFIER_atomic_begin();
+  g = 1; x = 42;
+  __VERIFIER_atomic_end();
+
+  assert(x >= 42); // TODO (ruined by reads in inc thread)
+  return 0;
+}

From 67558f4962875516a9336f58c23637c67b2ec0bf Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 25 Jan 2024 13:53:47 +0200
Subject: [PATCH 31/34] Make mutex-meet-tid-atomic more precise for no-write
 unlocks

---
 src/analyses/apron/relationPriv.apron.ml      | 26 +++++++++++--------
 .../75-case_distinction_with_ghosts-3.c       |  2 +-
 2 files changed, 16 insertions(+), 12 deletions(-)

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index 7173145d40..d046eb9e43 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -1112,17 +1112,21 @@ struct
     else (
       let rel_local = remove_globals_unprotected_after_unlock ask m rel in
       let w' = W.filter (fun v -> not (is_unprotected_without ask v m)) w in
-      let rel_side = keep_only_globals ask m rel in
-      let rel_side = Cluster.unlock w rel_side in
-      let digest = Digest.current ask in
-      let sidev = GMutex.singleton digest rel_side in
-      sideg (V.mutex atomic_mutex) (G.create_mutex sidev);
-      let (lmust', l') = W.fold (fun g (lmust, l) ->
-          let lm = LLock.global g in
-          (LMust.add lm lmust, L.add lm rel_side l)
-        ) w (lmust, l)
-      in
-      {rel = rel_local; priv = (w',lmust',l')}
+      let side_needed = not (W.is_empty w) in
+      if not side_needed then
+        {rel = rel_local; priv = (w',lmust,l)}
+      else
+        let rel_side = keep_only_globals ask m rel in
+        let rel_side = Cluster.unlock w rel_side in
+        let digest = Digest.current ask in
+        let sidev = GMutex.singleton digest rel_side in
+        sideg (V.mutex atomic_mutex) (G.create_mutex sidev);
+        let (lmust', l') = W.fold (fun g (lmust, l) ->
+            let lm = LLock.global g in
+            (LMust.add lm lmust, L.add lm rel_side l)
+          ) w (lmust, l)
+        in
+        {rel = rel_local; priv = (w',lmust',l')}
     )
 
   let thread_join ?(force=false) (ask:Q.ask) getg exp (st: relation_components_t) =
diff --git a/tests/regression/46-apron2/75-case_distinction_with_ghosts-3.c b/tests/regression/46-apron2/75-case_distinction_with_ghosts-3.c
index 0d33bf1281..c7d4b222a8 100644
--- a/tests/regression/46-apron2/75-case_distinction_with_ghosts-3.c
+++ b/tests/regression/46-apron2/75-case_distinction_with_ghosts-3.c
@@ -26,6 +26,6 @@ int main()
   g = 1; x = 42;
   __VERIFIER_atomic_end();
 
-  assert(x >= 42); // TODO (ruined by reads in inc thread)
+  assert(x >= 42);
   return 0;
 }

From 3bafccb5185a30eb4eed89a742580f4a0a96930b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 29 Jan 2024 14:45:08 +0200
Subject: [PATCH 32/34] Update __goblint_globalize documentation

Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
---
 docs/user-guide/annotating.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/user-guide/annotating.md b/docs/user-guide/annotating.md
index af632e60ed..8312869ef9 100644
--- a/docs/user-guide/annotating.md
+++ b/docs/user-guide/annotating.md
@@ -66,4 +66,4 @@ Include `goblint.h` when using these.
 * `__goblint_assume_join(id)` is like `pthread_join(id, NULL)`, but considers the given thread IDs must-joined even if Goblint cannot, e.g. due to non-uniqueness.
   Notably, this annotation can be used after a threads joining loop to make the assumption that the loop correctly joined all those threads.
   _Misuse of this annotation can cause unsoundness._
-* `__goblint_globalize(ptr)` forces data pointed to by `ptr` to be treated as global by simulating it escaping the thread.
+* `__goblint_globalize(ptr)` forces all data potentially pointed to by `ptr` to be treated as global by simulating it escaping the thread.

From ae5c42ea817555d87b8c52f24c4daf5c017433ce Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 29 Jan 2024 15:52:45 +0200
Subject: [PATCH 33/34] Remove commented out code in
 RelationPriv.PerMutexMeetPrivTID.write_global

---
 src/analyses/apron/relationPriv.apron.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index d046eb9e43..80a419314c 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -1059,12 +1059,8 @@ struct
       in
       {rel = rel_local'; priv = (W.add g w,LMust.add lm lmust,l')}
     )
-    else (
-      (* let rel_side = RD.keep_vars rel_local [g_var] in
-      let rel_side = Cluster.unlock (W.singleton g) rel_side in
-      let l' = L.add lm rel_side l in *)
+    else
       {rel = rel_local; priv = (W.add g w,lmust,l)}
-    )
 
   let lock ask getg (st: relation_components_t) m =
     let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in

From 6a2d078e39f45ed98264fb65e76a3b82e0e3e160 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 15 Feb 2024 13:35:50 +0200
Subject: [PATCH 34/34] Comment atomic privatizations

---
 src/analyses/apron/relationPriv.apron.ml | 44 +++++++++++++++---------
 src/analyses/basePriv.ml                 | 12 +++----
 src/analyses/commonPriv.ml               |  2 +-
 3 files changed, 35 insertions(+), 23 deletions(-)

diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index 80a419314c..b1cb777be7 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -481,6 +481,7 @@ struct
     let g_var = AV.global g in
     let get_mutex_global_g =
       if Param.handle_atomic then (
+        (* Unprotected invariant is one big relation. *)
         RD.keep_vars (getg (V.mutex atomic_mutex)) [g_var]
       )
       else
@@ -491,6 +492,7 @@ struct
     RD.join get_mutex_global_g get_mutex_inits'
 
   let get_mutex_global_g_with_mutex_inits_atomic ask getg =
+    (* Unprotected invariant is one big relation. *)
     let get_mutex_global_g = getg (V.mutex atomic_mutex) in
     let get_mutex_inits = getg V.mutex_inits in
     RD.join get_mutex_global_g get_mutex_inits
@@ -501,9 +503,9 @@ struct
     (* lock *)
     let rel =
       if atomic && RD.mem_var rel (AV.global g) then
-        rel
+        rel (* Read previous unpublished unprotected write in current atomic section. *)
       else if atomic then
-        RD.meet rel (get_mutex_global_g_with_mutex_inits_atomic ask getg)
+        RD.meet rel (get_mutex_global_g_with_mutex_inits_atomic ask getg) (* Read unprotected invariant as full relation. *)
       else
         RD.meet rel (get_mutex_global_g_with_mutex_inits ask getg g)
     in
@@ -523,7 +525,7 @@ struct
       rel_local'
     )
     else
-      rel_local
+      rel_local (* Keep write local as if it were protected by the atomic section. *)
 
   let write_global ?(invariant=false) (ask: Q.ask) getg sideg (st: relation_components_t) g x: relation_components_t =
     let atomic = Param.handle_atomic && ask.f MustBeAtomic in
@@ -531,9 +533,9 @@ struct
     (* lock *)
     let rel =
       if atomic && RD.mem_var rel (AV.global g) then
-        rel
+        rel (* Read previous unpublished unprotected write in current atomic section. *)
       else if atomic then
-        RD.meet rel (get_mutex_global_g_with_mutex_inits_atomic ask getg)
+        RD.meet rel (get_mutex_global_g_with_mutex_inits_atomic ask getg) (* Read unprotected invariant as full relation. *)
       else
         RD.meet rel (get_mutex_global_g_with_mutex_inits ask getg g)
     in
@@ -546,7 +548,7 @@ struct
     if not atomic then (
       let rel_side = RD.keep_vars rel_local [g_var] in
       if Param.handle_atomic then
-        sideg (V.mutex atomic_mutex) rel_side
+        sideg (V.mutex atomic_mutex) rel_side (* Unprotected invariant is one big relation. *)
       else
         sideg (V.global g) rel_side;
       let rel_local' =
@@ -558,7 +560,8 @@ struct
       {st with rel = rel_local'}
     )
     else
-      {st with rel = rel_local}
+      (* Delay publishing unprotected write in the atomic section. *)
+      {st with rel = rel_local} (* Keep write local as if it were protected by the atomic section. *)
 
 
   let lock ask getg (st: relation_components_t) m =
@@ -573,6 +576,7 @@ struct
       {st with rel = rel'}
     )
     else
+      (* Atomic section locking is recursive. *)
       st (* sound w.r.t. recursive lock *)
 
   let unlock ask getg sideg (st: relation_components_t) m: relation_components_t =
@@ -585,6 +589,7 @@ struct
       {st with rel = rel_local}
     )
     else (
+      (* Publish delayed unprotected write as if it were protected by the atomic section. *)
       (* List.iter (fun var ->
           match AV.find_metadata var with
           | Some (Global g) -> sideg (V.mutex atomic_mutex) (RD.keep_vars rel [AV.global g])
@@ -596,6 +601,7 @@ struct
           | _ -> false
         )
       in
+      (* Unprotected invariant is one big relation. *)
       sideg (V.mutex atomic_mutex) rel_side;
       let rel_local =
         let newly_unprot var = match AV.find_metadata var with
@@ -958,6 +964,7 @@ struct
   let get_mutex_global_g_with_mutex_inits inits ask getg g =
     let get_mutex_global_g =
       if Param.handle_atomic then (
+        (* Unprotected invariant is one big relation. *)
         get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.mutex atomic_mutex)
         |> Cluster.keep_global g
       )
@@ -978,6 +985,7 @@ struct
     r
 
   let get_mutex_global_g_with_mutex_inits_atomic inits ask getg =
+    (* Unprotected invariant is one big relation. *)
     let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.mutex atomic_mutex) in
     if not inits then
       get_mutex_global_g
@@ -995,9 +1003,9 @@ struct
     (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
     let rel =
       if atomic && RD.mem_var rel (AV.global g) then
-        rel
+        rel (* Read previous unpublished unprotected write in current atomic section. *)
       else if atomic then
-        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits_atomic (not (LMust.mem lm lmust)) ask getg)
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits_atomic (not (LMust.mem lm lmust)) ask getg) (* Read unprotected invariant as full relation. *)
       else
         Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g)
     in
@@ -1017,7 +1025,7 @@ struct
       rel_local'
     )
     else
-      rel_local
+      rel_local (* Keep write local as if it were protected by the atomic section. *)
 
   let write_global ?(invariant=false) (ask:Q.ask) getg sideg (st: relation_components_t) g x: relation_components_t =
     let atomic = Param.handle_atomic && ask.f MustBeAtomic in
@@ -1029,9 +1037,9 @@ struct
     (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
     let rel =
       if atomic && RD.mem_var rel (AV.global g) then
-        rel
+        rel (* Read previous unpublished unprotected write in current atomic section. *)
       else if atomic then
-        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits_atomic (not (LMust.mem lm lmust)) ask getg)
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits_atomic (not (LMust.mem lm lmust)) ask getg) (* Read unprotected invariant as full relation. *)
       else
         Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g)
     in
@@ -1047,7 +1055,7 @@ struct
       let digest = Digest.current ask in
       let sidev = GMutex.singleton digest rel_side in
       if Param.handle_atomic then
-        sideg (V.mutex atomic_mutex) (G.create_global sidev)
+        sideg (V.mutex atomic_mutex) (G.create_global sidev) (* Unprotected invariant is one big relation. *)
       else
         sideg (V.global g) (G.create_global sidev);
       let l' = L.add lm rel_side l in
@@ -1060,7 +1068,8 @@ struct
       {rel = rel_local'; priv = (W.add g w,LMust.add lm lmust,l')}
     )
     else
-      {rel = rel_local; priv = (W.add g w,lmust,l)}
+      (* Delay publishing unprotected write in the atomic section. *)
+      {rel = rel_local; priv = (W.add g w,lmust,l)} (* Keep write local as if it were protected by the atomic section. *)
 
   let lock ask getg (st: relation_components_t) m =
     let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in
@@ -1076,6 +1085,7 @@ struct
       {st with rel}
     )
     else
+      (* Atomic section locking is recursive. *)
       st (* sound w.r.t. recursive lock *)
 
   let keep_only_globals ask m oct =
@@ -1106,6 +1116,7 @@ struct
         {rel = rel_local; priv = (w',LMust.add lm lmust,l')}
     )
     else (
+      (* Publish delayed unprotected write as if it were protected by the atomic section. *)
       let rel_local = remove_globals_unprotected_after_unlock ask m rel in
       let w' = W.filter (fun v -> not (is_unprotected_without ask v m)) w in
       let side_needed = not (W.is_empty w) in
@@ -1116,6 +1127,7 @@ struct
         let rel_side = Cluster.unlock w rel_side in
         let digest = Digest.current ask in
         let sidev = GMutex.singleton digest rel_side in
+        (* Unprotected invariant is one big relation. *)
         sideg (V.mutex atomic_mutex) (G.create_mutex sidev);
         let (lmust', l') = W.fold (fun g (lmust, l) ->
             let lm = LLock.global g in
@@ -1386,9 +1398,9 @@ let priv_module: (module S) Lazy.t =
          | "protection" -> (module ProtectionBasedPriv (struct let path_sensitive = false end))
          | "protection-path" -> (module ProtectionBasedPriv (struct let path_sensitive = true end))
          | "mutex-meet" -> (module PerMutexMeetPriv (NoAtomic))
-         | "mutex-meet-atomic" -> (module PerMutexMeetPriv (struct let handle_atomic = true end))
+         | "mutex-meet-atomic" -> (module PerMutexMeetPriv (struct let handle_atomic = true end)) (* experimental *)
          | "mutex-meet-tid" -> (module PerMutexMeetPrivTID (NoAtomic) (ThreadDigest) (NoCluster))
-         | "mutex-meet-tid-atomic" -> (module PerMutexMeetPrivTID (struct let handle_atomic = true end) (ThreadDigest) (NoCluster))
+         | "mutex-meet-tid-atomic" -> (module PerMutexMeetPrivTID (struct let handle_atomic = true end) (ThreadDigest) (NoCluster)) (* experimental *)
          | "mutex-meet-tid-cluster12" -> (module PerMutexMeetPrivTID (NoAtomic) (ThreadDigest) (DownwardClosedCluster (Clustering12)))
          | "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (NoAtomic) (ThreadDigest) (ArbitraryCluster (Clustering2)))
          | "mutex-meet-tid-cluster-max" -> (module PerMutexMeetPrivTID (NoAtomic) (ThreadDigest) (ArbitraryCluster (ClusteringMax)))
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index 2c8d32181f..66f2831c75 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -677,7 +677,7 @@ struct
     if P.mem x st.priv then
       CPA.find x st.cpa
     else if Param.handle_atomic && ask.f MustBeAtomic then
-      VD.join (CPA.find x st.cpa) (getg (V.unprotected x))
+      VD.join (CPA.find x st.cpa) (getg (V.unprotected x)) (* Account for previous unpublished unprotected writes in current atomic section. *)
     else if is_unprotected ask x then
       getg (V.unprotected x) (* CPA unnecessary because all values in GUnprot anyway *)
     else
@@ -686,13 +686,13 @@ struct
   let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v =
     if not invariant then (
       if not (Param.handle_atomic && ask.f MustBeAtomic) then
-        sideg (V.unprotected x) v;
+        sideg (V.unprotected x) v; (* Delay publishing unprotected write in the atomic section. *)
       if !earlyglobs then (* earlyglobs workaround for 13/60 *)
         sideg (V.protected x) v
         (* Unlock after invariant will still side effect refined value (if protected) from CPA, because cannot distinguish from non-invariant write since W is implicit. *)
     );
     if Param.handle_atomic && ask.f MustBeAtomic then
-      {st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv}
+      {st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv} (* Keep write local as if it were protected by the atomic section. *)
     else if is_unprotected ask x then
       st
     else
@@ -711,7 +711,7 @@ struct
           if not Param.check_read_unprotected || is_unprotected_without ask ~write:false x m then
             sideg (V.protected x) v;
           if atomic then
-            sideg (V.unprotected x) v;
+            sideg (V.unprotected x) v; (* Publish delayed unprotected write as if it were protected by the atomic section. *)
 
           if is_unprotected_without ask x m then (* is_in_V' *)
             {st with cpa = CPA.remove x st.cpa; priv = P.remove x st.priv}
@@ -1790,9 +1790,9 @@ let priv_module: (module S) Lazy.t =
         | "mutex-meet" -> (module PerMutexMeetPriv)
         | "mutex-meet-tid" -> (module PerMutexMeetTIDPriv (ThreadDigest))
         | "protection" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = false end))
-        | "protection-atomic" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = true end))
+        | "protection-atomic" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = true end)) (* experimental *)
         | "protection-read" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = false end))
-        | "protection-read-atomic" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = true end))
+        | "protection-read-atomic" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = true end)) (* experimental *)
         | "mine" -> (module MinePriv)
         | "mine-nothread" -> (module MineNoThreadPriv)
         | "mine-W" -> (module MineWPriv (struct let side_effect_global_init = true end))
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index dafc3bdf1d..627b39166e 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -12,7 +12,7 @@ module VD     = BaseDomain.VD
 module type AtomicParam =
 sig
   val handle_atomic: bool
-  (** Whether to handle SV-COMP atomic blocks. *)
+  (** Whether to handle SV-COMP atomic blocks (experimental). *)
 end
 
 module NoAtomic: AtomicParam =