From: weiyu Date: Wed, 12 Feb 2020 00:21:30 +0000 (-0800) Subject: Remove redundant data structures and FuncNode's dependencies on old actions X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=acc3332c059d0dd7113409a1e3e4664eada0cec0;p=c11tester.git Remove redundant data structures and FuncNode's dependencies on old actions --- diff --git a/funcinst.cc b/funcinst.cc index d4288a14..4c584452 100644 --- a/funcinst.cc +++ b/funcinst.cc @@ -4,7 +4,8 @@ FuncInst::FuncInst(ModelAction *act, FuncNode *func_node) : single_location(true), execution_number(0), - action_marker(0) /* The marker for FuncNode starts from 1 */ + associated_reads(), + thrd_marker() /* The marker for FuncNode starts from 1 */ { ASSERT(act); ASSERT(func_node); @@ -47,18 +48,30 @@ bool FuncInst::add_succ(FuncInst * other) return true; } -void FuncInst::set_associated_act(ModelAction * act, uint32_t marker) +void FuncInst::set_associated_read(thread_id_t tid, uint64_t read_val, uint32_t marker) { - associated_act = act; - action_marker = marker; + int thread_id = id_to_int(tid); + int old_size = associated_reads.size(); + + if (old_size < thread_id + 1) { + for (int i = old_size; i < thread_id + 1; i++ ) { + associated_reads.push_back(VALUE_NONE); + thrd_marker.push_back(0); + } + } + + thrd_marker[thread_id] = marker; + associated_reads[thread_id] = read_val; } -ModelAction * FuncInst::get_associated_act(uint32_t marker) +uint64_t FuncInst::get_associated_read(thread_id_t tid, uint32_t marker) { - if (action_marker == marker) - return associated_act; + int thread_id = id_to_int(tid); + + if (thrd_marker[thread_id] == marker) + return associated_reads[thread_id]; else - return NULL; + return VALUE_NONE; } /* Search the FuncInst that has the same type as act in the collision list */ diff --git a/funcinst.h b/funcinst.h index 79ec01ad..ca733f67 100644 --- a/funcinst.h +++ b/funcinst.h @@ -3,6 +3,7 @@ #include "action.h" #include "hashtable.h" +#include "threads-model.h" class ModelAction; @@ -39,8 +40,8 @@ public: void set_execution_number(int new_number) { execution_number = new_number; } int get_execution_number() { return execution_number; } - void set_associated_act(ModelAction * act, uint32_t marker); - ModelAction * get_associated_act(uint32_t marker); + void set_associated_read(thread_id_t tid, uint64_t read_val, uint32_t marker); + uint64_t get_associated_read(thread_id_t tid, uint32_t marker); void print(); @@ -64,8 +65,8 @@ private: bool single_location; int execution_number; - ModelAction * associated_act; - uint32_t action_marker; + ModelVector associated_reads; + ModelVector thrd_marker; /** * Collisions store a list of FuncInsts with the same position diff --git a/funcnode.cc b/funcnode.cc index a0850c70..ff62a527 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -11,14 +11,15 @@ FuncNode::FuncNode(ModelHistory * history) : history(history), exit_count(0), - marker(1), inst_counter(1), + marker(1), + thrd_marker(), func_inst_map(), inst_list(), entry_insts(), thrd_inst_pred_map(), thrd_inst_id_map(), - thrd_loc_act_map(), + thrd_loc_inst_map(), predicate_tree_position(), predicate_leaves(), leaves_tmp_storage(), @@ -167,9 +168,8 @@ void FuncNode::add_entry_inst(FuncInst * inst) void FuncNode::function_entry_handler(thread_id_t tid) { - marker++; - - init_predicate_tree_position(tid); + set_marker(tid); + set_predicate_tree_position(tid, predicate_tree_entry); init_inst_act_map(tid); init_maps(tid); } @@ -197,7 +197,6 @@ void FuncNode::function_exit_handler(thread_id_t tid) void FuncNode::update_tree(ModelAction * act) { HashTable * write_history = history->getWriteHistory(); - HashSet write_actions; /* build inst_list from act_list for later processing */ // func_inst_list_t inst_list; @@ -280,9 +279,9 @@ void FuncNode::update_predicate_tree(ModelAction * next_act) { thread_id_t tid = next_act->get_tid(); int thread_id = id_to_int(tid); + int this_marker = thrd_marker[thread_id]; - // Clear hashtables - loc_act_map_t * loc_act_map = thrd_loc_act_map[thread_id]; + loc_inst_map_t * loc_inst_map = thrd_loc_inst_map[thread_id]; inst_pred_map_t * inst_pred_map = thrd_inst_pred_map[thread_id]; inst_id_map_t * inst_id_map = thrd_inst_id_map[thread_id]; @@ -292,7 +291,7 @@ void FuncNode::update_predicate_tree(ModelAction * next_act) Predicate * curr_pred = get_predicate_tree_position(tid); while (true) { FuncInst * next_inst = get_inst(next_act); - next_inst->set_associated_act(next_act, marker); + next_inst->set_associated_read(tid, next_act->get_reads_from_value(), this_marker); Predicate * unset_predicate = NULL; bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &unset_predicate); @@ -324,6 +323,7 @@ void FuncNode::update_predicate_tree(ModelAction * next_act) // Add to the set of backedges curr_pred->add_backedge(back_pred); curr_pred = back_pred; + continue; } } @@ -341,7 +341,7 @@ void FuncNode::update_predicate_tree(ModelAction * next_act) if (next_act->is_read()) { /* Only need to store the locations of read actions */ - loc_act_map->put(next_act->get_location(), next_act); + loc_inst_map->put(next_inst->get_location(), next_inst); } inst_pred_map->put(next_inst, curr_pred); @@ -367,6 +367,9 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, { /* Check if a branch with func_inst and corresponding predicate exists */ bool branch_found = false; + thread_id_t tid = next_act->get_tid(); + int this_marker = thrd_marker[id_to_int(tid)]; + ModelVector * branches = (*curr_pred)->get_children(); for (uint i = 0;i < branches->size();i++) { Predicate * branch = (*branches)[i]; @@ -401,12 +404,11 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, break; case EQUALITY: FuncInst * to_be_compared; - ModelAction * last_act; - to_be_compared = pred_expression->func_inst; - last_act = to_be_compared->get_associated_act(marker); - last_read = last_act->get_reads_from_value(); + last_read = to_be_compared->get_associated_read(tid, this_marker); + ASSERT(last_read != VALUE_NONE); + next_read = next_act->get_reads_from_value(); equality = (last_read == next_read); if (equality != pred_expression->value) @@ -445,13 +447,12 @@ void FuncNode::infer_predicates(FuncInst * next_inst, ModelAction * next_act, { void * loc = next_act->get_location(); int thread_id = id_to_int(next_act->get_tid()); - loc_act_map_t * loc_act_map = thrd_loc_act_map[thread_id]; + loc_inst_map_t * loc_inst_map = thrd_loc_inst_map[thread_id]; if (next_inst->is_read()) { /* read + rmw */ - if ( loc_act_map->contains(loc) ) { - ModelAction * last_act = loc_act_map->get(loc); - FuncInst * last_inst = get_inst(last_act); + if ( loc_inst_map->contains(loc) ) { + FuncInst * last_inst = loc_inst_map->get(loc); struct half_pred_expr * expression = new half_pred_expr(EQUALITY, last_inst); half_pred_expressions->push_back(expression); } else if ( next_inst->is_single_location() ) { @@ -461,9 +462,8 @@ void FuncNode::infer_predicates(FuncInst * next_inst, ModelAction * next_act, loc_set_iter * loc_it = loc_may_equal->iterator(); while (loc_it->hasNext()) { void * neighbor = loc_it->next(); - if (loc_act_map->contains(neighbor)) { - ModelAction * last_act = loc_act_map->get(neighbor); - FuncInst * last_inst = get_inst(last_act); + if (loc_inst_map->contains(neighbor)) { + FuncInst * last_inst = loc_inst_map->get(neighbor); struct half_pred_expr * expression = new half_pred_expr(EQUALITY, last_inst); half_pred_expressions->push_back(expression); @@ -647,19 +647,12 @@ void FuncNode::update_loc_may_equal_map(void * new_loc, loc_set_t * old_location delete loc_it; } -/* Every time a thread enters a function, set its position to the predicate tree entry */ -void FuncNode::init_predicate_tree_position(thread_id_t tid) +void FuncNode::set_predicate_tree_position(thread_id_t tid, Predicate * pred) { int thread_id = id_to_int(tid); if (predicate_tree_position.size() <= (uint) thread_id) predicate_tree_position.resize(thread_id + 1); - predicate_tree_position[thread_id] = predicate_tree_entry; -} - -void FuncNode::set_predicate_tree_position(thread_id_t tid, Predicate * pred) -{ - int thread_id = id_to_int(tid); predicate_tree_position[thread_id] = pred; } @@ -714,31 +707,42 @@ inst_act_map_t * FuncNode::get_inst_act_map(thread_id_t tid) return (*thrd_inst_act_map)[thread_id]; } -/* Make sure elements of thrd_loc_act_map are initialized properly when threads enter functions */ +void FuncNode::set_marker(thread_id_t tid) +{ + marker++; + uint thread_id = id_to_int(tid); + for (uint i = thrd_marker.size(); i < thread_id + 1; i++) { + thrd_marker.push_back(0); + } + + thrd_marker[thread_id] = marker; +} + +/* Make sure elements of maps are initialized properly when threads enter functions */ void FuncNode::init_maps(thread_id_t tid) { int thread_id = id_to_int(tid); - uint old_size = thrd_loc_act_map.size(); + uint old_size = thrd_loc_inst_map.size(); if (old_size <= (uint) thread_id) { uint new_size = thread_id + 1; - thrd_loc_act_map.resize(new_size); + thrd_loc_inst_map.resize(new_size); thrd_inst_id_map.resize(new_size); thrd_inst_pred_map.resize(new_size); - for (uint i = old_size; i < new_size;i++) { - thrd_loc_act_map[i] = new loc_act_map_t(128); + for (uint i = old_size; i < new_size; i++) { + thrd_loc_inst_map[i] = new loc_inst_map_t(128); thrd_inst_id_map[i] = new inst_id_map_t(128); thrd_inst_pred_map[i] = new inst_pred_map_t(128); } } } -/* Reset elements of thrd_loc_act_map when threads exit functions */ +/* Reset elements of maps when threads exit functions */ void FuncNode::reset_maps(thread_id_t tid) { int thread_id = id_to_int(tid); - thrd_loc_act_map[thread_id]->reset(); + thrd_loc_inst_map[thread_id]->reset(); thrd_inst_id_map[thread_id]->reset(); thrd_inst_pred_map[thread_id]->reset(); } diff --git a/funcnode.h b/funcnode.h index be0fdd86..ffc56119 100644 --- a/funcnode.h +++ b/funcnode.h @@ -9,7 +9,7 @@ #define MAX_DIST 10 typedef ModelList func_inst_list_mt; -typedef HashTable loc_act_map_t; +typedef HashTable loc_inst_map_t; typedef HashTable inst_id_map_t; typedef HashTable inst_pred_map_t; @@ -51,7 +51,6 @@ public: void add_to_val_loc_map(value_set_t * values, void * loc); void update_loc_may_equal_map(void * new_loc, loc_set_t * old_locations); - void init_predicate_tree_position(thread_id_t tid); void set_predicate_tree_position(thread_id_t tid, Predicate * pred); Predicate * get_predicate_tree_position(thread_id_t tid); @@ -77,8 +76,11 @@ private: Predicate * predicate_tree_exit; // A dummy node uint32_t exit_count; - uint32_t marker; uint32_t inst_counter; + uint32_t marker; + ModelVector thrd_marker; + + void set_marker(thread_id_t tid); /* Use source line number as the key of hashtable, to check if * atomic operation with this line number has been added or not @@ -92,13 +94,13 @@ private: func_inst_list_mt entry_insts; /* Map a FuncInst to the its predicate when updating predicate trees */ - SnapVector thrd_inst_pred_map; + ModelVector thrd_inst_pred_map; /* Number FuncInsts to detect loops when updating predicate trees */ - SnapVector thrd_inst_id_map; + ModelVector thrd_inst_id_map; /* Delect read actions at the same locations when updating predicate trees */ - SnapVector thrd_loc_act_map; + ModelVector thrd_loc_inst_map; void init_maps(thread_id_t tid); void reset_maps(thread_id_t tid); diff --git a/history.cc b/history.cc index b11614bd..762849bf 100644 --- a/history.cc +++ b/history.cc @@ -16,14 +16,14 @@ ModelHistory::ModelHistory() : func_counter(1), /* function id starts with 1 */ func_map(), func_map_rev(), - func_nodes() + func_nodes(), + last_action(NULL) { /* The following are snapshot data structures */ write_history = new HashTable(); loc_rd_func_nodes_map = new HashTable *, uintptr_t, 0>(); loc_wr_func_nodes_map = new HashTable *, uintptr_t, 0>(); loc_waiting_writes_map = new HashTable *, uintptr_t, 0>(); - thrd_func_act_lists = new SnapVector< SnapList *>(); thrd_func_list = new SnapVector(); thrd_last_entered_func = new SnapVector(); thrd_waiting_write = new SnapVector(); @@ -46,21 +46,15 @@ void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid) if ( thrd_func_list->size() <= id ) { uint oldsize = thrd_func_list->size(); thrd_func_list->resize( id + 1 ); - thrd_func_act_lists->resize( id + 1 ); for (uint i = oldsize;i < id + 1;i++) { // push 0 as a dummy function id to a void seg fault new (&(*thrd_func_list)[i]) func_id_list_t(); (*thrd_func_list)[i].push_back(0); - - (*thrd_func_act_lists)[i] = new SnapList(); thrd_last_entered_func->push_back(0); } } - SnapList * func_act_lists = (*thrd_func_act_lists)[id]; - func_act_lists->push_back( new action_list_t() ); - uint32_t last_entered_func_id = (*thrd_last_entered_func)[id]; (*thrd_last_entered_func)[id] = func_id; (*thrd_func_list)[id].push_back(func_id); @@ -85,8 +79,6 @@ void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid) void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid) { uint32_t id = id_to_int(tid); - - SnapList * func_act_lists = (*thrd_func_act_lists)[id]; uint32_t last_func_id = (*thrd_func_list)[id].back(); if (last_func_id == func_id) { @@ -94,7 +86,6 @@ void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid) func_node->function_exit_handler(tid); (*thrd_func_list)[id].pop_back(); - func_act_lists->pop_back(); } else { model_print("trying to exit with a wrong function id\n"); model_print("--- last_func: %d, func_id: %d\n", last_func_id, func_id); @@ -152,17 +143,9 @@ void ModelHistory::process_action(ModelAction *act, thread_id_t tid) if (func_id == 0 || act->get_position() == NULL) return; - SnapList * func_act_lists = (*thrd_func_act_lists)[thread_id]; - - /* The list of actions that thread tid has taken in its current function */ - action_list_t * curr_act_list = func_act_lists->back(); - - if (skip_action(act, curr_act_list)) + if (skip_action(act)) return; - /* Add to curr_inst_list */ - curr_act_list->push_back(act); - FuncNode * func_node = func_nodes[func_id]; func_node->add_inst(act); @@ -187,6 +170,7 @@ void ModelHistory::process_action(ModelAction *act, thread_id_t tid) */ func_node->update_tree(act); + last_action = act; } /* Return the FuncNode given its func_id */ @@ -432,10 +416,8 @@ SnapVector * ModelHistory::getThrdInstActMap(uint32_t func_id) return maps; } -bool ModelHistory::skip_action(ModelAction * act, SnapList * curr_act_list) +bool ModelHistory::skip_action(ModelAction * act) { - ASSERT(curr_act_list != NULL); - bool second_part_of_rmw = act->is_rmwc() || act->is_rmw(); modelclock_t curr_seq_number = act->get_seq_number(); @@ -444,9 +426,8 @@ bool ModelHistory::skip_action(ModelAction * act, SnapList * curr return true; /* Skip actions with the same sequence number */ - if (curr_act_list->size() != 0) { - ModelAction * last_act = curr_act_list->back(); - if (last_act->get_seq_number() == curr_seq_number) + if (last_action != NULL) { + if (last_action->get_seq_number() == curr_seq_number) return true; } diff --git a/history.h b/history.h index f06c2e44..dbc9f1d1 100644 --- a/history.h +++ b/history.h @@ -74,11 +74,8 @@ private: HashTable *, uintptr_t, 0> * loc_waiting_writes_map; - /* Keeps track of atomic actions that thread i has performed in some - * function. Index of SnapVector is thread id. SnapList simulates - * the call stack. - */ - SnapVector< SnapList *> * thrd_func_act_lists; + /* The last action processed by ModelHistory */ + ModelAction * last_action; /* thrd_func_list stores a list of function ids for each thread. * Each element in thrd_func_list stores the functions that @@ -95,7 +92,7 @@ private: * Manipulated by FuncNode, and needed by NewFuzzer */ HashTable *, int, 0> * func_inst_act_maps; - bool skip_action(ModelAction * act, SnapList * curr_act_list); + bool skip_action(ModelAction * act); void monitor_waiting_thread(uint32_t func_id, thread_id_t tid); void monitor_waiting_thread_counter(thread_id_t tid); diff --git a/pthread_test/CDSPass/addr-satcycle.cc b/pthread_test/CDSPass/addr-satcycle.cc deleted file mode 100755 index 84aa83d8..00000000 Binary files a/pthread_test/CDSPass/addr-satcycle.cc and /dev/null differ diff --git a/pthread_test/CDSPass/bug1.cc b/pthread_test/CDSPass/bug1.cc deleted file mode 100755 index fe715a64..00000000 Binary files a/pthread_test/CDSPass/bug1.cc and /dev/null differ diff --git a/pthread_test/CDSPass/compile.sh b/pthread_test/CDSPass/compile.sh deleted file mode 100755 index 56e324e5..00000000 --- a/pthread_test/CDSPass/compile.sh +++ /dev/null @@ -1,18 +0,0 @@ -#!/bin/sh - -# C test cases -# clang -Xclang -load -Xclang /scratch/llvm/build/lib/libCDSPass.so -c -I/scratch/random-fuzzer/include/ /scratch/random-fuzzer/test/userprog.c - -# gcc -o userprog userprog.o -L/scratch/random-fuzzer -lmodel - - -DIR=/scratch/random-fuzzer/pthread_test/CDSPass/dummy - -export LD_LIBRARY_PATH=/scratch/random-fuzzer - -# compile with CDSPass -if [ "$2" != "" ]; then # C++ - clang++ -Xclang -load -Xclang /scratch/llvm/build/lib/libCDSPass.so -g -o $DIR/$1.o -I /scratch/random-fuzzer/include -L/scratch/random-fuzzer -lmodel $1 -else # C - clang -Xclang -load -Xclang /scratch/llvm/build/lib/libCDSPass.so -o $DIR/$1.o -I/scratch/random-fuzzer/include/ -L/scratch/random-fuzzer -lmodel $1 -fi diff --git a/pthread_test/CDSPass/condvar.cc b/pthread_test/CDSPass/condvar.cc deleted file mode 100755 index f4f111be..00000000 Binary files a/pthread_test/CDSPass/condvar.cc and /dev/null differ diff --git a/pthread_test/CDSPass/deadlock.cc b/pthread_test/CDSPass/deadlock.cc deleted file mode 100755 index 76a93767..00000000 Binary files a/pthread_test/CDSPass/deadlock.cc and /dev/null differ diff --git a/pthread_test/CDSPass/insanesync.cc b/pthread_test/CDSPass/insanesync.cc deleted file mode 100755 index 00bb40d7..00000000 Binary files a/pthread_test/CDSPass/insanesync.cc and /dev/null differ diff --git a/pthread_test/CDSPass/iriw.cc b/pthread_test/CDSPass/iriw.cc deleted file mode 100755 index 8042a13b..00000000 Binary files a/pthread_test/CDSPass/iriw.cc and /dev/null differ diff --git a/pthread_test/CDSPass/iriw_wildcard.cc b/pthread_test/CDSPass/iriw_wildcard.cc deleted file mode 100755 index 1b17a2a4..00000000 Binary files a/pthread_test/CDSPass/iriw_wildcard.cc and /dev/null differ diff --git a/pthread_test/CDSPass/mo-satcycle.cc b/pthread_test/CDSPass/mo-satcycle.cc deleted file mode 100755 index 80938850..00000000 Binary files a/pthread_test/CDSPass/mo-satcycle.cc and /dev/null differ diff --git a/pthread_test/CDSPass/mutex_test.cc b/pthread_test/CDSPass/mutex_test.cc deleted file mode 100755 index 2c605c0c..00000000 Binary files a/pthread_test/CDSPass/mutex_test.cc and /dev/null differ diff --git a/pthread_test/CDSPass/pthread_mutex_test.cc b/pthread_test/CDSPass/pthread_mutex_test.cc deleted file mode 100755 index ebda3282..00000000 Binary files a/pthread_test/CDSPass/pthread_mutex_test.cc and /dev/null differ diff --git a/pthread_test/CDSPass/uninit b/pthread_test/CDSPass/uninit deleted file mode 100755 index f6b682f4..00000000 Binary files a/pthread_test/CDSPass/uninit and /dev/null differ diff --git a/pthread_test/CDSPass/uninit.cc b/pthread_test/CDSPass/uninit.cc deleted file mode 100755 index f6b682f4..00000000 Binary files a/pthread_test/CDSPass/uninit.cc and /dev/null differ diff --git a/pthread_test/addr-satcycle.cc b/pthread_test/addr-satcycle.cc deleted file mode 100644 index a3d970b9..00000000 --- a/pthread_test/addr-satcycle.cc +++ /dev/null @@ -1,69 +0,0 @@ -/** - * @file addr-satcycle.cc - * @brief Address-based satisfaction cycle test - * - * This program has a peculiar behavior which is technically legal under the - * current C++ memory model but which is a result of a type of satisfaction - * cycle. We use this as justification for part of our modifications to the - * memory model when proving our model-checker's correctness. - */ - -#include -#include -#include - -#include "model-assert.h" - -using namespace std; - -atomic_int x[2], idx, y; - -int r1, r2, r3; /* "local" variables */ - -static void *a(void *obj) -{ - r1 = idx.load(memory_order_relaxed); - x[r1].store(0, memory_order_relaxed); - - /* Key point: can we guarantee that &x[0] == &x[r1]? */ - r2 = x[0].load(memory_order_relaxed); - y.store(r2); - return NULL; -} - -static void *b(void *obj) -{ - r3 = y.load(memory_order_relaxed); - idx.store(r3, memory_order_relaxed); - return NULL; -} - -int user_main(int argc, char **argv) -{ - pthread_t t1, t2; - - atomic_init(&x[0], 1); - atomic_init(&idx, 0); - atomic_init(&y, 0); - - printf("Main thread: creating 2 threads\n"); - pthread_create(&t1,NULL, &a, NULL); - pthread_create(&t2,NULL, &b, NULL); - - pthread_join(t1,NULL); - pthread_join(t2,NULL); - printf("Main thread is finished\n"); - - printf("r1 = %d\n", r1); - printf("r2 = %d\n", r2); - printf("r3 = %d\n", r3); - - /* - * This condition should not be hit because it only occurs under a - * satisfaction cycle - */ - bool cycle = (r1 == 1 && r2 == 1 && r3 == 1); - MODEL_ASSERT(!cycle); - - return 0; -} diff --git a/pthread_test/bug1.cc b/pthread_test/bug1.cc deleted file mode 100644 index 16d2b594..00000000 --- a/pthread_test/bug1.cc +++ /dev/null @@ -1,74 +0,0 @@ -/** - * @file iriw.cc - * @brief Independent read and independent write test - */ - -#include -#include -#include - -#define N 14 -//#include "wildcard.h" -//#include "model-assert.h" - -using namespace std; - -std::atomic_int x, y; -int r1, r2, r3, r4; /* "local" variables */ - -static void *a(void *obj) -{ -// x.store(1, memory_order_seq_cst); - return NULL; -} - - -static void *b(void *obj) -{ - y.store(1, memory_order_seq_cst); - return NULL; -} - -static void *c(void *obj) -{ - r1 = x.load(memory_order_acquire); - r2 = y.load(memory_order_seq_cst); - return NULL; -} - -static void *d(void *obj) -{ - r3 = y.load(memory_order_acquire); - r4 = x.load(memory_order_seq_cst); - return NULL; -} - - -int user_main(int argc, char **argv) -{ - pthread_t threads[20]; - - atomic_init(&x, 0); - atomic_init(&y, 0); - - printf("Main thread: creating %d threads\n", N); - - for (int i = 0; i< N; i++) - pthread_create(&threads[i],NULL, &a, NULL); - - for (int i=0; i - -#include "pthread.h" -#include "librace.h" -#include "stdatomic.h" -#include "mutex.h" -#include - -cdsc::mutex * m; -cdsc::condition_variable *v; -int shareddata; - -static void *a(void *obj) -{ - m->lock(); - while(load_32(&shareddata)==0) - v->wait(*m); - m->unlock(); - return NULL; -} - -static void *b(void *obj) -{ - m->lock(); - store_32(&shareddata, (unsigned int) 1); - v->notify_all(); - m->unlock(); - return NULL; -} - -int user_main(int argc, char **argv) -{ - pthread_t t1, t2; - store_32(&shareddata, (unsigned int) 0); - m=new cdsc::mutex(); - v=new cdsc::condition_variable(); - - pthread_create(&t1,NULL, &a, NULL); - pthread_create(&t2,NULL, &b, NULL); - - pthread_join(t1,NULL); - pthread_join(t2,NULL); - return 0; -} diff --git a/pthread_test/deadlock.cc b/pthread_test/deadlock.cc deleted file mode 100644 index 43828192..00000000 --- a/pthread_test/deadlock.cc +++ /dev/null @@ -1,47 +0,0 @@ -#include -#include - -#include "librace.h" - -pthread_mutex_t x; -pthread_mutex_t y; -uint32_t shared = 0; - -static void *a(void *obj) -{ - pthread_mutex_lock(&x); - pthread_mutex_lock(&y); - printf("shared = %u\n", load_32(&shared)); - pthread_mutex_unlock(&y); - pthread_mutex_unlock(&x); - return NULL; -} - -static void *b(void *obj) -{ - pthread_mutex_lock(&y); - pthread_mutex_lock(&x); - store_32(&shared, 16); - printf("write shared = 16\n"); - pthread_mutex_unlock(&x); - pthread_mutex_unlock(&y); - return NULL; -} - -int user_main(int argc, char **argv) -{ - pthread_t t1, t2; - - pthread_mutex_init(&x, NULL); - pthread_mutex_init(&y, NULL); - - printf("Main thread: creating 2 threads\n"); - pthread_create(&t1,NULL, &a, NULL); - pthread_create(&t2,NULL, &b, NULL); - - pthread_join(t1,NULL); - pthread_join(t2,NULL); - printf("Main thread is finished\n"); - - return 0; -} diff --git a/pthread_test/insanesync.cc b/pthread_test/insanesync.cc deleted file mode 100644 index bcc34ad7..00000000 --- a/pthread_test/insanesync.cc +++ /dev/null @@ -1,72 +0,0 @@ -#include -#include -#include -#include - -#include "librace.h" -#include "model-assert.h" - -using namespace std; - -atomic_int x, y; -atomic_intptr_t z, z2; - -int r1, r2, r3; /* "local" variables */ - -/** - This example illustrates a self-satisfying cycle involving - synchronization. A failed synchronization creates the store that - causes the synchronization to fail. - - The C++11 memory model nominally allows r1=0, r2=1, r3=5. - - This example is insane, we don't support that behavior. -*/ - - -static void *a(void *obj) -{ - z.store((intptr_t)&y, memory_order_relaxed); - r1 = y.fetch_add(1, memory_order_release); - z.store((intptr_t)&x, memory_order_relaxed); - r2 = y.fetch_add(1, memory_order_release); - return NULL; -} - - -static void *b(void *obj) -{ - r3 = y.fetch_add(1, memory_order_acquire); - intptr_t ptr = z.load(memory_order_relaxed); - z2.store(ptr, memory_order_relaxed); - return NULL; -} - -static void *c(void *obj) -{ - atomic_int *ptr2 = (atomic_int *)z2.load(memory_order_relaxed); - (*ptr2).store(5, memory_order_relaxed); - return NULL; -} - -int user_main(int argc, char **argv) -{ - pthread_t t1, t2, t3; - - atomic_init(&x, 0); - atomic_init(&y, 0); - atomic_init(&z, (intptr_t) &x); - atomic_init(&z2, (intptr_t) &x); - - pthread_create(&t1,NULL, &a, NULL); - pthread_create(&t2,NULL, &b, NULL); - pthread_create(&t3,NULL, &c, NULL); - - pthread_join(t1,NULL); - pthread_join(t2,NULL); - pthread_join(t3,NULL); - - printf("r1=%d, r2=%d, r3=%d\n", r1, r2, r3); - - return 0; -} diff --git a/pthread_test/iriw.cc b/pthread_test/iriw.cc deleted file mode 100644 index 42ba9364..00000000 --- a/pthread_test/iriw.cc +++ /dev/null @@ -1,71 +0,0 @@ -/** - * @file iriw.cc - * @brief Independent read and independent write test - */ - -#include -#include -#include - -#include "wildcard.h" -#include "model-assert.h" - -using namespace std; - -atomic_int x, y; -int r1, r2, r3, r4; /* "local" variables */ - -static void *a(void *obj) -{ - x.store(1, memory_order_seq_cst); - return new int(1); -} - -static void *b(void *obj) -{ - y.store(1, memory_order_seq_cst); - return new int(2); -} - -static void *c(void *obj) -{ - r1 = x.load(memory_order_acquire); - r2 = y.load(memory_order_seq_cst); - return new int(3); -} - -static void *d(void *obj) -{ - r3 = y.load(memory_order_acquire); - r4 = x.load(memory_order_seq_cst); - return new int(4); -} - - -int user_main(int argc, char **argv) -{ - pthread_t t1, t2, t3, t4; - - atomic_init(&x, 0); - atomic_init(&y, 0); - - printf("Main thread: creating 4 threads\n"); - pthread_create(&t1,NULL, &a, NULL); - pthread_create(&t2,NULL, &b, NULL); - pthread_create(&t3,NULL, &c, NULL); - pthread_create(&t4,NULL, &d, NULL); - - pthread_join(t1,NULL); - pthread_join(t2,NULL); - pthread_join(t3,NULL); - pthread_join(t4,NULL); - printf("Main thread is finished\n"); - - /* - * This condition should not be hit if the execution is SC */ - bool sc = (r1 == 1 && r2 == 0 && r3 == 1 && r4 == 0); - printf("r1 = %d, r2 = %d, r3 = %d and r4 = %d\n", r1, r2, r3, r4); - MODEL_ASSERT(!sc); - - return 0; -} diff --git a/pthread_test/iriw_wildcard.cc b/pthread_test/iriw_wildcard.cc deleted file mode 100644 index adea420f..00000000 --- a/pthread_test/iriw_wildcard.cc +++ /dev/null @@ -1,70 +0,0 @@ -/** - * @file iriw.cc - * @brief Independent read and independent write test - */ - -#include -#include -#include - -#include "wildcard.h" -#include "model-assert.h" - -using namespace std; - -atomic_int x, y; -int r1, r2, r3, r4; /* "local" variables */ - -static void *a(void *obj) -{ - x.store(1, wildcard(1)); - return NULL; -} - -static void *b(void *obj) -{ - y.store(1, wildcard(2)); - return NULL; -} - -static void *c(void *obj) -{ - r1 = x.load(wildcard(3)); - r2 = y.load(wildcard(4)); - return NULL; -} - -static void *d(void *obj) -{ - r3 = y.load(wildcard(5)); - r4 = x.load(wildcard(6)); - return NULL; -} - - -int user_main(int argc, char **argv) -{ - pthread_t t1, t2, t3, t4; - - atomic_init(&x, 0); - atomic_init(&y, 0); - - printf("Main thread: creating 4 threads\n"); - pthread_create(&t1,NULL, &a, NULL); - pthread_create(&t2,NULL, &b, NULL); - pthread_create(&t3,NULL, &c, NULL); - pthread_create(&t4,NULL, &d, NULL); - - pthread_join(t1,NULL); - pthread_join(t2,NULL); - pthread_join(t3,NULL); - pthread_join(t4,NULL); - printf("Main thread is finished\n"); - - /* - * This condition should not be hit if the execution is SC */ - bool sc = (r1 == 1 && r2 == 0 && r3 == 1 && r4 == 0); - //MODEL_ASSERT(!sc); - - return 0; -} diff --git a/pthread_test/mo-satcycle.cc b/pthread_test/mo-satcycle.cc deleted file mode 100644 index d0a60559..00000000 --- a/pthread_test/mo-satcycle.cc +++ /dev/null @@ -1,71 +0,0 @@ -/** - * @file mo-satcycle.cc - * @brief MO satisfaction cycle test - * - * This program has a peculiar behavior which is technically legal under the - * current C++ memory model but which is a result of a type of satisfaction - * cycle. We use this as justification for part of our modifications to the - * memory model when proving our model-checker's correctness. - */ - -#include -#include -#include - -#include "model-assert.h" - -using namespace std; - -atomic_int x, y; -int r0, r1, r2, r3; /* "local" variables */ - -static void *a(void *obj) -{ - y.store(10, memory_order_relaxed); - x.store(1, memory_order_release); - return NULL; -} - -static void *b(void *obj) -{ - r0 = x.load(memory_order_relaxed); - r1 = x.load(memory_order_acquire); - y.store(11, memory_order_relaxed); - return NULL; -} - -static void *c(void *obj) -{ - r2 = y.load(memory_order_relaxed); - r3 = y.load(memory_order_relaxed); - if (r2 == 11 && r3 == 10) - x.store(0, memory_order_relaxed); - return NULL; -} - -int user_main(int argc, char **argv) -{ - pthread_t t1, t2, t3; - - atomic_init(&x, 0); - atomic_init(&y, 0); - - printf("Main thread: creating 3 threads\n"); - pthread_create(&t1,NULL, &a, NULL); - pthread_create(&t2,NULL, &b, NULL); - pthread_create(&t3,NULL, &c, NULL); - - pthread_join(t1,NULL); - pthread_join(t2,NULL); - pthread_join(t3,NULL); - printf("Main thread is finished\n"); - - /* - * This condition should not be hit because it only occurs under a - * satisfaction cycle - */ - bool cycle = (r0 == 1 && r1 == 0 && r2 == 11 && r3 == 10); - MODEL_ASSERT(!cycle); - - return 0; -} diff --git a/pthread_test/normal_compile.sh b/pthread_test/normal_compile.sh deleted file mode 100755 index 56cba5a5..00000000 --- a/pthread_test/normal_compile.sh +++ /dev/null @@ -1,9 +0,0 @@ -#g++ -o test.o test.cc -Wall -g -O3 -I.. -I../include -L.. -lmodel - -export LD_LIBRARY_PATH=/scratch/random-fuzzer - -if [ "$2" != "" ]; then - g++ -o "$1.o" $1 -Wall -g -O3 -I.. -I../include -L.. -lmodel -else - gcc -o "$1.o" $1 -Wall -g -O3 -I.. -I../include -L.. -lmodel -fi diff --git a/pthread_test/protect/mutex_test.cc b/pthread_test/protect/mutex_test.cc deleted file mode 100644 index 9a84b1d1..00000000 --- a/pthread_test/protect/mutex_test.cc +++ /dev/null @@ -1,41 +0,0 @@ -#include - -#include "threads.h" -#include "librace.h" -#include "stdatomic.h" -#include - -int shareddata; -pthread_mutex_t m; - -static void* a(void *obj) -{ - int i; - for(i=0;i<2;i++) { - if ((i%2)==0) { - pthread_mutex_lock(&m); - store_32(&shareddata,(unsigned int)i); - printf("shareddata: %d\n", shareddata); - pthread_mutex_unlock(&m); - } else { - while(!pthread_mutex_trylock(&m)) - thrd_yield(); - store_32(&shareddata,(unsigned int)i); - printf("shareddata: %d\n", shareddata); - pthread_mutex_unlock(&m); - } - } -} - -int user_main(int argc, char **argv) -{ - thrd_t t1, t2; - pthread_mutex_init(&m, NULL); - - thrd_create(&t1, (thrd_start_t)&a, NULL); - thrd_create(&t2, (thrd_start_t)&a, NULL); - - thrd_join(t1); - thrd_join(t2); - return 0; -} diff --git a/pthread_test/pthread_mutex_test.cc b/pthread_test/pthread_mutex_test.cc deleted file mode 100644 index 55bea220..00000000 --- a/pthread_test/pthread_mutex_test.cc +++ /dev/null @@ -1,69 +0,0 @@ -#include -#include -#define NTHREADS 2 -void *thread_function(void *); -//pthread_mutex_t mutex1; - -int counter=0; - -class Box { -public: -// int counter; - - static Box& getInstance() { - static Box instance; - return instance; - } - - void addone() { - pthread_mutex_lock(&pool_mutex); - counter++; - pthread_mutex_unlock(&pool_mutex); - } - -private: - Box() { - pthread_mutex_init(&pool_mutex, NULL); - counter = 0; - } - pthread_mutex_t pool_mutex; -}; - -int user_main(int argv, char **argc) -{ -// void *dummy = NULL; -// pthread_mutex_init(&mutex1, NULL); /* PTHREAD_MUTEX_INITIALIZER;*/ - -// pthread_t thread_id[NTHREADS]; -// int i, j; - - Box::getInstance().addone(); - -/* for(i=0; i < NTHREADS; i++) - { - pthread_create( &thread_id[i], NULL, &thread_function, NULL ); - } - - for(j=0; j < NTHREADS; j++) - { - pthread_join( thread_id[j], NULL); - } -*/ - - printf("Final counter value: %d\n", counter); - /* - for (i=0;i -#include -#include -#include - -#define N 4 -//#include "wildcard.h" -//#include "model-assert.h" - -using namespace std; - -atomic x(1); -atomic y(1); - -int r1, r2, r3, r4; /* "local" variables */ - -static void *a(void *obj) -{ - x.store(1, memory_order_relaxed); - y.store(1, memory_order_relaxed); - - return new int(1); -} - - -static void *b(void *obj) -{ - y.store(1, memory_order_relaxed); - - return new int(2); -} - -static void *c(void *obj) -{ - r1 = x.load(memory_order_acquire); - r2 = y.load(memory_order_relaxed); - - return new int(3); -} - -static void *d(void *obj) -{ - r3 = y.load(memory_order_acquire); - r4 = x.load(memory_order_relaxed); - - return new int(4); -} - - -int main(int argc, char **argv) -{ - printf("Main thread starts\n"); - - x.store(2, memory_order_relaxed); - y.store(2, memory_order_relaxed); - - r1 = x.load(memory_order_relaxed); - printf("%d\n", r1); - -// x.compare_exchange_strong(r1, r2); -// r3 = x.load(memory_order_relaxed); - -// printf("%d\n", r3); - - printf("Main thread is finished\n"); - - return 0; -} diff --git a/pthread_test/uninit.cc b/pthread_test/uninit.cc deleted file mode 100644 index 075e2acf..00000000 --- a/pthread_test/uninit.cc +++ /dev/null @@ -1,57 +0,0 @@ -/** - * @file uninit.cc - * @brief Uninitialized loads test - * - * This is a test of the "uninitialized loads" code. While we don't explicitly - * initialize y, this example's synchronization pattern should guarantee we - * never see it uninitialized. - */ -#include -#include -#include - -//#include "librace.h" - -std::atomic_int x; -std::atomic_int y; - -static void *a(void *obj) -{ - int flag = x.load(std::memory_order_acquire); - printf("flag: %d\n", flag); - if (flag == 2) - printf("Load: %d\n", y.load(std::memory_order_relaxed)); - return NULL; -} - -static void *b(void *obj) -{ - printf("fetch_add: %d\n", x.fetch_add(1, std::memory_order_relaxed)); - return NULL; -} - -static void *c(void *obj) -{ - y.store(3, std::memory_order_relaxed); - x.store(1, std::memory_order_release); - return NULL; -} - -int user_main(int argc, char **argv) -{ - pthread_t t1, t2, t3; - - std::atomic_init(&x, 0); - - printf("Main thread: creating 3 threads\n"); - pthread_create(&t1,NULL, &a, NULL); - pthread_create(&t2,NULL, &b, NULL); - pthread_create(&t3,NULL, &c, NULL); - - pthread_join(t1,NULL); - pthread_join(t2,NULL); - pthread_join(t3,NULL); - printf("Main thread is finished\n"); - - return 0; -}