SNAPSHOTALLOC
};
-
-#ifdef TLS
-#include <dlfcn.h>
-
-//Code taken from LLVM and licensed under the University of Illinois Open Source
-//License.
-static uintptr_t thread_descriptor_size;
-#if __LP64__ || defined(_WIN64)
-# define SANITIZER_WORDSIZE 64
-#else
-# define SANITIZER_WORDSIZE 32
-#endif
-
-#if SANITIZER_WORDSIZE == 64
-# define FIRST_32_SECOND_64(a, b) (b)
-#else
-# define FIRST_32_SECOND_64(a, b) (a)
-#endif
-
-#if defined(__x86_64__) && !defined(_LP64)
-# define SANITIZER_X32 1
-#else
-# define SANITIZER_X32 0
-#endif
-
-#if defined(__arm__)
-# define SANITIZER_ARM 1
-#else
-# define SANITIZER_ARM 0
-#endif
-
-uintptr_t ThreadDescriptorSize() {
- uintptr_t val = thread_descriptor_size;
- if (val)
- return val;
-#if defined(__x86_64__) || defined(__i386__) || defined(__arm__)
-#ifdef _CS_GNU_LIBC_VERSION
- char buf[64];
- uintptr_t len = confstr(_CS_GNU_LIBC_VERSION, buf, sizeof(buf));
- if (len < sizeof(buf) && strncmp(buf, "glibc 2.", 8) == 0) {
- char *end;
- int minor = strtoll(buf + 8, &end, 10);
- if (end != buf + 8 && (*end == '\0' || *end == '.' || *end == '-')) {
- int patch = 0;
- if (*end == '.')
- // strtoll will return 0 if no valid conversion could be performed
- patch = strtoll(end + 1, nullptr, 10);
-
- /* sizeof(struct pthread) values from various glibc versions. */
- if (SANITIZER_X32)
- val = 1728;// Assume only one particular version for x32.
- // For ARM sizeof(struct pthread) changed in Glibc 2.23.
- else if (SANITIZER_ARM)
- val = minor <= 22 ? 1120 : 1216;
- else if (minor <= 3)
- val = FIRST_32_SECOND_64(1104, 1696);
- else if (minor == 4)
- val = FIRST_32_SECOND_64(1120, 1728);
- else if (minor == 5)
- val = FIRST_32_SECOND_64(1136, 1728);
- else if (minor <= 9)
- val = FIRST_32_SECOND_64(1136, 1712);
- else if (minor == 10)
- val = FIRST_32_SECOND_64(1168, 1776);
- else if (minor == 11 || (minor == 12 && patch == 1))
- val = FIRST_32_SECOND_64(1168, 2288);
- else if (minor <= 13)
- val = FIRST_32_SECOND_64(1168, 2304);
- else
- val = FIRST_32_SECOND_64(1216, 2304);
- }
- }
-#endif
-#elif defined(__mips__)
- // TODO(sagarthakur): add more values as per different glibc versions.
- val = FIRST_32_SECOND_64(1152, 1776);
-#elif defined(__aarch64__)
- // The sizeof (struct pthread) is the same from GLIBC 2.17 to 2.22.
- val = 1776;
-#elif defined(__powerpc64__)
- val = 1776; // from glibc.ppc64le 2.20-8.fc21
-#elif defined(__s390__)
- val = FIRST_32_SECOND_64(1152, 1776); // valid for glibc 2.22
-#endif
- if (val)
- thread_descriptor_size = val;
- return val;
-}
-
-#ifdef __i386__
-# define DL_INTERNAL_FUNCTION __attribute__((regparm(3), stdcall))
-#else
-# define DL_INTERNAL_FUNCTION
-#endif
-
-intptr_t RoundUpTo(uintptr_t size, uintptr_t boundary) {
- return (size + boundary - 1) & ~(boundary - 1);
-}
-
-uintptr_t getTlsSize() {
- // all current supported platforms have 16 bytes stack alignment
- const size_t kStackAlign = 16;
- typedef void (*get_tls_func)(size_t*, size_t*) DL_INTERNAL_FUNCTION;
- get_tls_func get_tls;
- void *get_tls_static_info_ptr = dlsym(RTLD_NEXT, "_dl_get_tls_static_info");
- memcpy(&get_tls, &get_tls_static_info_ptr, sizeof(get_tls_static_info_ptr));
- ASSERT(get_tls != 0);
- size_t tls_size = 0;
- size_t tls_align = 0;
- get_tls(&tls_size, &tls_align);
- if (tls_align < kStackAlign)
- tls_align = kStackAlign;
- return RoundUpTo(tls_size, tls_align);
-}
-
-#endif
-
/** @brief Constructor */
ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
model(m),
thrd_last_action(1),
thrd_last_fence_release(),
priv(new struct model_snapshot_members ()),
- mo_graph(new CycleGraph()),
+ mo_graph(new CycleGraph()),
fuzzer(new Fuzzer()),
thrd_func_list(),
- thrd_func_inst_lists()
-#ifdef TLS
- ,tls_base(NULL),
- tls_addr(0),
- tls_size(0),
- thd_desc_size(0)
-#endif
+ thrd_func_inst_lists(),
+ isfinished(false)
{
/* Initialize a model-checker thread, for special ModelActions */
model_thread = new Thread(get_next_id());
scheduler->register_engine(this);
}
-#ifdef TLS
-void ModelExecution::initTLS() {
- tls_addr = get_tls_addr();
- tls_size = getTlsSize();
- tls_addr -= tls_size;
- thd_desc_size = ThreadDescriptorSize();
- tls_addr += thd_desc_size;
- tls_base = (char *) snapshot_calloc(tls_size,1);
- memcpy(tls_base, reinterpret_cast<const char *>(tls_addr), tls_size);
-}
-#endif
-
/** @brief Destructor */
ModelExecution::~ModelExecution()
{
return act;
}
-
/**
* Processes a read model action.
* @param curr is the read model action to process.
continue;
/* Establish hypothetical release sequences */
- ClockVector *cv = get_hb_from_write(act);
- if (curr->get_cv()->merge(cv))
+ ClockVector *cv = get_hb_from_write(act->get_reads_from());
+ if (cv != NULL && curr->get_cv()->merge(cv))
updated = true;
}
}
* @param curr The current action
* @return True if synchronization was updated or a thread completed
*/
-bool ModelExecution::process_thread_action(ModelAction *curr)
+void ModelExecution::process_thread_action(ModelAction *curr)
{
- bool updated = false;
-
switch (curr->get_type()) {
case THREAD_CREATE: {
thrd_t *thrd = (thrd_t *)curr->get_location();
Thread *blocking = curr->get_thread_operand();
ModelAction *act = get_last_action(blocking->get_id());
synchronize(act, curr);
- updated = true; /* trigger rel-seq checks */
break;
}
case PTHREAD_JOIN: {
Thread *blocking = curr->get_thread_operand();
ModelAction *act = get_last_action(blocking->get_id());
synchronize(act, curr);
- updated = true; /* trigger rel-seq checks */
break; // WL: to be add (modified)
}
+ case THREADONLY_FINISH:
case THREAD_FINISH: {
Thread *th = get_thread(curr);
+ if (curr == THREAD_FINISH &&
+ th == model->getInitThread()) {
+ th->complete();
+ setFinished();
+ break;
+ }
+
/* Wake up any joining threads */
for (unsigned int i = 0;i < get_num_threads();i++) {
Thread *waiting = get_thread(int_to_id(i));
scheduler->wake(waiting);
}
th->complete();
- updated = true; /* trigger rel-seq checks */
break;
}
case THREAD_START: {
default:
break;
}
-
- return updated;
}
/**
if (act->happens_before(curr)) {
if (i==0) {
if (last_sc_fence_local == NULL ||
- (*last_sc_fence_local < *prev_same_thread)) {
+ (*last_sc_fence_local < *act)) {
prev_same_thread = act;
}
}
unsigned int i;
ASSERT(curr->is_write());
+ SnapList<ModelAction *> edgeset;
+
if (curr->is_seqcst()) {
/* We have to at least see the last sequentially consistent write,
so we are initialized. */
ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
if (last_seq_cst != NULL) {
- mo_graph->addEdge(last_seq_cst, curr);
+ edgeset.push_back(last_seq_cst);
}
+ //update map for next query
+ obj_last_sc_map.put(curr->get_location(), curr);
}
/* Last SC fence in the current thread */
/* Iterate over actions in thread, starting from most recent */
action_list_t *list = &(*thrd_lists)[i];
action_list_t::reverse_iterator rit;
- bool force_edge = false;
for (rit = list->rbegin();rit != list->rend();rit++) {
ModelAction *act = *rit;
if (act == curr) {
* 3) If normal write, we need to look at earlier actions, so
* continue processing list.
*/
- force_edge = true;
if (curr->is_rmw()) {
if (curr->get_reads_from() != NULL)
break;
/* C++, Section 29.3 statement 7 */
if (last_sc_fence_thread_before && act->is_write() &&
*act < *last_sc_fence_thread_before) {
- mo_graph->addEdge(act, curr, force_edge);
+ edgeset.push_back(act);
break;
}
* readfrom(act) --mo--> act
*/
if (act->is_write())
- mo_graph->addEdge(act, curr, force_edge);
+ edgeset.push_back(act);
else if (act->is_read()) {
//if previous read accessed a null, just keep going
- mo_graph->addEdge(act->get_reads_from(), curr, force_edge);
+ edgeset.push_back(act->get_reads_from());
}
break;
}
}
}
+ mo_graph->addEdges(&edgeset, curr);
+
}
/**
void ModelExecution::add_write_to_lists(ModelAction *write) {
- // Update seq_cst map
- if (write->is_seqcst())
- obj_last_sc_map.put(write->get_location(), write);
-
SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
int tid = id_to_int(write->get_tid());
if (tid >= (int)vec->size())
ASSERT(curr);
/* Process this action in ModelHistory for records*/
- model->get_history()->process_action( curr, curr_thrd->get_id() );
+ model->get_history()->process_action( curr, curr->get_tid() );
if (curr_thrd->is_blocked() || curr_thrd->is_complete())
scheduler->remove_thread(curr_thrd);
projects / c11tester.git / blobdiff