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);
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 */
#include "action.h"
#include "hashtable.h"
+#include "threads-model.h"
class ModelAction;
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();
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
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(),
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);
}
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;
{
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];
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);
// Add to the set of backedges
curr_pred->add_backedge(back_pred);
curr_pred = back_pred;
+
continue;
}
}
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);
{
/* 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];
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)
{
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() ) {
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);
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;
}
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();
}
#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;
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);
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
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);
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 *>();
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);
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) {
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);
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);
*/
func_node->update_tree(act);
+ last_action = act;
}
/* Return the FuncNode given its 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();
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;
}
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
* 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);
+++ /dev/null
-#!/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
+++ /dev/null
-/**
- * @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;
-}
+++ /dev/null
-/**
- * @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;
-}
+++ /dev/null
-#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;
-}
+++ /dev/null
-#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;
-}
+++ /dev/null
-#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;
-}
+++ /dev/null
-/**
- * @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;
-}
+++ /dev/null
-/**
- * @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;
-}
+++ /dev/null
-/**
- * @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;
-}
+++ /dev/null
-#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
+++ /dev/null
-#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;
-}
+++ /dev/null
-#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;
-}
+++ /dev/null
-/**
- * @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;
-}
+++ /dev/null
-/**
- * @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;
-}
projects / c11tester.git / commitdiff