}
/* Transfer all outgoing edges from the from node to the rmw node */
- /* This process should not add a cycle because either:
+ /* This process should not add a cycle because either:
* (1) The rmw should not have any incoming edges yet if it is the
* new node or
- * (2) the fromnode is the new node and therefore it should not
+ * (2) the fromnode is the new node and therefore it should not
* have any outgoing edges.
*/
std::vector<CycleNode *> * edges=fromnode->getEdges();
return next;
}
-
/**
* Processes a read or rmw model action.
* @param curr is the read model action to process.
* @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
* @return True if processing this read updates the mo_graph.
*/
-
bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part_of_rmw) {
uint64_t value;
bool updated=false;
add_action_to_lists(curr);
check_curr_backtracking(curr);
-
+
set_backtracking(curr);
return get_next_thread(curr);
void ModelChecker::check_curr_backtracking(ModelAction * curr) {
Node *currnode = curr->get_node();
Node *parnode = currnode->get_parent();
-
+
if ((!parnode->backtrack_empty() ||
!currnode->read_from_empty() ||
!currnode->future_value_empty() ||
}
}
-
bool ModelChecker::promises_expired() {
for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
Promise *promise = (*promises)[promise_index];
return true;
}
-
/**
* Finds the head(s) of the release sequence(s) containing a given ModelAction.
* The ModelAction under consideration is expected to be taking part in
return resolved;
}
-
-
/**
* Compute the set of promises that could potentially be satisfied by this
* action. Note that the set computation actually appears in the Node, not in
private:
/** The scheduler to use: tracks the running/ready Threads */
Scheduler *scheduler;
-
+
bool thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader);
bool has_asserted() {return asserted;}
void reset_asserted() {asserted=false;}
bool resolve_promises(ModelAction *curr);
void compute_promises(ModelAction *curr);
-
void check_curr_backtracking(ModelAction * curr);
void add_action_to_lists(ModelAction *act);
ModelAction * get_last_action(thread_id_t tid);
#include "librace.h"
#include "stdatomic.h"
-
#define RW_LOCK_BIAS 0x00100000
#define WRITE_LOCK_CMP RW_LOCK_BIAS
/** Example implementation of linux rw lock along with 2 thread test
* driver... */
-
typedef union {
atomic_int lock;
} rwlock_t;
int priorvalue=atomic_fetch_sub_explicit(&rw->lock, 1, memory_order_acquire);
if (priorvalue>0)
return 1;
-
+
atomic_fetch_add_explicit(&rw->lock, 1, memory_order_relaxed);
return 0;
}
int priorvalue=atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_acquire);
if (priorvalue==RW_LOCK_BIAS)
return 1;
-
+
atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_relaxed);
return 0;
}
thrd_create(&t1, (thrd_start_t)&a, NULL);
thrd_create(&t2, (thrd_start_t)&a, NULL);
-
+
thrd_join(t1);
thrd_join(t2);
}