Merge branch 'interactive' into interactive_postsolver_pruning

Author: michael-schwarz

src/solvers/td3.ml

@@ -548,6 +548,9 @@ module WP =
 
       start_event ();
 
+      (* reluctantly unchanged return nodes to additionally query for postsolving to get warnings, etc. *)
+      let reluctant_vs: S.Var.t list ref = ref [] in
+
       if GobConfig.get_bool "incremental.load" then (
         let c = S.increment.changes in
         List.(Printf.printf "change_info = { unchanged = %d; changed = %d; added = %d; removed = %d }\n" (length c.unchanged) (length c.changed) (length c.added) (length c.removed));
@@ -745,7 +748,7 @@ module WP =
         print_endline "Removing data for changed and removed functions...";
         let delete_marked s = HM.iter (fun k _ -> HM.remove s k) marked_for_deletion in
         delete_marked rho;
-        delete_marked infl;
+        delete_marked infl; (* TODO: delete from inner sets? *)
         delete_marked wpoint;
         delete_marked dep;
 
@@ -835,8 +838,15 @@ module WP =
         );
 
         delete_marked stable;
-        delete_marked side_dep;
-        delete_marked side_infl;
+        delete_marked side_dep; (* TODO: delete from inner sets? *)
+        delete_marked side_infl; (* TODO: delete from inner sets? *)
+
+        (* delete from incremental postsolving/warning structures to remove spurious warnings *)
+        delete_marked superstable;
+        delete_marked var_messages;
+        delete_marked rho_write;
+        HM.iter (fun x w -> delete_marked w) rho_write;
+
         print_data data "Data after clean-up";
 
         (* TODO: reluctant doesn't call destabilize on removed functions or old copies of modified functions (e.g. after removing write), so those globals don't get restarted *)
@@ -854,6 +864,10 @@ module WP =
                 destabilize x;
                 HM.replace stable x ()
               )
+              else (
+                print_endline "Destabilization not required...";
+                reluctant_vs := x :: !reluctant_vs
+              )
             ) old_ret;
 
           print_endline "Final solve..."
@@ -1012,7 +1026,7 @@ module WP =
               Option.may (VS.iter one_var') (HM.find_option side_infl x)
             )
           in
-          (Stats.time "cheap_full_reach" (List.iter one_var')) vs;
+          (Stats.time "cheap_full_reach" (List.iter one_var')) (vs @ !reluctant_vs);
 
           reachable_and_superstable (* consider superstable reached if it is still reachable: stop recursion (evaluation) and keep from being pruned *)
         else
@@ -1124,7 +1138,7 @@ module WP =
 
       let module Post = PostSolver.MakeIncrList (MakeIncrListArg) in
 
-      Post.post st vs rho;
+      Post.post st (!reluctant_vs @ vs) rho;
 
       print_data data "Data after postsolve";
 

tests/incremental/13-restart-write/06-mutex-simple-reluctant.c

@@ -0,0 +1,23 @@
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  myglobal=myglobal+1; // RACE!
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_mutex_lock(&mutex2);
+  myglobal=myglobal+1; // RACE!
+  pthread_mutex_unlock(&mutex2);
+  pthread_join (id, NULL);
+  return 0;
+}

tests/incremental/13-restart-write/06-mutex-simple-reluctant.json

@@ -0,0 +1,12 @@
+{
+    "incremental": {
+        "restart": {
+            "sided": {
+                "enabled": false
+            }
+        },
+        "reluctant": {
+            "on": true
+        }
+    }
+}

tests/incremental/13-restart-write/06-mutex-simple-reluctant.patch

@@ -0,0 +1,24 @@
+--- tests/incremental/13-restart-write/06-mutex-simple-reluctant.c
++++ tests/incremental/13-restart-write/06-mutex-simple-reluctant.c
+@@ -7,7 +7,7 @@ pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+
+ void *t_fun(void *arg) {
+   pthread_mutex_lock(&mutex1);
+-  myglobal=myglobal+1; // RACE!
++  myglobal=myglobal+1; // NORACE
+   pthread_mutex_unlock(&mutex1);
+   return NULL;
+ }
+@@ -15,9 +15,9 @@ void *t_fun(void *arg) {
+ int main(void) {
+   pthread_t id;
+   pthread_create(&id, NULL, t_fun, NULL);
+-  pthread_mutex_lock(&mutex2);
+-  myglobal=myglobal+1; // RACE!
+-  pthread_mutex_unlock(&mutex2);
++  pthread_mutex_lock(&mutex1);
++  myglobal=myglobal+1; // NORACE
++  pthread_mutex_unlock(&mutex1);
+   pthread_join (id, NULL);
+   return 0;
+ }

tests/incremental/13-restart-write/07-mutex-simple-reluctant2.c

@@ -0,0 +1,23 @@
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  myglobal=myglobal+1; // RACE!
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_mutex_lock(&mutex2);
+  myglobal=myglobal+1; // RACE!
+  pthread_mutex_unlock(&mutex2);
+  pthread_join (id, NULL);
+  return 0;
+}

tests/incremental/13-restart-write/07-mutex-simple-reluctant2.json

@@ -0,0 +1,12 @@
+{
+    "incremental": {
+        "restart": {
+            "sided": {
+                "enabled": false
+            }
+        },
+        "reluctant": {
+            "on": true
+        }
+    }
+}

tests/incremental/13-restart-write/07-mutex-simple-reluctant2.patch

@@ -0,0 +1,11 @@
+--- tests/incremental/13-restart-write/07-mutex-simple-reluctant2.c
++++ tests/incremental/13-restart-write/07-mutex-simple-reluctant2.c
+@@ -7,7 +7,7 @@ pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+
+ void *t_fun(void *arg) {
+   pthread_mutex_lock(&mutex1);
+-  myglobal=myglobal+1; // RACE!
++  myglobal=myglobal+2; // RACE!
+   pthread_mutex_unlock(&mutex1);
+   return NULL;
+ }

tests/incremental/13-restart-write/08-mutex-simple-reluctant3.c

@@ -0,0 +1,22 @@
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_mutex_lock(&mutex2);
+  myglobal=myglobal+1; // NORACE
+  pthread_mutex_unlock(&mutex2);
+  pthread_join (id, NULL);
+  return 0;
+}

tests/incremental/13-restart-write/08-mutex-simple-reluctant3.json

@@ -0,0 +1,12 @@
+{
+    "incremental": {
+        "restart": {
+            "sided": {
+                "enabled": false
+            }
+        },
+        "reluctant": {
+            "on": true
+        }
+    }
+}

tests/incremental/13-restart-write/08-mutex-simple-reluctant3.patch

@@ -0,0 +1,19 @@
+--- tests/incremental/13-restart-write/08-mutex-simple-reluctant3.c
++++ tests/incremental/13-restart-write/08-mutex-simple-reluctant3.c
+@@ -7,6 +7,7 @@ pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+
+ void *t_fun(void *arg) {
+   pthread_mutex_lock(&mutex1);
++  myglobal=myglobal+1; // RACE!
+   pthread_mutex_unlock(&mutex1);
+   return NULL;
+ }
+@@ -15,7 +16,7 @@ int main(void) {
+   pthread_t id;
+   pthread_create(&id, NULL, t_fun, NULL);
+   pthread_mutex_lock(&mutex2);
+-  myglobal=myglobal+1; // NORACE
++  myglobal=myglobal+1; // RACE!
+   pthread_mutex_unlock(&mutex2);
+   pthread_join (id, NULL);
+   return 0;