From 616c0ed2533f50f2c9b0d0cd5fec6f48bee6888d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 27 Apr 2022 18:08:33 +0300 Subject: [PATCH 1/5] Add test for incremental warnings not removed with reluctant destabilization (issue #708) --- .../06-mutex-simple-reluctant.c | 23 ++++++++++++++++++ .../06-mutex-simple-reluctant.json | 12 ++++++++++ .../06-mutex-simple-reluctant.patch | 24 +++++++++++++++++++ 3 files changed, 59 insertions(+) create mode 100644 tests/incremental/13-restart-write/06-mutex-simple-reluctant.c create mode 100644 tests/incremental/13-restart-write/06-mutex-simple-reluctant.json create mode 100644 tests/incremental/13-restart-write/06-mutex-simple-reluctant.patch diff --git a/tests/incremental/13-restart-write/06-mutex-simple-reluctant.c b/tests/incremental/13-restart-write/06-mutex-simple-reluctant.c new file mode 100644 index 0000000000..82c1642a93 --- /dev/null +++ b/tests/incremental/13-restart-write/06-mutex-simple-reluctant.c @@ -0,0 +1,23 @@ +#include +#include + +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; +} diff --git a/tests/incremental/13-restart-write/06-mutex-simple-reluctant.json b/tests/incremental/13-restart-write/06-mutex-simple-reluctant.json new file mode 100644 index 0000000000..699332fa16 --- /dev/null +++ b/tests/incremental/13-restart-write/06-mutex-simple-reluctant.json @@ -0,0 +1,12 @@ +{ + "incremental": { + "restart": { + "sided": { + "enabled": false + } + }, + "reluctant": { + "on": true + } + } +} \ No newline at end of file diff --git a/tests/incremental/13-restart-write/06-mutex-simple-reluctant.patch b/tests/incremental/13-restart-write/06-mutex-simple-reluctant.patch new file mode 100644 index 0000000000..3674a31c23 --- /dev/null +++ b/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; + } From 60b756bfb29e709d7bff5f3f2626eb1ccf51e5d9 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 27 Apr 2022 18:19:26 +0300 Subject: [PATCH 2/5] Fix incremental unknown deletion to apply to incremental postsolving structures as well (issue #708) --- src/solvers/td3.ml | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 1b52aa81c5..839433daa2 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -737,7 +737,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; (* destabilize_with_side doesn't have all infl to follow anymore, so should somewhat work with reluctant *) @@ -826,8 +826,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 *) From 428cda0964dc4c20bec84920ee3329b3d65d86e4 Mon Sep 17 00:00:00 2001 From: Vesal Vojdani Date: Wed, 27 Apr 2022 22:45:40 +0000 Subject: [PATCH 3/5] Add test where warning should remain. --- .../07-mutex-simple-reluctant2.c | 23 +++++++++++++++++++ .../07-mutex-simple-reluctant2.json | 12 ++++++++++ .../07-mutex-simple-reluctant2.patch | 11 +++++++++ 3 files changed, 46 insertions(+) create mode 100644 tests/incremental/13-restart-write/07-mutex-simple-reluctant2.c create mode 100644 tests/incremental/13-restart-write/07-mutex-simple-reluctant2.json create mode 100644 tests/incremental/13-restart-write/07-mutex-simple-reluctant2.patch diff --git a/tests/incremental/13-restart-write/07-mutex-simple-reluctant2.c b/tests/incremental/13-restart-write/07-mutex-simple-reluctant2.c new file mode 100644 index 0000000000..82c1642a93 --- /dev/null +++ b/tests/incremental/13-restart-write/07-mutex-simple-reluctant2.c @@ -0,0 +1,23 @@ +#include +#include + +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; +} diff --git a/tests/incremental/13-restart-write/07-mutex-simple-reluctant2.json b/tests/incremental/13-restart-write/07-mutex-simple-reluctant2.json new file mode 100644 index 0000000000..36c62c6389 --- /dev/null +++ b/tests/incremental/13-restart-write/07-mutex-simple-reluctant2.json @@ -0,0 +1,12 @@ +{ + "incremental": { + "restart": { + "sided": { + "enabled": false + } + }, + "reluctant": { + "on": true + } + } +} diff --git a/tests/incremental/13-restart-write/07-mutex-simple-reluctant2.patch b/tests/incremental/13-restart-write/07-mutex-simple-reluctant2.patch new file mode 100644 index 0000000000..3d2a480c67 --- /dev/null +++ b/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; + } From b4fd3cb6d2ed972e009f4886ce1107a82f5aea3f Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 28 Apr 2022 10:19:11 +0300 Subject: [PATCH 4/5] Add test for incremental warnings not added with reluctant destabilization (PR #709) --- src/solvers/td3.ml | 3 +++ .../08-mutex-simple-reluctant3.c | 22 +++++++++++++++++++ .../08-mutex-simple-reluctant3.json | 12 ++++++++++ .../08-mutex-simple-reluctant3.patch | 19 ++++++++++++++++ 4 files changed, 56 insertions(+) create mode 100644 tests/incremental/13-restart-write/08-mutex-simple-reluctant3.c create mode 100644 tests/incremental/13-restart-write/08-mutex-simple-reluctant3.json create mode 100644 tests/incremental/13-restart-write/08-mutex-simple-reluctant3.patch diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 839433daa2..06019953f9 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -852,6 +852,9 @@ module WP = destabilize x; HM.replace stable x () ) + else ( + print_endline "Destabilization not required..."; + ) ) old_ret; print_endline "Final solve..." diff --git a/tests/incremental/13-restart-write/08-mutex-simple-reluctant3.c b/tests/incremental/13-restart-write/08-mutex-simple-reluctant3.c new file mode 100644 index 0000000000..b817928884 --- /dev/null +++ b/tests/incremental/13-restart-write/08-mutex-simple-reluctant3.c @@ -0,0 +1,22 @@ +#include +#include + +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; +} diff --git a/tests/incremental/13-restart-write/08-mutex-simple-reluctant3.json b/tests/incremental/13-restart-write/08-mutex-simple-reluctant3.json new file mode 100644 index 0000000000..699332fa16 --- /dev/null +++ b/tests/incremental/13-restart-write/08-mutex-simple-reluctant3.json @@ -0,0 +1,12 @@ +{ + "incremental": { + "restart": { + "sided": { + "enabled": false + } + }, + "reluctant": { + "on": true + } + } +} \ No newline at end of file diff --git a/tests/incremental/13-restart-write/08-mutex-simple-reluctant3.patch b/tests/incremental/13-restart-write/08-mutex-simple-reluctant3.patch new file mode 100644 index 0000000000..e85790ca7c --- /dev/null +++ b/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; From aca39c3fee5b926a3e0d5367d9b7c693800d97b2 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 28 Apr 2022 10:23:07 +0300 Subject: [PATCH 5/5] Fix reluctantly not destabilized functions not being postsolved (PR #709) --- src/solvers/td3.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 06019953f9..c5ee732c11 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -540,6 +540,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)); @@ -854,6 +857,7 @@ module WP = ) else ( print_endline "Destabilization not required..."; + reluctant_vs := x :: !reluctant_vs ) ) old_ret; @@ -1111,7 +1115,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";