From fcae856e66379752f8d227784d28c424206ab0c1 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 15 Feb 2013 11:02:05 -0800 Subject: [PATCH] model: fix leaking "pending actions" ModelActions that are "pending" for each thread are not automatically freed when we rollback; we keep most of the active ModelActions on the NodeStack, then we free them from there when we explore a new branch of the state space. This fix causes all the pending actions to be freed on any rollback. This is safe for now, since we always roll back to the beginning of the execution. If we roll back to an intermediate point, though, we need to retain those pending actions which were also pending before the rollback point. Hence the FIXME notice included in reset_to_initial_state(). --- model.cc | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/model.cc b/model.cc index 01e4c491..503253af 100644 --- a/model.cc +++ b/model.cc @@ -159,6 +159,14 @@ void ModelChecker::reset_to_initial_state() /* Print all model-checker output before rollback */ fflush(model_out); + /** + * FIXME: if we utilize partial rollback, we will need to free only + * those pending actions which were NOT pending before the rollback + * point + */ + for (unsigned int i = 0; i < get_num_threads(); i++) + delete get_thread(int_to_id(i))->get_pending(); + snapshot_backtrack_before(0); } -- 2.34.1