+ * Checks whether a thread has read from the same write for too many times
+ * without seeing the effects of a later write.
+ *
+ * Basic idea:
+ * 1) there must a different write that we could read from that would satisfy the modification order,
+ * 2) we must have read from the same value in excess of maxreads times, and
+ * 3) that other write must have been in the reads_from set for maxreads times.
+ *
+ * If so, we decide that the execution is no longer feasible.
+ */
+void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
+ if (params.maxreads != 0) {
+
+ if (curr->get_node()->get_read_from_size() <= 1)
+ return;
+ //Must make sure that execution is currently feasible... We could
+ //accidentally clear by rolling back
+ if (!isfeasible())
+ return;
+ std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+ int tid = id_to_int(curr->get_tid());
+
+ /* Skip checks */
+ if ((int)thrd_lists->size() <= tid)
+ return;
+ action_list_t *list = &(*thrd_lists)[tid];
+
+ action_list_t::reverse_iterator rit = list->rbegin();
+ /* Skip past curr */
+ for (; (*rit) != curr; rit++)
+ ;
+ /* go past curr now */
+ rit++;
+
+ action_list_t::reverse_iterator ritcopy = rit;
+ //See if we have enough reads from the same value
+ int count = 0;
+ for (; count < params.maxreads; rit++,count++) {
+ if (rit==list->rend())
+ return;
+ ModelAction *act = *rit;
+ if (!act->is_read())
+ return;
+
+ if (act->get_reads_from() != rf)
+ return;
+ if (act->get_node()->get_read_from_size() <= 1)
+ return;
+ }
+ for (int i = 0; i<curr->get_node()->get_read_from_size(); i++) {
+ //Get write
+ const ModelAction * write = curr->get_node()->get_read_from_at(i);
+
+ //Need a different write
+ if (write==rf)
+ continue;
+
+ /* Test to see whether this is a feasible write to read from*/
+ mo_graph->startChanges();
+ r_modification_order(curr, write);
+ bool feasiblereadfrom = isfeasible();
+ mo_graph->rollbackChanges();
+
+ if (!feasiblereadfrom)
+ continue;
+ rit = ritcopy;
+
+ bool feasiblewrite = true;
+ //new we need to see if this write works for everyone
+
+ for (int loop = count; loop>0; loop--,rit++) {
+ ModelAction *act=*rit;
+ bool foundvalue = false;
+ for (int j = 0; j<act->get_node()->get_read_from_size(); j++) {
+ if (act->get_node()->get_read_from_at(i)==write) {
+ foundvalue = true;
+ break;
+ }
+ }
+ if (!foundvalue) {
+ feasiblewrite = false;
+ break;
+ }
+ }
+ if (feasiblewrite) {
+ too_many_reads = true;
+ return;
+ }
+ }
+ }
+}
+
+/**
+ * Updates the mo_graph with the constraints imposed from the current
+ * read.
+ *
+ * Basic idea is the following: Go through each other thread and find
+ * the lastest action that happened before our read. Two cases:
+ *
+ * (1) The action is a write => that write must either occur before
+ * the write we read from or be the write we read from.
+ *
+ * (2) The action is a read => the write that that action read from
+ * must occur before the write we read from or be the same write.
+ *
+ * @param curr The current action. Must be a read.
+ * @param rf The action that curr reads from. Must be a write.
+ * @return True if modification order edges were added; false otherwise
+ */
+bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf)
+{
+ std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+ unsigned int i;
+ bool added = false;
+ ASSERT(curr->is_read());
+
+ /* Iterate over all threads */
+ for (i = 0; i < thrd_lists->size(); i++) {
+ /* Iterate over actions in thread, starting from most recent */
+ action_list_t *list = &(*thrd_lists)[i];
+ action_list_t::reverse_iterator rit;
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *act = *rit;
+
+ /*
+ * Include at most one act per-thread that "happens
+ * before" curr. Don't consider reflexively.
+ */
+ if (act->happens_before(curr) && act != curr) {
+ if (act->is_write()) {
+ if (rf != act) {
+ mo_graph->addEdge(act, rf);
+ added = true;
+ }
+ } else {
+ const ModelAction *prevreadfrom = act->get_reads_from();
+ if (prevreadfrom != NULL && rf != prevreadfrom) {
+ mo_graph->addEdge(prevreadfrom, rf);
+ added = true;
+ }
+ }
+ break;
+ }
+ }
+ }
+
+ return added;
+}
+
+/** This method fixes up the modification order when we resolve a
+ * promises. The basic problem is that actions that occur after the
+ * read curr could not property add items to the modification order
+ * for our read.
+ *
+ * So for each thread, we find the earliest item that happens after
+ * the read curr. This is the item we have to fix up with additional
+ * constraints. If that action is write, we add a MO edge between
+ * the Action rf and that action. If the action is a read, we add a
+ * MO edge between the Action rf, and whatever the read accessed.
+ *
+ * @param curr is the read ModelAction that we are fixing up MO edges for.
+ * @param rf is the write ModelAction that curr reads from.
+ *
+ */
+void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
+{
+ std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+ unsigned int i;
+ ASSERT(curr->is_read());
+
+ /* Iterate over all threads */
+ for (i = 0; i < thrd_lists->size(); i++) {
+ /* Iterate over actions in thread, starting from most recent */
+ action_list_t *list = &(*thrd_lists)[i];
+ action_list_t::reverse_iterator rit;
+ ModelAction *lastact = NULL;
+
+ /* Find last action that happens after curr that is either not curr or a rmw */
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *act = *rit;
+ if (curr->happens_before(act) && (curr != act || curr->is_rmw())) {
+ lastact = act;
+ } else
+ break;
+ }
+
+ /* Include at most one act per-thread that "happens before" curr */
+ if (lastact != NULL) {
+ if (lastact==curr) {
+ //Case 1: The resolved read is a RMW, and we need to make sure
+ //that the write portion of the RMW mod order after rf
+
+ mo_graph->addEdge(rf, lastact);
+ } else if (lastact->is_read()) {
+ //Case 2: The resolved read is a normal read and the next
+ //operation is a read, and we need to make sure the value read
+ //is mod ordered after rf
+
+ const ModelAction *postreadfrom = lastact->get_reads_from();
+ if (postreadfrom != NULL&&rf != postreadfrom)
+ mo_graph->addEdge(rf, postreadfrom);
+ } else {
+ //Case 3: The resolved read is a normal read and the next
+ //operation is a write, and we need to make sure that the
+ //write is mod ordered after rf
+ if (lastact!=rf)
+ mo_graph->addEdge(rf, lastact);
+ }
+ break;
+ }
+ }
+}
+
+/**
+ * Updates the mo_graph with the constraints imposed from the current write.
+ *
+ * Basic idea is the following: Go through each other thread and find
+ * the lastest action that happened before our write. Two cases:
+ *
+ * (1) The action is a write => that write must occur before
+ * the current write
+ *
+ * (2) The action is a read => the write that that action read from
+ * must occur before the current write.
+ *
+ * This method also handles two other issues:
+ *
+ * (I) Sequential Consistency: Making sure that if the current write is
+ * seq_cst, that it occurs after the previous seq_cst write.
+ *
+ * (II) Sending the write back to non-synchronizing reads.
+ *
+ * @param curr The current action. Must be a write.
+ * @return True if modification order edges were added; false otherwise
+ */
+bool ModelChecker::w_modification_order(ModelAction *curr)
+{
+ std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+ unsigned int i;
+ bool added = false;
+ ASSERT(curr->is_write());
+
+ if (curr->is_seqcst()) {
+ /* We have to at least see the last sequentially consistent write,
+ so we are initialized. */
+ ModelAction *last_seq_cst = get_last_seq_cst(curr);
+ if (last_seq_cst != NULL) {
+ mo_graph->addEdge(last_seq_cst, curr);
+ added = true;
+ }
+ }
+
+ /* Iterate over all threads */
+ for (i = 0; i < thrd_lists->size(); i++) {
+ /* Iterate over actions in thread, starting from most recent */
+ action_list_t *list = &(*thrd_lists)[i];
+ action_list_t::reverse_iterator rit;
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *act = *rit;
+ if (act == curr) {
+ /*
+ * If RMW, we already have all relevant edges,
+ * so just skip to next thread.
+ * If normal write, we need to look at earlier
+ * actions, so continue processing list.
+ */
+ if (curr->is_rmw())
+ break;
+ else
+ continue;
+ }
+
+ /*
+ * Include at most one act per-thread that "happens
+ * before" curr
+ */
+ if (act->happens_before(curr)) {
+ /*
+ * Note: if act is RMW, just add edge:
+ * act --mo--> curr
+ * The following edge should be handled elsewhere:
+ * readfrom(act) --mo--> act
+ */
+ if (act->is_write())
+ mo_graph->addEdge(act, curr);
+ else if (act->is_read() && act->get_reads_from() != NULL)
+ mo_graph->addEdge(act->get_reads_from(), curr);
+ added = true;
+ break;
+ } else if (act->is_read() && !act->is_synchronizing(curr) &&
+ !act->same_thread(curr)) {
+ /* We have an action that:
+ (1) did not happen before us
+ (2) is a read and we are a write
+ (3) cannot synchronize with us
+ (4) is in a different thread
+ =>
+ that read could potentially read from our write.
+ */
+ if (thin_air_constraint_may_allow(curr, act)) {
+ if (isfeasible() ||
+ (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && isfeasibleotherthanRMW())) {
+ struct PendingFutureValue pfv = {curr->get_value(),curr->get_seq_number()+params.maxfuturedelay,act};
+ futurevalues->push_back(pfv);
+ }
+ }
+ }
+ }
+ }
+
+ return added;
+}
+
+/** Arbitrary reads from the future are not allowed. Section 29.3
+ * part 9 places some constraints. This method checks one result of constraint
+ * constraint. Others require compiler support. */
+bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader) {
+ if (!writer->is_rmw())
+ return true;
+
+ if (!reader->is_rmw())
+ return true;
+
+ for (const ModelAction *search = writer->get_reads_from(); search != NULL; search = search->get_reads_from()) {
+ if (search == reader)
+ return false;
+ if (search->get_tid() == reader->get_tid() &&
+ search->happens_before(reader))
+ break;
+ }
+
+ 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
+ * release/acquire synchronization as an object of the "reads from" relation.
+ * Note that this can only provide release sequence support for RMW chains
+ * which do not read from the future, as those actions cannot be traced until
+ * their "promise" is fulfilled. Similarly, we may not even establish the
+ * presence of a release sequence with certainty, as some modification order
+ * constraints may be decided further in the future. Thus, this function
+ * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
+ * and a boolean representing certainty.
+ *
+ * @todo Finish lazy updating, when promises are fulfilled in the future
+ * @param rf The action that might be part of a release sequence. Must be a
+ * write.
+ * @param release_heads A pass-by-reference style return parameter. After
+ * execution of this function, release_heads will contain the heads of all the
+ * relevant release sequences, if any exists
+ * @return true, if the ModelChecker is certain that release_heads is complete;
+ * false otherwise