summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
2cd14a2)
(1) need to compute promises for rmw nodes...they could satisfy them
(2) don't call rmwedge if you don't know where you are reading from yet
(3) miscopied commit from big merge (already_added -> !already_added)
(4) avoid adding rmw edges back to itself
(5) probably worth adding a check that the execution isfeasible before sending future values
(6) resolve promises should add rmwedges when appropriate
(7) fix seq_cst to mask earlier writes..
second_part_of_rmw = true;
delete curr;
curr = tmp;
second_part_of_rmw = true;
delete curr;
curr = tmp;
+ compute_promises(curr);
} else {
ModelAction *tmp = node_stack->explore_action(curr);
if (tmp) {
} else {
ModelAction *tmp = node_stack->explore_action(curr);
if (tmp) {
int tid = id_to_int(act->get_tid());
ModelAction *lastread = get_last_action(tid);
lastread->process_rmw(act);
int tid = id_to_int(act->get_tid());
ModelAction *lastread = get_last_action(tid);
lastread->process_rmw(act);
+ if (act->is_rmw() && lastread->get_reads_from()!=NULL) {
mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
+ mo_graph->commitChanges();
+ }
action_list_t::reverse_iterator rit = list->rbegin();
/* Skip past curr */
action_list_t::reverse_iterator rit = list->rbegin();
/* Skip past curr */
for (; (*rit) != curr; rit++)
;
/* go past curr now */
for (; (*rit) != curr; rit++)
;
/* go past curr now */
* The following edge should be handled elsewhere:
* readfrom(act) --mo--> act
*/
* 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)
+ if (act->is_write()) {
+ //RMW shouldn't have an edge to themselves
+ if (act!=curr)
+ 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;
mo_graph->addEdge(act->get_reads_from(), curr);
added = true;
break;
=>
that read could potentially read from our write.
*/
=>
that read could potentially read from our write.
*/
- if (act->get_node()->add_future_value(curr->get_value()) &&
+ if (isfeasible() && act->get_node()->add_future_value(curr->get_value()) &&
(!priv->next_backtrack || *act > *priv->next_backtrack))
priv->next_backtrack = act;
}
(!priv->next_backtrack || *act > *priv->next_backtrack))
priv->next_backtrack = act;
}
if (write->get_node()->get_promise(i)) {
ModelAction *read = promise->get_action();
read->read_from(write);
if (write->get_node()->get_promise(i)) {
ModelAction *read = promise->get_action();
read->read_from(write);
+ if (read->is_rmw()) {
+ mo_graph->addRMWEdge(write, read);
+ }
r_modification_order(read, write);
post_r_modification_order(read, write);
promises->erase(promises->begin() + promise_index);
r_modification_order(read, write);
post_r_modification_order(read, write);
promises->erase(promises->begin() + promise_index);
continue;
/* Don't consider more than one seq_cst write if we are a seq_cst read. */
continue;
/* Don't consider more than one seq_cst write if we are a seq_cst read. */
- if (!act->is_seqcst() || !curr->is_seqcst() || act == last_seq_cst) {
+ if (!curr->is_seqcst()|| (!act->is_seqcst() && (last_seq_cst==NULL||!act->happens_before(last_seq_cst))) || act == last_seq_cst) {
DEBUG("Adding action to may_read_from:\n");
if (DBG_ENABLED()) {
act->print();
DEBUG("Adding action to may_read_from:\n");
if (DBG_ENABLED()) {
act->print();