Skip to content

Commit 49d319e

Browse files
sim642sim642
authored
Merge pull request #629 from goblint/restart-sided-fuel
Incremental TD3: limit side-effected restarting using fuel
2 parents da790e0 + 77b3fca commit 49d319e

14 files changed

+302
-22
lines changed

‎src/solvers/td3.ml‎

Lines changed: 44 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -366,6 +366,8 @@ module WP =
366366
(* reluctantly unchanged return nodes to additionally query for postsolving to get warnings, etc. *)
367367
let reluctant_vs: S.Var.t list ref = ref [] in
368368

369+
let restart_write_only = GobConfig.get_bool "incremental.restart.write-only" in
370+
369371
if GobConfig.get_bool "incremental.load" then (
370372
let c = S.increment.changes in
371373
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));
@@ -386,9 +388,12 @@ module WP =
386388
()
387389
in
388390

391+
let restart_fuel_only_globals = GobConfig.get_bool "incremental.restart.sided.fuel-only-global" in
392+
389393
(* destabilize which restarts side-effected vars *)
390-
let rec destabilize_with_side x =
391-
if tracing then trace "sol2" "destabilize_with_side %a\n" S.Var.pretty_trace x;
394+
(* side_fuel specifies how many times (in recursion depth) to destabilize side_infl, None means infinite *)
395+
let rec destabilize_with_side ~side_fuel x =
396+
if tracing then trace "sol2" "destabilize_with_side %a %a\n" S.Var.pretty_trace x (Pretty.docOpt (Pretty.dprintf "%d")) side_fuel;
392397

393398
(* is side-effected var (global/function entry)? *)
394399
let w = HM.find_default side_dep x VS.empty in
@@ -398,7 +403,7 @@ module WP =
398403
if restart_only_access then
399404
S.Var.is_write_only x
400405
else
401-
(not restart_only_globals || Node.equal (S.Var.node x) (Function Cil.dummyFunDec)) && (not (S.Var.is_write_only x))
406+
(not restart_only_globals || Node.equal (S.Var.node x) (Function Cil.dummyFunDec)) && (not (S.Var.is_write_only x) || not restart_write_only)
402407
in
403408

404409
if not (VS.is_empty w) && should_restart then (
@@ -412,7 +417,7 @@ module WP =
412417
HM.remove stable y;
413418
HM.remove superstable y;
414419
if restart_destab_with_sides then
415-
destabilize_with_side y
420+
destabilize_with_side ~side_fuel y
416421
else
417422
destabilize_normal y
418423
) w
@@ -426,25 +431,40 @@ module WP =
426431
if tracing then trace "sol2" "stable remove %a\n" S.Var.pretty_trace y;
427432
HM.remove stable y;
428433
HM.remove superstable y;
429-
destabilize_with_side y
434+
destabilize_with_side ~side_fuel y
430435
) w;
431436

432437
(* destabilize side infl *)
433438
let w = HM.find_default side_infl x VS.empty in
434439
HM.remove side_infl x;
435-
(* TODO: should this also be conditional on restart_only_globals? right now goes through function entry side effects, but just doesn't restart them *)
436-
VS.iter (fun y ->
437-
if tracing then trace "sol2" "destabilize_with_side %a side_infl %a\n" S.Var.pretty_trace x S.Var.pretty_trace y;
438-
if tracing then trace "sol2" "stable remove %a\n" S.Var.pretty_trace y;
439-
HM.remove stable y;
440-
HM.remove superstable y;
441-
destabilize_with_side y
442-
) w
440+
441+
if side_fuel <> Some 0 then ( (* non-0 or infinite fuel is fine *)
442+
let side_fuel' =
443+
if not restart_fuel_only_globals || Node.equal (S.Var.node x) (Function Cil.dummyFunDec) then
444+
Option.map Int.pred side_fuel
445+
else
446+
side_fuel (* don't decrease fuel for function entry side effect *)
447+
in
448+
(* TODO: should this also be conditional on restart_only_globals? right now goes through function entry side effects, but just doesn't restart them *)
449+
VS.iter (fun y ->
450+
if tracing then trace "sol2" "destabilize_with_side %a side_infl %a\n" S.Var.pretty_trace x S.Var.pretty_trace y;
451+
if tracing then trace "sol2" "stable remove %a\n" S.Var.pretty_trace y;
452+
HM.remove stable y;
453+
HM.remove superstable y;
454+
destabilize_with_side ~side_fuel:side_fuel' y
455+
) w
456+
)
443457
in
444458

445459
destabilize_ref :=
446-
if restart_sided then
447-
destabilize_with_side
460+
if restart_sided then (
461+
let side_fuel =
462+
match GobConfig.get_int "incremental.restart.sided.fuel" with
463+
| fuel when fuel >= 0 -> Some fuel
464+
| _ -> None (* infinite *)
465+
in
466+
destabilize_with_side ~side_fuel
467+
)
448468
else
449469
destabilize_normal;
450470

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

859-
(* restart write-only *)
860-
HM.iter (fun x w ->
861-
HM.iter (fun y d ->
862-
HM.replace rho y (S.Dom.bot ());
863-
) w
864-
) rho_write;
879+
if restart_write_only then (
880+
(* restart write-only *)
881+
HM.iter (fun x w ->
882+
HM.iter (fun y d ->
883+
ignore (Pretty.printf "Restarting write-only to bot %a\n" S.Var.pretty_trace y);
884+
HM.replace rho y (S.Dom.bot ());
885+
) w
886+
) rho_write
887+
);
865888

866889
if incr_verify then (
867890
HM.filteri_inplace (fun x _ -> HM.mem reachable_and_superstable x) var_messages;

‎src/util/options.schema.json‎

Lines changed: 19 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1047,7 +1047,7 @@
10471047
},
10481048
"only-global": {
10491049
"title": "incremental.restart.sided.only-global",
1050-
"description": "Restart only constraint system globals.",
1050+
"description": "Restart only constraint system globals (not function entry nodes).",
10511051
"type": "boolean",
10521052
"default": false
10531053
},
@@ -1062,6 +1062,18 @@
10621062
"description" : "TODO BROKEN",
10631063
"type" : "boolean",
10641064
"default" : true
1065+
},
1066+
"fuel": {
1067+
"title": "incremental.restart.sided.fuel",
1068+
"description": "Initial fuel for bounding transitive restarting, which uses one fuel each time when following side_fuel to restart. Zero fuel never restarts. Negative fuel doesn't bound (infinite fuel).",
1069+
"type": "integer",
1070+
"default": -1
1071+
},
1072+
"fuel-only-global": {
1073+
"title": "incremental.restart.sided.fuel-only-global",
1074+
"description": "Decrease fuel only when going to constraint system globals (not function entry nodes).",
1075+
"type": "boolean",
1076+
"default": false
10651077
}
10661078
},
10671079
"additionalProperties": false
@@ -1074,6 +1086,12 @@
10741086
"type": "string"
10751087
},
10761088
"default": []
1089+
},
1090+
"write-only": {
1091+
"title": "incremental.restart.write-only",
1092+
"description": "Restart write-only variables to bot during postprocessing.",
1093+
"type": "boolean",
1094+
"default": true
10771095
}
10781096
},
10791097
"additionalProperties": false

‎tests/incremental/11-restart/14-mutex-simple-wrap2.c‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
#include <pthread.h>
2+
#include <stdio.h>
3+
4+
int myglobal;
5+
pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
6+
pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
7+
8+
void *t_fun(void *arg) {
9+
pthread_mutex_lock(&mutex1);
10+
myglobal=myglobal+1; // RACE!
11+
pthread_mutex_unlock(&mutex1);
12+
return NULL;
13+
}
14+
15+
void wrap() {
16+
pthread_mutex_lock(&mutex2);
17+
myglobal=myglobal+1; // RACE!
18+
pthread_mutex_unlock(&mutex2);
19+
}
20+
21+
int main(void) {
22+
pthread_t id;
23+
pthread_create(&id, NULL, t_fun, NULL);
24+
wrap();
25+
pthread_join (id, NULL);
26+
return 0;
27+
}

‎tests/incremental/11-restart/14-mutex-simple-wrap2.json‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
{
2+
"incremental": {
3+
"restart": {
4+
"sided": {
5+
"enabled": true,
6+
"fuel": 2
7+
},
8+
"write-only": false
9+
}
10+
}
11+
}

‎tests/incremental/11-restart/14-mutex-simple-wrap2.patch‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
--- tests/incremental/11-restart/14-mutex-simple-wrap2.c
2+
+++ tests/incremental/11-restart/14-mutex-simple-wrap2.c
3+
@@ -7,15 +7,15 @@ pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
4+
5+
void *t_fun(void *arg) {
6+
pthread_mutex_lock(&mutex1);
7+
- myglobal=myglobal+1; // RACE!
8+
+ myglobal=myglobal+1; // NORACE
9+
pthread_mutex_unlock(&mutex1);
10+
return NULL;
11+
}
12+
13+
void wrap() {
14+
- pthread_mutex_lock(&mutex2);
15+
- myglobal=myglobal+1; // RACE!
16+
- pthread_mutex_unlock(&mutex2);
17+
+ pthread_mutex_lock(&mutex1);
18+
+ myglobal=myglobal+1; // NORACE
19+
+ pthread_mutex_unlock(&mutex1);
20+
}
21+
22+
int main(void) {

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

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
#include <pthread.h>
2+
#include <stdio.h>
3+
4+
int myglobal;
5+
pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
6+
pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
7+
8+
void *t_fun(void *arg) {
9+
pthread_mutex_lock(&mutex1);
10+
myglobal=myglobal+1; // RACE!
11+
pthread_mutex_unlock(&mutex1);
12+
return NULL;
13+
}
14+
15+
void wrap() {
16+
pthread_mutex_lock(&mutex2);
17+
myglobal=myglobal+1; // RACE!
18+
pthread_mutex_unlock(&mutex2);
19+
}
20+
21+
int main(void) {
22+
pthread_t id;
23+
pthread_create(&id, NULL, t_fun, NULL);
24+
wrap();
25+
pthread_join (id, NULL);
26+
return 0;
27+
}

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

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
{
2+
"incremental": {
3+
"restart": {
4+
"sided": {
5+
"enabled": true,
6+
"fuel": 1
7+
},
8+
"write-only": false
9+
}
10+
}
11+
}

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

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
--- tests/incremental/11-restart/15-mutex-simple-wrap1.c
2+
+++ tests/incremental/11-restart/15-mutex-simple-wrap1.c
3+
@@ -7,15 +7,15 @@ pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
4+
5+
void *t_fun(void *arg) {
6+
pthread_mutex_lock(&mutex1);
7+
- myglobal=myglobal+1; // RACE!
8+
+ myglobal=myglobal+1; // RACE (not enough fuel)
9+
pthread_mutex_unlock(&mutex1);
10+
return NULL;
11+
}
12+
13+
void wrap() {
14+
- pthread_mutex_lock(&mutex2);
15+
- myglobal=myglobal+1; // RACE!
16+
- pthread_mutex_unlock(&mutex2);
17+
+ pthread_mutex_lock(&mutex1);
18+
+ myglobal=myglobal+1; // RACE (not enough fuel)
19+
+ pthread_mutex_unlock(&mutex1);
20+
}
21+
22+
int main(void) {

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

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
#include <pthread.h>
2+
#include <stdio.h>
3+
4+
int myglobal;
5+
pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
6+
pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
7+
8+
void *t_fun(void *arg) {
9+
pthread_mutex_lock(&mutex1);
10+
myglobal=myglobal+1; // RACE!
11+
pthread_mutex_unlock(&mutex1);
12+
return NULL;
13+
}
14+
15+
void wrap() {
16+
pthread_mutex_lock(&mutex2);
17+
myglobal=myglobal+1; // RACE!
18+
pthread_mutex_unlock(&mutex2);
19+
}
20+
21+
int main(void) {
22+
pthread_t id;
23+
pthread_create(&id, NULL, t_fun, NULL);
24+
wrap();
25+
pthread_join (id, NULL);
26+
return 0;
27+
}

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
{
2+
"incremental": {
3+
"restart": {
4+
"sided": {
5+
"enabled": true,
6+
"fuel": 1,
7+
"fuel-only-global": true
8+
},
9+
"write-only": false
10+
}
11+
}
12+
}

0 commit comments

Comments
 (0)