Fork handler mitigations

diff --git a/classlist.h b/classlist.h
index 641a148103b73f98a1d5448a9ff755867368e372..24c635fd352d550fabb9f7777172095c43d95b60 100644 (file)
--- a/classlist.h
+++ b/classlist.h
@@ -19,4 +19,6 @@ class Fuzzer;
 struct model_snapshot_members;
 struct bug_message;
 typedef SnapList<ModelAction *> action_list_t;
+
+extern volatile int forklock;
 #endif

diff --git a/common.h b/common.h
index 0f0ad64f9e317b634c38eba45496e60672bfbc64..27f4c8ef0e753fd0b160472eb41a0156fb983942 100644 (file)
--- a/common.h
+++ b/common.h
@@ -11,10 +11,8 @@
 #include "printf.h"
 
 extern int model_out;
-extern int switch_alloc;
 
 #define model_print(fmt, ...) do { \
-               switch_alloc = 1;              \
                char mprintbuf[256];                                                \
                int printbuflen=snprintf_(mprintbuf, 256, fmt, ## __VA_ARGS__);     \
                int lenleft = printbuflen < 256 ? printbuflen : 256;                   \
@@ -24,7 +22,6 @@ extern int switch_alloc;
                        lenleft-=byteswritten;                                            \
                        totalwritten+=byteswritten;                                       \
                }                                                                   \
-               switch_alloc = 0;                                                   \
 } while (0)
 
 #ifdef CONFIG_DEBUG

diff --git a/config.h b/config.h
index 43c044278eac3350d507309f86a9b05582308ca8..ed0b6bac2e62e02043570503f552a73e4f028ffd 100644 (file)
--- a/config.h
+++ b/config.h
@@ -54,4 +54,7 @@
 /** Enable debugging assertions (via ASSERT()) */
 #define CONFIG_ASSERT
 
+/** Enable mitigations against fork handlers that call into locks...  */
+#define FORK_HANDLER_HACK
+
 #endif

diff --git a/model.cc b/model.cc
index 1be15edbf2a1a63c4912684c367a338cb1f1da39..8454d0fb7e661945714ef116e060dfe40914c869 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -319,7 +319,17 @@ void ModelChecker::switch_from_master(Thread *thread)
  */
 uint64_t ModelChecker::switch_to_master(ModelAction *act)
 {
-       DBG();
+  if (forklock) {
+    static bool fork_message_printed = false;
+
+    if (!fork_message_printed) {
+      model_print("Fork handler trying to call into model checker...\n");
+      fork_message_printed = true;
+    }
+    delete act;
+    return 0;
+  }
+  DBG();
        Thread *old = thread_current();
        scheduler->set_current_thread(NULL);
        ASSERT(!old->get_pending());

diff --git a/mymemory.cc b/mymemory.cc
index a85c48c31121bc5175d658fe48ddad3a62c48d0c..66a4fb973066621e3531b3963f045eafb63977f7 100644 (file)
--- a/mymemory.cc
+++ b/mymemory.cc
@@ -17,7 +17,6 @@
 size_t allocatedReqs[REQUESTS_BEFORE_ALLOC] = { 0 };
 int nextRequest = 0;
 int howManyFreed = 0;
-int switch_alloc = 0;
 #if !USE_MPROTECT_SNAPSHOT
 static mspace sStaticSpace = NULL;
 #endif
@@ -181,9 +180,6 @@ static void * user_malloc(size_t size)
 void *malloc(size_t size)
 {
        if (user_snapshot_space) {
-               if (switch_alloc) {
-                       return model_malloc(size);
-               }
                /* Only perform user allocations from user context */
                ASSERT(!model || thread_current());
                return user_malloc(size);
@@ -195,9 +191,6 @@ void *malloc(size_t size)
 void free(void * ptr)
 {
        if (!DontFree(ptr)) {
-               if (switch_alloc) {
-                       return model_free(ptr);
-               }
                mspace_free(user_snapshot_space, ptr);
        }
 }

diff --git a/snapshot.cc b/snapshot.cc
index dc42614efd8f89d7f6fb6360132afb2fe7410c5b..6725a7aed80ffefab54247fde99e87d848c60329 100644 (file)
--- a/snapshot.cc
+++ b/snapshot.cc
@@ -375,6 +375,8 @@ static void fork_snapshot_init(unsigned int numbackingpages,
        model_snapshot_space = create_mspace(numheappages * PAGESIZE, 1);
 }
 
+volatile int forklock = 0;
+
 static void fork_loop() {
        /* switch back here when takesnapshot is called */
        snapshotid = fork_snap->currSnapShotID;
@@ -386,7 +388,10 @@ static void fork_loop() {
        while (true) {
                pid_t forkedID;
                fork_snap->currSnapShotID = snapshotid + 1;
+
+               forklock = 1;
                forkedID = fork();
+               forklock = 0;
 
                if (0 == forkedID) {
                        setcontext(&fork_snap->shared_ctxt);