X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=execution.cc;h=32fa727daa9fdd13807b929d2e2fc1abea0e6453;hp=af54b54a54cc43e962c8606115eb10be467ddffa;hb=ec7cf0eb61ee239b3da1f184a9e43f77b0dcc25d;hpb=04ffc0dafb0bfa78aa73b21359ca5b53622e675d diff --git a/execution.cc b/execution.cc index af54b54a..32fa727d 100644 --- a/execution.cc +++ b/execution.cc @@ -47,123 +47,6 @@ struct model_snapshot_members { SNAPSHOTALLOC }; - -#ifdef TLS -#include - -//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), @@ -180,16 +63,11 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : 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()); @@ -197,18 +75,6 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : 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(tls_addr), tls_size); -} -#endif - /** @brief Destructor */ ModelExecution::~ModelExecution() { @@ -412,7 +278,6 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) { return act; } - /** * Processes a read model action. * @param curr is the read model action to process. @@ -615,10 +480,8 @@ bool ModelExecution::process_fence(ModelAction *curr) * @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(); @@ -648,19 +511,25 @@ bool ModelExecution::process_thread_action(ModelAction *curr) 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)); @@ -669,7 +538,6 @@ bool ModelExecution::process_thread_action(ModelAction *curr) scheduler->wake(waiting); } th->complete(); - updated = true; /* trigger rel-seq checks */ break; } case THREAD_START: { @@ -678,8 +546,6 @@ bool ModelExecution::process_thread_action(ModelAction *curr) default: break; } - - return updated; } /** @@ -1045,13 +911,17 @@ void ModelExecution::w_modification_order(ModelAction *curr) unsigned int i; ASSERT(curr->is_write()); + SnapList 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 */ @@ -1067,7 +937,6 @@ void ModelExecution::w_modification_order(ModelAction *curr) /* 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) { @@ -1082,7 +951,6 @@ void ModelExecution::w_modification_order(ModelAction *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; @@ -1095,7 +963,7 @@ void ModelExecution::w_modification_order(ModelAction *curr) /* 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; } @@ -1111,15 +979,17 @@ void ModelExecution::w_modification_order(ModelAction *curr) * 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); + } /** @@ -1340,10 +1210,6 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act) 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 *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()) @@ -1767,7 +1633,7 @@ Thread * ModelExecution::take_step(ModelAction *curr) 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);