Remove redundant data structures and FuncNode's dependencies on old actions
authorweiyu <weiyuluo1232@gmail.com>
Wed, 12 Feb 2020 00:21:30 +0000 (16:21 -0800)
committerweiyu <weiyuluo1232@gmail.com>
Wed, 12 Feb 2020 00:21:30 +0000 (16:21 -0800)
32 files changed:
funcinst.cc
funcinst.h
funcnode.cc
funcnode.h
history.cc
history.h
pthread_test/CDSPass/addr-satcycle.cc [deleted file]
pthread_test/CDSPass/bug1.cc [deleted file]
pthread_test/CDSPass/compile.sh [deleted file]
pthread_test/CDSPass/condvar.cc [deleted file]
pthread_test/CDSPass/deadlock.cc [deleted file]
pthread_test/CDSPass/insanesync.cc [deleted file]
pthread_test/CDSPass/iriw.cc [deleted file]
pthread_test/CDSPass/iriw_wildcard.cc [deleted file]
pthread_test/CDSPass/mo-satcycle.cc [deleted file]
pthread_test/CDSPass/mutex_test.cc [deleted file]
pthread_test/CDSPass/pthread_mutex_test.cc [deleted file]
pthread_test/CDSPass/uninit [deleted file]
pthread_test/CDSPass/uninit.cc [deleted file]
pthread_test/addr-satcycle.cc [deleted file]
pthread_test/bug1.cc [deleted file]
pthread_test/condvar.cc [deleted file]
pthread_test/deadlock.cc [deleted file]
pthread_test/insanesync.cc [deleted file]
pthread_test/iriw.cc [deleted file]
pthread_test/iriw_wildcard.cc [deleted file]
pthread_test/mo-satcycle.cc [deleted file]
pthread_test/normal_compile.sh [deleted file]
pthread_test/protect/mutex_test.cc [deleted file]
pthread_test/pthread_mutex_test.cc [deleted file]
pthread_test/test.cc [deleted file]
pthread_test/uninit.cc [deleted file]

index d4288a1..4c58445 100644 (file)
@@ -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 */
index 79ec01a..ca733f6 100644 (file)
@@ -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<uint64_t> associated_reads;
+       ModelVector<uint32_t> thrd_marker;
 
        /**
         * Collisions store a list of FuncInsts with the same position
index a0850c7..ff62a52 100644 (file)
 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<void *, value_set_t *, uintptr_t, 0> * write_history = history->getWriteHistory();
-       HashSet<ModelAction *, uintptr_t, 2> 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<Predicate *> * 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();
 }
index be0fdd8..ffc5611 100644 (file)
@@ -9,7 +9,7 @@
 #define MAX_DIST 10
 
 typedef ModelList<FuncInst *> func_inst_list_mt;
-typedef HashTable<void *, ModelAction *, uintptr_t, 0, model_malloc, model_calloc, model_free> loc_act_map_t;
+typedef HashTable<void *, FuncInst *, uintptr_t, 0, model_malloc, model_calloc, model_free> loc_inst_map_t;
 typedef HashTable<FuncInst *, uint32_t, uintptr_t, 0, model_malloc, model_calloc, model_free> inst_id_map_t;
 typedef HashTable<FuncInst *, Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> 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<uint32_t> 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<inst_pred_map_t *> thrd_inst_pred_map;
+       ModelVector<inst_pred_map_t *> thrd_inst_pred_map;
 
        /* Number FuncInsts to detect loops when updating predicate trees */
-       SnapVector<inst_id_map_t *> thrd_inst_id_map;
+       ModelVector<inst_id_map_t *> thrd_inst_id_map;
 
        /* Delect read actions at the same locations when updating predicate trees */
-       SnapVector<loc_act_map_t *> thrd_loc_act_map;
+       ModelVector<loc_inst_map_t *> thrd_loc_inst_map;
 
        void init_maps(thread_id_t tid);
        void reset_maps(thread_id_t tid);
index b11614b..762849b 100644 (file)
@@ -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<void *, value_set_t *, uintptr_t, 0>();
        loc_rd_func_nodes_map = new HashTable<void *, SnapVector<FuncNode *> *, uintptr_t, 0>();
        loc_wr_func_nodes_map = new HashTable<void *, SnapVector<FuncNode *> *, uintptr_t, 0>();
        loc_waiting_writes_map = new HashTable<void *, SnapVector<ConcretePredicate *> *, uintptr_t, 0>();
-       thrd_func_act_lists = new SnapVector< SnapList<action_list_t *> *>();
        thrd_func_list = new SnapVector<func_id_list_t>();
        thrd_last_entered_func = new SnapVector<uint32_t>();
        thrd_waiting_write = new SnapVector<ConcretePredicate *>();
@@ -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<action_list_t *>();
                        thrd_last_entered_func->push_back(0);
                }
        }
 
-       SnapList<action_list_t *> * 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<action_list_t *> * 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<action_list_t *> * 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<inst_act_map_t *> * ModelHistory::getThrdInstActMap(uint32_t func_id)
        return maps;
 }
 
-bool ModelHistory::skip_action(ModelAction * act, SnapList<ModelAction *> * 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<ModelAction *> * 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;
        }
 
index f06c2e4..dbc9f1d 100644 (file)
--- a/history.h
+++ b/history.h
@@ -74,11 +74,8 @@ private:
 
        HashTable<void *, SnapVector<ConcretePredicate *> *, 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<action_list_t *> *> * 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<uint32_t, SnapVector<inst_act_map_t *> *, int, 0> * func_inst_act_maps;
 
-       bool skip_action(ModelAction * act, SnapList<ModelAction *> * 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 (executable)
index 84aa83d..0000000
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 (executable)
index fe715a6..0000000
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 (executable)
index 56e324e..0000000
+++ /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 (executable)
index f4f111b..0000000
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 (executable)
index 76a9376..0000000
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 (executable)
index 00bb40d..0000000
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 (executable)
index 8042a13..0000000
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 (executable)
index 1b17a2a..0000000
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 (executable)
index 8093885..0000000
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 (executable)
index 2c605c0..0000000
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 (executable)
index ebda328..0000000
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 (executable)
index f6b682f..0000000
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 (executable)
index f6b682f..0000000
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 (file)
index a3d970b..0000000
+++ /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 <atomic>
-#include <pthread.h>
-#include <stdio.h>
-
-#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 (file)
index 16d2b59..0000000
+++ /dev/null
@@ -1,74 +0,0 @@
-/**
- * @file iriw.cc
- * @brief Independent read and independent write test
- */
-
-#include <atomic>
-#include <pthread.h>
-#include <stdio.h>
-
-#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<N; i++)
-               printf("thread id: %ld\n", threads[i]);
-
-       for (int i = 0; i< N; i++)
-               pthread_join( threads[i],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/condvar.cc b/pthread_test/condvar.cc
deleted file mode 100644 (file)
index aae622b..0000000
+++ /dev/null
@@ -1,44 +0,0 @@
-#include <stdio.h>
-
-#include "pthread.h"
-#include "librace.h"
-#include "stdatomic.h"
-#include "mutex.h"
-#include <condition_variable>
-
-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 (file)
index 4382819..0000000
+++ /dev/null
@@ -1,47 +0,0 @@
-#include <stdio.h>
-#include <pthread.h>
-
-#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 (file)
index bcc34ad..0000000
+++ /dev/null
@@ -1,72 +0,0 @@
-#include <stdlib.h>
-#include <stdio.h>
-#include <pthread.h>
-#include <atomic>
-
-#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 (file)
index 42ba936..0000000
+++ /dev/null
@@ -1,71 +0,0 @@
-/**
- * @file iriw.cc
- * @brief Independent read and independent write test
- */
-
-#include <atomic>
-#include <pthread.h>
-#include <stdio.h>
-
-#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 (file)
index adea420..0000000
+++ /dev/null
@@ -1,70 +0,0 @@
-/**
- * @file iriw.cc
- * @brief Independent read and independent write test
- */
-
-#include <atomic>
-#include <pthread.h>
-#include <stdio.h>
-
-#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 (file)
index d0a6055..0000000
+++ /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 <atomic>
-#include <pthread.h>
-#include <stdio.h>
-
-#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 (executable)
index 56cba5a..0000000
+++ /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 (file)
index 9a84b1d..0000000
+++ /dev/null
@@ -1,41 +0,0 @@
-#include <stdio.h> 
-#include "threads.h" 
-#include "librace.h" 
-#include "stdatomic.h" 
-#include <pthread.h>
-
-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 (file)
index 55bea22..0000000
+++ /dev/null
@@ -1,69 +0,0 @@
-#include <stdio.h>
-#include <pthread.h>
-#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<NTHREADS; i++) {
-      printf("id %ld\n", thread_id[i]);
-   }*/
-   return 0;
-}
-
-void *thread_function(void *dummyPtr)
-{
-//   printf("Thread number %ld\n", pthread_self());
-   Box::getInstance().addone();
-//   pthread_mutex_lock( &mutex1 );
-//   Box::getInstance().counter++;
-//   pthread_mutex_unlock( &mutex1 );
-   return NULL;
-}
diff --git a/pthread_test/test.cc b/pthread_test/test.cc
deleted file mode 100644 (file)
index f5b0857..0000000
+++ /dev/null
@@ -1,73 +0,0 @@
-/**
- * @file iriw.cc
- * @brief Independent read and independent write test
- */
-
-#include <atomic>
-#include <pthread.h>
-#include <stdio.h>
-#include <iostream>
-
-#define N 4
-//#include "wildcard.h"
-//#include "model-assert.h"
-
-using namespace std;
-
-atomic<int> x(1);
-atomic<int> 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 (file)
index 075e2ac..0000000
+++ /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 <stdio.h>
-#include <pthread.h>
-#include <atomic>
-
-//#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;
-}