Remove snapshot stack

diff --git a/Makefile b/Makefile
index d74c3a3d1408a62e373f81df9b390f9624eddc7b..c1d0e232f73aa3c0a089e46de596af5d7d828b89 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -1,7 +1,7 @@
 include common.mk
 
 OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \
-          clockvector.o main.o snapshot-interface.o cyclegraph.o \
+          clockvector.o main.o cyclegraph.o \
           datarace.o impatomic.o cmodelint.o \
           snapshot.o malloc.o mymemory.o common.o mutex.o conditionvariable.o \
           context.o execution.o libannotate.o plugins.o pthread.o futex.o fuzzer.o \

diff --git a/model.cc b/model.cc
index d6e5ed24e76108f89c37c1c7d9269978bb3f0460..a934d0adcb7be451907d3141243f4239564743d2 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -85,7 +85,7 @@ void ModelChecker::reset_to_initial_state()
        for (unsigned int i = 0;i < get_num_threads();i++)
                delete get_thread(int_to_id(i))->get_pending();
 
-       snapshot_backtrack_before(0);
+       snapshot_roll_back(snapshot);
 }
 
 /** @return the number of user threads created during this execution */
@@ -356,8 +356,7 @@ static void runChecker() {
 
 void ModelChecker::startChecker() {
        startExecution(get_system_context(), runChecker);
-       snapshot_stack_init();
-       snapshot_record(0);
+       snapshot = take_snapshot();
        initMainThread();
 }
 

diff --git a/model.h b/model.h
index ea526f7499bff4e919385fa9fda5d31f2d207eec..c5a5aa78647deb2bfdb3ae7cf269b972ae5f89f0 100644 (file)
--- a/model.h
+++ b/model.h
@@ -16,6 +16,7 @@
 #include "context.h"
 #include "params.h"
 #include "classlist.h"
+#include "snapshot-interface.h"
 
 typedef SnapList<ModelAction *> action_list_t;
 
@@ -71,6 +72,9 @@ private:
        /** Flag indicates whether to restart the model checker. */
        bool restart_flag;
 
+       /** Snapshot id we return to restart. */
+       snapshot_id snapshot;
+
        /** The scheduler to use: tracks the running/ready Threads */
        Scheduler * const scheduler;
        ModelHistory * history;

diff --git a/snapshot-interface.cc b/snapshot-interface.cc
deleted file mode 100644 (file)
index bf12fe8..0000000
--- a/snapshot-interface.cc
+++ /dev/null
@@ -1,175 +0,0 @@
-#include <stdlib.h>
-#include <unistd.h>
-#include <cstring>
-#include <inttypes.h>
-
-#include "snapshot-interface.h"
-#include "snapshot.h"
-#include "common.h"
-#include "mymemory.h"
-#include "stl-model.h"
-
-/* MYBINARYNAME only works because our pathname usually includes 'model' (e.g.,
- * /.../model-checker/test/userprog.o) */
-#define MYBINARYNAME "model"
-#define MAPFILE "/proc/self/maps"
-
-struct snapshot_entry {
-       snapshot_entry(snapshot_id id, int idx) : snapshotid(id), index(idx) { }
-       snapshot_id snapshotid;
-       int index;
-       MEMALLOC
-};
-
-class SnapshotStack {
-public:
-       int backTrackBeforeStep(int seq_index);
-       void snapshotStep(int seq_index);
-
-       MEMALLOC
-private:
-       ModelVector<struct snapshot_entry> stack;
-};
-
-static SnapshotStack *snap_stack;
-
-#ifdef MAC
-/** The SnapshotGlobalSegments function computes the memory regions
- *     that may contain globals and then configures the snapshotting
- *     library to snapshot them.
- */
-static void SnapshotGlobalSegments()
-{
-       int pid = getpid();
-       char buf[9000], execname[100];
-       FILE *map;
-
-       sprintf(execname, "vmmap -interleaved %d", pid);
-       map = popen(execname, "r");
-
-       if (!map) {
-               perror("popen");
-               exit(EXIT_FAILURE);
-       }
-
-       /* Wait for correct part */
-       while (fgets(buf, sizeof(buf), map)) {
-               if (strstr(buf, "==== regions for process"))
-                       break;
-       }
-
-       while (fgets(buf, sizeof(buf), map)) {
-               char regionname[200] = "";
-               char type[23];
-               char smstr[23];
-               char r, w, x;
-               char mr, mw, mx;
-               void *begin, *end;
-
-               //Skip out at the end of the section
-               if (buf[0] == '\n')
-                       break;
-
-               sscanf(buf, "%22s %p-%p", type, &begin, &end);
-
-               char * secondpart = strstr(buf, "]");
-
-               sscanf(&secondpart[2], "%c%c%c/%c%c%c SM=%3s %200s\n", &r, &w, &x, &mr, &mw, &mx, smstr, regionname);
-               if (w == 'w' && strstr(regionname, MYBINARYNAME)) {
-                       size_t len = ((uintptr_t)end - (uintptr_t)begin) / PAGESIZE;
-                       if (len != 0)
-                               snapshot_add_memory_region(begin, len);
-               }
-       }
-       pclose(map);
-}
-#else
-
-static void get_binary_name(char *buf, size_t len)
-{
-       ssize_t size = readlink("/proc/self/exe", buf, len);
-       if (size < 0) {
-               perror("readlink");
-               exit(EXIT_FAILURE);
-       }
-
-       /* Terminate string */
-       if ((size_t)size > len)
-               size = len;
-       buf[size] = '\0';
-}
-
-/** The SnapshotGlobalSegments function computes the memory regions
- *     that may contain globals and then configures the snapshotting
- *     library to snapshot them.
- */
-static void SnapshotGlobalSegments()
-{
-       char buf[9000];
-       char binary_name[800];
-       FILE *map;
-
-       map = fopen(MAPFILE, "r");
-       if (!map) {
-               perror("fopen");
-               exit(EXIT_FAILURE);
-       }
-       get_binary_name(binary_name, sizeof(binary_name));
-       while (fgets(buf, sizeof(buf), map)) {
-               char regionname[200] = "";
-               char r, w, x, p;
-               void *begin, *end;
-
-               sscanf(buf, "%p-%p %c%c%c%c %*x %*x:%*x %*u %200s\n", &begin, &end, &r, &w, &x, &p, regionname);
-               if (w == 'w' && strstr(regionname, binary_name)) {
-                       size_t len = ((uintptr_t)end - (uintptr_t)begin) / PAGESIZE;
-                       if (len != 0)
-                               snapshot_add_memory_region(begin, len);
-                       DEBUG("%55s: %18p - %18p\t%c%c%c%c\n", regionname, begin, end, r, w, x, p);
-               }
-       }
-       fclose(map);
-}
-#endif
-
-/** This method returns to the last snapshot before the inputted
- * sequence number.  This function must be called from the model
- * checking thread and not from a snapshotted stack.
- * @param seqindex is the sequence number to rollback before.
- * @return is the sequence number we actually rolled back to.
- */
-int SnapshotStack::backTrackBeforeStep(int seqindex)
-{
-       int i;
-       for (i = (int)stack.size() - 1;i >= 0;i++)
-               if (stack[i].index <= seqindex)
-                       break;
-               else
-                       stack.pop_back();
-
-       ASSERT(i >= 0);
-       snapshot_roll_back(stack[i].snapshotid);
-       return stack[i].index;
-}
-
-/** This method takes a snapshot at the given sequence number. */
-void SnapshotStack::snapshotStep(int seqindex)
-{
-       stack.push_back(snapshot_entry(take_snapshot(), seqindex));
-}
-
-void snapshot_stack_init()
-{
-       snap_stack = new SnapshotStack();
-       SnapshotGlobalSegments();
-}
-
-void snapshot_record(int seq_index)
-{
-       snap_stack->snapshotStep(seq_index);
-}
-
-int snapshot_backtrack_before(int seq_index)
-{
-       return snap_stack->backTrackBeforeStep(seq_index);
-}

diff --git a/snapshot-interface.h b/snapshot-interface.h
index 4d27ae04cecfcd679b8d81d64061579391a25075..7a5030b85dc23df43112189e03e611fe0cc86c76 100644 (file)
--- a/snapshot-interface.h
+++ b/snapshot-interface.h
@@ -14,8 +14,8 @@ void snapshot_system_init(unsigned int numbackingpages,
                                                                                                        unsigned int numsnapshots, unsigned int nummemoryregions,
                                                                                                        unsigned int numheappages);
 void startExecution(ucontext_t * context, VoidFuncPtr entryPoint);
-void snapshot_stack_init();
-void snapshot_record(int seq_index);
-int snapshot_backtrack_before(int seq_index);
+snapshot_id take_snapshot();
+void snapshot_roll_back(snapshot_id theSnapShot);
+
 
 #endif

diff --git a/snapshot.cc b/snapshot.cc
index 1770fd648d414ef40cd064b1179ebbae3f65d85a..c049167e52bb753e35dcb4dca11c45da821bc5cb 100644 (file)
--- a/snapshot.cc
+++ b/snapshot.cc
@@ -211,12 +211,6 @@ void startExecution(ucontext_t *context, VoidFuncPtr entryPoint)
        fork_startExecution(context, entryPoint);
 }
 
-/** Assumes that addr is page aligned. */
-void snapshot_add_memory_region(void *addr, unsigned int numPages)
-{
-       /* not needed for fork-based snapshotting */
-}
-
 /** Takes a snapshot of memory.
  * @return The snapshot identifier.
  */

diff --git a/snapshot.h b/snapshot.h
index 1aa1435f7fd6542dcbd42007e3bc6b2b4dcc4bba..47e48b234f0f2f9b980c710186b4eab9117a13e1 100644 (file)
--- a/snapshot.h
+++ b/snapshot.h
@@ -9,9 +9,6 @@
 #include "config.h"
 #include "mymemory.h"
 
-void snapshot_add_memory_region(void *ptr, unsigned int numPages);
-snapshot_id take_snapshot();
-void snapshot_roll_back(snapshot_id theSnapShot);
 mspace create_shared_mspace();
 
 #endif