From 28ad364d515e48abc7a57371ff906b63e19c8d7a Mon Sep 17 00:00:00 2001 From: root Date: Fri, 6 Dec 2019 22:41:31 -0800 Subject: [PATCH] Remove snapshot stack --- Makefile | 2 +- model.cc | 5 +- model.h | 4 + snapshot-interface.cc | 175 ------------------------------------------ snapshot-interface.h | 6 +- snapshot.cc | 6 -- snapshot.h | 3 - 7 files changed, 10 insertions(+), 191 deletions(-) delete mode 100644 snapshot-interface.cc diff --git a/Makefile b/Makefile index d74c3a3d..c1d0e232 100644 --- 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 d6e5ed24..a934d0ad 100644 --- 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 ea526f74..c5a5aa78 100644 --- 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 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 index bf12fe8a..00000000 --- a/snapshot-interface.cc +++ /dev/null @@ -1,175 +0,0 @@ -#include -#include -#include -#include - -#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 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 4d27ae04..7a5030b8 100644 --- 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 1770fd64..c049167e 100644 --- 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 1aa1435f..47e48b23 100644 --- 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 -- 2.34.1