Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Incremental TD3: limit side-effected restarting using fuel #629

Merged
merged 9 commits into from
May 23, 2022
65 changes: 44 additions & 21 deletions src/solvers/td3.ml
Original file line number Diff line number Diff line change
Expand Up @@ -366,6 +366,8 @@ module WP =
(* reluctantly unchanged return nodes to additionally query for postsolving to get warnings, etc. *)
let reluctant_vs: S.Var.t list ref = ref [] in

let restart_write_only = GobConfig.get_bool "incremental.restart.write-only" 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));
Expand All @@ -386,9 +388,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 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 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
Expand All @@ -398,7 +403,7 @@ module WP =
if restart_only_access then
S.Var.is_write_only x
else
(not restart_only_globals || Node.equal (S.Var.node x) (Function Cil.dummyFunDec)) && (not (S.Var.is_write_only x))
(not restart_only_globals || Node.equal (S.Var.node x) (Function Cil.dummyFunDec)) && (not (S.Var.is_write_only x) || not restart_write_only)
in

if not (VS.is_empty w) && should_restart then (
Expand All @@ -412,7 +417,7 @@ module WP =
HM.remove stable y;
HM.remove superstable y;
if restart_destab_with_sides then
destabilize_with_side y
destabilize_with_side ~side_fuel y
else
destabilize_normal y
) w
Expand All @@ -426,25 +431,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 y
destabilize_with_side ~side_fuel 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 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' 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;

Expand Down Expand Up @@ -856,12 +876,15 @@ module WP =
HM.create 0 (* doesn't matter, not used *)
in

(* restart write-only *)
HM.iter (fun x w ->
HM.iter (fun y d ->
HM.replace rho y (S.Dom.bot ());
) w
) rho_write;
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
);
Comment on lines +879 to +887
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I just brought this PR up to date with all the interactive branch improvements and noticed that the restarting of write-only unknowns during postprocessing was actually doing some of the restarting that a few of the previously added fuel tests were checking (so the tests didn't pass or didn't check anything meaningful about fuel).

Hence I added another option to disable the write-only restarting during postprocessing.
But now I'm very confused about #703 and this because:

  1. With Restarting of Access globals as a baseline for the incremental solver #703 and incremental postsolver disabled, we were still restarting the write-only during postprocessing here, even with the non-incremental postsolver.
  2. But if this is the case, then isn't Restarting of Access globals as a baseline for the incremental solver #703 completely redundant because for the comparison benchmark one can just disable the incremental postsolver, but have this restarting still take place, without having to have any only-access and fuel things for the general side effect restarting.

cc: @michael-schwarz

Copy link
Member

@michael-schwarz michael-schwarz May 23, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, now I am confused. We want to have three possible settings:

  1. No incremental post-solver at all, restarting of accesses globals (by destabilizing everything that has a side-effect on an access global)
  2. Incremental post-solver without our write-only global insight (by destabilizing everything that has a side-effect on an access global)
  3. Incremental post-solver with our write-only global insight (by not explicitly destabilizing things that have a side-effect on an access global, and reusing side-effects from unknowns that remain superstable & reachable)

It seems to me that we need special handling for the second thing here? What am I missing?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree with the sequence of settings:

  • 1 → 2 enables incremental postsolver,
  • 2 → 3 enables write-only restarting during postprocessing (as opposed to preprocessing, which gives us the general restarting).

My point is that at the time, there was no option to disable write-only restarting during postprocessing (it was unconditionally enabled). I only added such option here in this PR later.
This means that configurations 1 and 2 were impossible to achieve on the interactive branch. With general restarting enabled, but limited to only-access, and disabling your destab-with-side (or similarly using fuel 1), the write-only unknowns got restarted twice: first during the preprocessing restarting and then also during the postprocessing restarting.

So indeed, to get that sequence of changes we need fuel 1 only-access restarting, but it also means those benchmarks were even more flawed than just the issue with destab-with-side ending up with excessive restarting.
When writing my previous comment, I think I implicitly assumed there wasn't another flaw and so only a single direct benchmark comparison like 1 → 3 made sense in my head, which is how I also got confused and thought neither destab-with-side nor fuel would be necessary.

Anyway, I'll go forward with getting fuel merged to interactive as decided last week, but this realization means that the incremental.restart.write-only option (added just here) is also crucial for doing the re-benchmarking. I hope this doesn't cause a difference in results (the enabled and accidentally excessive destab-with-side only-access restarting probably dominates the special write-only restarting).


if incr_verify then (
HM.filteri_inplace (fun x _ -> HM.mem reachable_and_superstable x) var_messages;
Expand Down
18 changes: 18 additions & 0 deletions src/util/options.schema.json
Original file line number Diff line number Diff line change
Expand Up @@ -1062,6 +1062,18 @@
"description" : "TODO BROKEN",
"type" : "boolean",
"default" : true
},
"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
Expand All @@ -1074,6 +1086,12 @@
"type": "string"
},
"default": []
},
"write-only": {
"title": "incremental.restart.write-only",
"description": "TODO",
"type": "boolean",
"default": true
}
},
"additionalProperties": false
Expand Down
27 changes: 27 additions & 0 deletions tests/incremental/11-restart/14-mutex-simple-wrap2.c
Original file line number Diff line number Diff line change
@@ -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;
}
11 changes: 11 additions & 0 deletions tests/incremental/11-restart/14-mutex-simple-wrap2.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
{
"incremental": {
"restart": {
"sided": {
"enabled": true,
"fuel": 2
},
"write-only": false
}
}
}
22 changes: 22 additions & 0 deletions tests/incremental/11-restart/14-mutex-simple-wrap2.patch
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
--- tests/incremental/11-restart/14-mutex-simple-wrap2.c
+++ tests/incremental/11-restart/14-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) {
27 changes: 27 additions & 0 deletions tests/incremental/11-restart/15-mutex-simple-wrap1.c
Original file line number Diff line number Diff line change
@@ -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;
}
11 changes: 11 additions & 0 deletions tests/incremental/11-restart/15-mutex-simple-wrap1.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
{
"incremental": {
"restart": {
"sided": {
"enabled": true,
"fuel": 1
},
"write-only": false
}
}
}
22 changes: 22 additions & 0 deletions tests/incremental/11-restart/15-mutex-simple-wrap1.patch
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
--- tests/incremental/11-restart/15-mutex-simple-wrap1.c
+++ tests/incremental/11-restart/15-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) {
27 changes: 27 additions & 0 deletions tests/incremental/11-restart/16-mutex-simple-wrap1-global.c
Original file line number Diff line number Diff line change
@@ -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;
}
12 changes: 12 additions & 0 deletions tests/incremental/11-restart/16-mutex-simple-wrap1-global.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
{
"incremental": {
"restart": {
"sided": {
"enabled": true,
"fuel": 1,
"fuel-only-global": true
},
"write-only": false
}
}
}
22 changes: 22 additions & 0 deletions tests/incremental/11-restart/16-mutex-simple-wrap1-global.patch
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
--- tests/incremental/11-restart/16-mutex-simple-wrap1-global.c
+++ tests/incremental/11-restart/16-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) {
23 changes: 23 additions & 0 deletions tests/incremental/11-restart/17-mutex-simple-fuel.c
Original file line number Diff line number Diff line change
@@ -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;
}
11 changes: 11 additions & 0 deletions tests/incremental/11-restart/17-mutex-simple-fuel.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
{
"incremental": {
"restart": {
"sided": {
"enabled": true,
"fuel": 1
},
"write-only": false
}
}
}
Loading