Incremental TD3: limit side-effected restarting using fuel

src/solvers/td3.ml

@@ -542,9 +542,12 @@ module WP =
             ()
         in
 
+        let restart_fuel_only_globals = GobConfig.get_bool "incremental.restart.sided.fuel-only-global" in
+
         (* destabilize which restarts side-effected vars *)
-        let rec destabilize_with_side ?(front=true) x =
-          if tracing then trace "sol2" "destabilize_with_side %a\n" S.Var.pretty_trace x;
+        (* side_fuel specifies how many times (in recursion depth) to destabilize side_infl, None means infinite *)
+        let rec destabilize_with_side ~side_fuel ?(front=true) x =
+          if tracing then trace "sol2" "destabilize_with_side %a %a\n" S.Var.pretty_trace x (Pretty.docOpt (Pretty.dprintf "%d")) side_fuel;
 
           (* is side-effected var (global/function entry)? *)
           let w = HM.find_default side_dep x VS.empty in
@@ -563,7 +566,7 @@ module WP =
                 if tracing then trace "sol2" "stable remove %a\n" S.Var.pretty_trace y;
                 HM.remove stable y;
                 HM.remove superstable y;
-                destabilize_with_side ~front:false y
+                destabilize_with_side ~side_fuel ~front:false y
               ) w
           );
 
@@ -576,25 +579,40 @@ module WP =
               if tracing then trace "sol2" "stable remove %a\n" S.Var.pretty_trace y;
               HM.remove stable y;
               HM.remove superstable y;
-              destabilize_with_side ~front:false y
+              destabilize_with_side ~side_fuel ~front:false y
             ) w;
 
           (* destabilize side infl *)
           let w = HM.find_default side_infl x VS.empty in
           HM.remove side_infl x;
-          (* TODO: should this also be conditional on restart_only_globals? right now goes through function entry side effects, but just doesn't restart them *)
-          VS.iter (fun y ->
-              if tracing then trace "sol2" "destabilize_with_side %a side_infl %a\n" S.Var.pretty_trace x S.Var.pretty_trace y;
-              if tracing then trace "sol2" "stable remove %a\n" S.Var.pretty_trace y;
-              HM.remove stable y;
-              HM.remove superstable y;
-              destabilize_with_side ~front:false y
-            ) w
+
+          if side_fuel <> Some 0 then ( (* non-0 or infinite fuel is fine *)
+            let side_fuel' =
+              if not restart_fuel_only_globals || Node.equal (S.Var.node x) (Function Cil.dummyFunDec) then
+                Option.map Int.pred side_fuel
+              else
+                side_fuel (* don't decrease fuel for function entry side effect *)
+            in
+            (* TODO: should this also be conditional on restart_only_globals? right now goes through function entry side effects, but just doesn't restart them *)
+            VS.iter (fun y ->
+                if tracing then trace "sol2" "destabilize_with_side %a side_infl %a\n" S.Var.pretty_trace x S.Var.pretty_trace y;
+                if tracing then trace "sol2" "stable remove %a\n" S.Var.pretty_trace y;
+                HM.remove stable y;
+                HM.remove superstable y;
+                destabilize_with_side ~side_fuel:side_fuel' ~front:false y
+              ) w
+          )
         in
 
         destabilize_ref :=
-          if restart_sided then
-            destabilize_with_side
+          if restart_sided then (
+            let side_fuel =
+              match GobConfig.get_int "incremental.restart.sided.fuel" with
+              | fuel when fuel >= 0 -> Some fuel
+              | _ -> None (* infinite *)
+            in
+            destabilize_with_side ~side_fuel
+          )
           else
             destabilize_normal;
 

src/util/options.schema.json

@@ -961,6 +961,18 @@
                   "description": "TODO",
                   "type": "boolean",
                   "default": false
+                },
+                "fuel": {
+                  "title": "incremental.restart.sided.fuel",
+                  "description": "TODO",
+                  "type": "integer",
+                  "default": -1
+                },
+                "fuel-only-global": {
+                  "title": "incremental.restart.sided.fuel-only-global",
+                  "description": "TODO",
+                  "type": "boolean",
+                  "default": false
                 }
               },
               "additionalProperties": false

tests/incremental/11-restart/12-mutex-simple.json

@@ -2,7 +2,8 @@
     "incremental": {
         "restart": {
             "sided": {
-                "enabled": false
+                "enabled": true,
+                "fuel": 1
             }
         }
     }

tests/incremental/11-restart/13-mutex-simple-wrap2.c

@@ -0,0 +1,27 @@
+#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;
+}
+
+void wrap() {
+  pthread_mutex_lock(&mutex2);
+  myglobal=myglobal+1; // RACE!
+  pthread_mutex_unlock(&mutex2);
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  wrap();
+  pthread_join (id, NULL);
+  return 0;
+}

tests/incremental/11-restart/13-mutex-simple-wrap2.json

@@ -0,0 +1,10 @@
+{
+    "incremental": {
+        "restart": {
+            "sided": {
+                "enabled": true,
+                "fuel": 2
+            }
+        }
+    }
+}

tests/incremental/11-restart/13-mutex-simple-wrap2.patch

@@ -0,0 +1,22 @@
+--- tests/incremental/11-restart/13-mutex-simple-wrap2.c
++++ tests/incremental/11-restart/13-mutex-simple-wrap2.c
+@@ -7,15 +7,15 @@ 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;
+ }
+
+ void wrap() {
+-  pthread_mutex_lock(&mutex2);
+-  myglobal=myglobal+1; // RACE!
+-  pthread_mutex_unlock(&mutex2);
++  pthread_mutex_lock(&mutex1);
++  myglobal=myglobal+1; // NORACE
++  pthread_mutex_unlock(&mutex1);
+ }
+
+ int main(void) {

tests/incremental/11-restart/14-mutex-simple-wrap1.c

@@ -0,0 +1,27 @@
+#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;
+}
+
+void wrap() {
+  pthread_mutex_lock(&mutex2);
+  myglobal=myglobal+1; // RACE!
+  pthread_mutex_unlock(&mutex2);
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  wrap();
+  pthread_join (id, NULL);
+  return 0;
+}

tests/incremental/11-restart/14-mutex-simple-wrap1.json

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

tests/incremental/11-restart/14-mutex-simple-wrap1.patch

@@ -0,0 +1,22 @@
+--- tests/incremental/11-restart/14-mutex-simple-wrap1.c
++++ tests/incremental/11-restart/14-mutex-simple-wrap1.c
+@@ -7,15 +7,15 @@ pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+
+ void *t_fun(void *arg) {
+   pthread_mutex_lock(&mutex1);
+-  myglobal=myglobal+1; // RACE!
++  myglobal=myglobal+1; // RACE (not enough fuel)
+   pthread_mutex_unlock(&mutex1);
+   return NULL;
+ }
+
+ void wrap() {
+-  pthread_mutex_lock(&mutex2);
+-  myglobal=myglobal+1; // RACE!
+-  pthread_mutex_unlock(&mutex2);
++  pthread_mutex_lock(&mutex1);
++  myglobal=myglobal+1; // RACE (not enough fuel)
++  pthread_mutex_unlock(&mutex1);
+ }
+
+ int main(void) {

tests/incremental/11-restart/15-mutex-simple-wrap1-global.c

@@ -0,0 +1,27 @@
+#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;
+}
+
+void wrap() {
+  pthread_mutex_lock(&mutex2);
+  myglobal=myglobal+1; // RACE!
+  pthread_mutex_unlock(&mutex2);
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  wrap();
+  pthread_join (id, NULL);
+  return 0;
+}

tests/incremental/11-restart/15-mutex-simple-wrap1-global.json

@@ -0,0 +1,11 @@
+{
+    "incremental": {
+        "restart": {
+            "sided": {
+                "enabled": true,
+                "fuel": 1,
+                "fuel-only-global": true
+            }
+        }
+    }
+}

tests/incremental/11-restart/15-mutex-simple-wrap1-global.patch

@@ -0,0 +1,22 @@
+--- tests/incremental/11-restart/15-mutex-simple-wrap1-global.c
++++ tests/incremental/11-restart/15-mutex-simple-wrap1-global.c
+@@ -7,15 +7,15 @@ 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;
+ }
+
+ void wrap() {
+-  pthread_mutex_lock(&mutex2);
+-  myglobal=myglobal+1; // RACE!
+-  pthread_mutex_unlock(&mutex2);
++  pthread_mutex_lock(&mutex1);
++  myglobal=myglobal+1; // NORACE
++  pthread_mutex_unlock(&mutex1);
+ }
+
+ int main(void) {