12 #include "threads-model.h"
16 #define REQUESTS_BEFORE_ALLOC 1024
18 size_t allocatedReqs[REQUESTS_BEFORE_ALLOC] = { 0 };
21 mspace sStaticSpace = NULL;
23 /** Non-snapshotting calloc for our use. */
24 void *model_calloc(size_t count, size_t size)
26 return mspace_calloc(sStaticSpace, count, size);
29 /** Non-snapshotting malloc for our use. */
30 void *model_malloc(size_t size)
32 return mspace_malloc(sStaticSpace, size);
35 /** Non-snapshotting malloc for our use. */
36 void *model_realloc(void *ptr, size_t size)
38 return mspace_realloc(sStaticSpace, ptr, size);
41 /** @brief Snapshotting malloc, for use by model-checker (not user progs) */
42 void * snapshot_malloc(size_t size)
44 void *tmp = mspace_malloc(model_snapshot_space, size);
49 /** @brief Snapshotting calloc, for use by model-checker (not user progs) */
50 void * snapshot_calloc(size_t count, size_t size)
52 void *tmp = mspace_calloc(model_snapshot_space, count, size);
57 /** @brief Snapshotting realloc, for use by model-checker (not user progs) */
58 void *snapshot_realloc(void *ptr, size_t size)
60 void *tmp = mspace_realloc(model_snapshot_space, ptr, size);
65 /** @brief Snapshotting free, for use by model-checker (not user progs) */
66 void snapshot_free(void *ptr)
68 mspace_free(model_snapshot_space, ptr);
71 /** Non-snapshotting free for our use. */
72 void model_free(void *ptr)
74 mspace_free(sStaticSpace, ptr);
77 /** Bootstrap allocation. Problem is that the dynamic linker calls require
78 * calloc to work and calloc requires the dynamic linker to work. */
80 #define BOOTSTRAPBYTES 131072
81 char bootstrapmemory[BOOTSTRAPBYTES];
84 void * HandleEarlyAllocationRequest(size_t sz)
86 /* Align to 8 byte boundary */
89 if (sz > (BOOTSTRAPBYTES-offset)) {
90 model_print("OUT OF BOOTSTRAP MEMORY. Increase the size of BOOTSTRAPBYTES in mymemory.cc\n");
94 void *pointer = (void *)&bootstrapmemory[offset];
99 /** @brief Global mspace reference for the model-checker's snapshotting heap */
100 mspace model_snapshot_space = NULL;
102 /** @brief Snapshotting allocation function for use by the Thread class only */
103 void * Thread_malloc(size_t size)
105 return snapshot_malloc(size);
108 /** @brief Snapshotting free function for use by the Thread class only */
109 void Thread_free(void *ptr)
114 void * (*volatile real_memcpy)(void * dst, const void *src, size_t n) = NULL;
115 void * (*volatile real_memmove)(void * dst, const void *src, size_t len) = NULL;
116 void (*volatile real_bzero)(void * dst, size_t len) = NULL;
117 void * (*volatile real_memset)(void * dst, int c, size_t len) = NULL;
119 void init_memory_ops()
122 real_memcpy = (void * (*)(void * dst, const void *src, size_t n)) 1;
123 real_memcpy = (void * (*)(void * dst, const void *src, size_t n))dlsym(RTLD_NEXT, "memcpy");
126 real_memmove = (void * (*)(void * dst, const void *src, size_t n)) 1;
127 real_memmove = (void * (*)(void * dst, const void *src, size_t n))dlsym(RTLD_NEXT, "memmove");
130 real_memset = (void * (*)(void * dst, int c, size_t n)) 1;
131 real_memset = (void * (*)(void * dst, int c, size_t n))dlsym(RTLD_NEXT, "memset");
134 real_bzero = (void (*)(void * dst, size_t len)) 1;
135 real_bzero = (void (*)(void * dst, size_t len))dlsym(RTLD_NEXT, "bzero");
139 void * memcpy(void * dst, const void * src, size_t n) {
140 if (model && !inside_model) {
141 //model_print("memcpy size: %d\n", n);
142 thread_id_t tid = thread_current_id();
143 raceCheckReadMemop(tid, (void *)src, n);
144 raceCheckWriteMemop(tid, (void *)dst, n);
145 } else if (((uintptr_t)real_memcpy) < 2) {
146 for(uint i=0;i<n;i++) {
147 ((volatile char *)dst)[i] = ((char *)src)[i];
151 return real_memcpy(dst, src, n);
154 void * memmove(void * dst, const void * src, size_t n) {
155 if (model && !inside_model) {
156 thread_id_t tid = thread_current_id();
157 raceCheckReadMemop(tid, (void *)src, n);
158 raceCheckWriteMemop(tid, (void *)dst, n);
159 } else if (((uintptr_t)real_memmove) < 2) {
160 if (((uintptr_t)dst) < ((uintptr_t)src))
161 for(uint i=0;i<n;i++) {
162 ((volatile char *)dst)[i] = ((char *)src)[i];
165 for(uint i=n;i!=0; ) {
167 ((volatile char *)dst)[i] = ((char *)src)[i];
171 return real_memmove(dst, src, n);
174 void * memset(void *dst, int c, size_t n) {
175 if (model && !inside_model) {
176 //model_print("memset size: %d\n", n);
177 thread_id_t tid = thread_current_id();
178 raceCheckWriteMemop(tid, (void *)dst, n);
179 } else if (((uintptr_t)real_memset) < 2) {
180 //stuck in dynamic linker alloc cycle...
181 for(size_t s=0;s<n;s++) {
182 ((volatile char *)dst)[s] = (char) c;
186 return real_memset(dst, c, n);
189 void bzero(void *dst, size_t n) {
190 if (model && !inside_model) {
191 thread_id_t tid = thread_current_id();
192 raceCheckWriteMemop(tid, (void *)dst, n);
193 } else if (((uintptr_t)real_bzero) < 2) {
194 for(size_t s=0;s<n;s++) {
195 ((volatile char *)dst)[s] = 0;