Fix incremental write-only restarting for side effects from deleted nodes

src/solvers/td3.ml

@@ -712,6 +712,17 @@ module Base =
         (* delete from incremental postsolving/warning structures to remove spurious warnings *)
         delete_marked superstable;
         delete_marked var_messages;
+
+        if restart_write_only then (
+          (* restart write-only *)
+          (* before delete_marked because we also want to restart write-only side effects from deleted nodes *)
+          HM.iter (fun x w ->
+              HM.iter (fun y d ->
+                  ignore (Pretty.printf "Restarting write-only to bot %a\n" S.Var.pretty_trace y);
+                  HM.replace rho y (S.Dom.bot ());
+                ) w
+            ) rho_write
+        );
         delete_marked rho_write;
         HM.iter (fun x w -> delete_marked w) rho_write;
 
@@ -905,16 +916,6 @@ module Base =
           HM.create 0 (* doesn't matter, not used *)
       in
 
-      if restart_write_only then (
-        (* restart write-only *)
-        HM.iter (fun x w ->
-            HM.iter (fun y d ->
-                ignore (Pretty.printf "Restarting write-only to bot %a\n" S.Var.pretty_trace y);
-                HM.replace rho y (S.Dom.bot ());
-              ) w
-          ) rho_write
-      );
-
       if incr_verify then (
         HM.filteri_inplace (fun x _ -> HM.mem reachable_and_superstable x) var_messages;
         HM.filteri_inplace (fun x _ -> HM.mem reachable_and_superstable x) rho_write

tests/incremental/13-restart-write/09-mutex-self-fix.c

@@ -0,0 +1,17 @@
+#include <pthread.h>
+
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+int g;
+
+void *t_fun(void *arg) {
+  g++; // RACE!
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  while (1) {
+    pthread_create(&id, NULL, t_fun, NULL);
+  }
+  return 0;
+}

tests/incremental/13-restart-write/09-mutex-self-fix.json

@@ -0,0 +1,10 @@
+{
+  "incremental": {
+    "restart": {
+      "sided": {
+        "enabled": false
+      },
+      "write-only": true
+    }
+  }
+}

tests/incremental/13-restart-write/09-mutex-self-fix.patch

@@ -0,0 +1,13 @@
+--- tests/incremental/13-restart-write/09-mutex-self-fix.c
++++ tests/incremental/13-restart-write/09-mutex-self-fix.c
+@@ -4,7 +4,9 @@ pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+ int g;
+
+ void *t_fun(void *arg) {
+-  g++; // RACE!
++  pthread_mutex_lock(&A);
++  g++; // NORACE
++  pthread_mutex_unlock(&A);
+   return NULL;
+ }
+