model: fix leaking "pending actions"
authorBrian Norris <banorris@uci.edu>
Fri, 15 Feb 2013 19:02:05 +0000 (11:02 -0800)
committerBrian Norris <banorris@uci.edu>
Fri, 15 Feb 2013 22:55:02 +0000 (14:55 -0800)
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

index 01e4c49..503253a 100644 (file)
--- 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);
 
        /* 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);
 }
 
        snapshot_backtrack_before(0);
 }