model: only backtrack fences when acquire is before release

[model-checker.git] / mymemory.cc

diff --git a/mymemory.cc b/mymemory.cc
index a15a13dd522bf54bb0b7e3c7fd49ff014467db56..44985fa3aebc0d3fc32f97c0606b3c7ef11154a8 100644 (file)
--- a/mymemory.cc
+++ b/mymemory.cc
@@ -7,7 +7,6 @@
 
 #include "mymemory.h"
 #include "snapshot.h"
-#include "snapshotimp.h"
 #include "common.h"
 
 #define REQUESTS_BEFORE_ALLOC 1024
@@ -38,10 +37,8 @@ void *model_calloc(size_t count, size_t size)
        ptr = callocp(count, size);
        return ptr;
 #else
-       if (!snapshotrecord)
-               createSharedMemory();
        if (!sStaticSpace)
-               sStaticSpace = create_mspace_with_base((void *)(snapshotrecord->mSharedMemoryBase), SHARED_MEMORY_DEFAULT - sizeof(struct SnapShot), 1);
+               sStaticSpace = create_shared_mspace();
        return mspace_calloc(sStaticSpace, count, size);
 #endif
 }
@@ -65,10 +62,8 @@ void *model_malloc(size_t size)
        ptr = mallocp(size);
        return ptr;
 #else
-       if (!snapshotrecord)
-               createSharedMemory();
        if (!sStaticSpace)
-               sStaticSpace = create_mspace_with_base((void *)(snapshotrecord->mSharedMemoryBase), SHARED_MEMORY_DEFAULT - sizeof(struct SnapShot), 1);
+               sStaticSpace = create_shared_mspace();
        return mspace_malloc(sStaticSpace, size);
 #endif
 }