projects
/
c11tester.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
7f915e4
)
Improve documentation
author
Brian Demsky
<bdemsky@uci.edu>
Tue, 31 Dec 2019 01:56:30 +0000
(17:56 -0800)
committer
Brian Demsky
<bdemsky@uci.edu>
Tue, 31 Dec 2019 01:56:30 +0000
(17:56 -0800)
execution.cc
patch
|
blob
|
history
diff --git
a/execution.cc
b/execution.cc
index fb16def8748dac4c4c9d1825268d38004d3ae7a8..b0a12e584c28e6a6ab8c6f3596190eddbb1d08d0 100644
(file)
--- a/
execution.cc
+++ b/
execution.cc
@@
-1660,6
+1660,8
@@
Thread * ModelExecution::take_step(ModelAction *curr)
return action_select_next_thread(curr);
}
return action_select_next_thread(curr);
}
+/** This method removes references to an Action before we delete it. */
+
void ModelExecution::removeAction(ModelAction *act) {
{
sllnode<ModelAction *> * listref = act->getTraceRef();
void ModelExecution::removeAction(ModelAction *act) {
{
sllnode<ModelAction *> * listref = act->getTraceRef();
@@
-1697,12
+1699,13
@@
void ModelExecution::removeAction(ModelAction *act) {
obj_last_sc_map.remove(act->get_location());
}
obj_last_sc_map.remove(act->get_location());
}
-
//Remove from Cyclegraph
mo_graph->freeAction(act);
}
}
//Remove from Cyclegraph
mo_graph->freeAction(act);
}
}
+/** Computes clock vector that all running threads have already synchronized to. */
+
ClockVector * ModelExecution::computeMinimalCV() {
ClockVector *cvmin = NULL;
//Thread 0 isn't a real thread, so skip it..
ClockVector * ModelExecution::computeMinimalCV() {
ClockVector *cvmin = NULL;
//Thread 0 isn't a real thread, so skip it..
@@
-1720,8
+1723,10
@@
ClockVector * ModelExecution::computeMinimalCV() {
return cvmin;
}
return cvmin;
}
+
+/** Sometimes we need to remove an action that is the most recent in the thread. This happens if it is mo before action in other threads. In that case we need to create a replacement latest ModelAction */
+
void ModelExecution::fixupLastAct(ModelAction *act) {
void ModelExecution::fixupLastAct(ModelAction *act) {
-//Create a standin ModelAction
ModelAction *newact = new ModelAction(ATOMIC_NOP, std::memory_order_seq_cst, get_thread(act->get_tid()));
newact->set_seq_number(get_next_seq_num());
newact->create_cv(act);
ModelAction *newact = new ModelAction(ATOMIC_NOP, std::memory_order_seq_cst, get_thread(act->get_tid()));
newact->set_seq_number(get_next_seq_num());
newact->create_cv(act);
@@
-1729,6
+1734,8
@@
void ModelExecution::fixupLastAct(ModelAction *act) {
add_action_to_lists(newact, false);
}
add_action_to_lists(newact, false);
}
+/** Compute which actions to free. */
+
void ModelExecution::collectActions() {
//Compute minimal clock vector for all live threads
ClockVector *cvmin = computeMinimalCV();
void ModelExecution::collectActions() {
//Compute minimal clock vector for all live threads
ClockVector *cvmin = computeMinimalCV();
@@
-1750,6
+1757,8
@@
void ModelExecution::collectActions() {
thread_id_t act_tid = act->get_tid();
modelclock_t tid_clock = cvmin->getClock(act_tid);
thread_id_t act_tid = act->get_tid();
modelclock_t tid_clock = cvmin->getClock(act_tid);
+
+ //Free if it is invisible or we have set a flag to remove visible actions.
if (actseq <= tid_clock || params->removevisible) {
ModelAction * write;
if (act->is_write()) {
if (actseq <= tid_clock || params->removevisible) {
ModelAction * write;
if (act->is_write()) {
@@
-1778,6
+1787,9
@@
void ModelExecution::collectActions() {
}
}
}
}
}
}
+
+ //We may need to remove read actions in the window we don't delete to preserve correctness.
+
for (sllnode<ModelAction*> * it2 = action_trace.end();it2 != it;) {
ModelAction *act = it2->getVal();
//Do iteration early in case we delete the act
for (sllnode<ModelAction*> * it2 = action_trace.end();it2 != it;) {
ModelAction *act = it2->getVal();
//Do iteration early in case we delete the act
@@
-1792,7
+1804,7
@@
void ModelExecution::collectActions() {
if (act->is_read()) {
if (act->get_reads_from()->is_free()) {
if (act->is_rmw()) {
if (act->is_read()) {
if (act->get_reads_from()->is_free()) {
if (act->is_rmw()) {
- //
weaken to
write
+ //
Weaken a RMW from a freed store to a
write
act->set_type(ATOMIC_WRITE);
} else {
removeAction(act);
act->set_type(ATOMIC_WRITE);
} else {
removeAction(act);
@@
-1804,6
+1816,8
@@
void ModelExecution::collectActions() {
}
}
}
}
}
}
+ //If we don't delete the action, we should remove references to release fences
+
const ModelAction *rel_fence =act->get_last_fence_release();
if (rel_fence != NULL) {
modelclock_t relfenceseq = rel_fence->get_seq_number();
const ModelAction *rel_fence =act->get_last_fence_release();
if (rel_fence != NULL) {
modelclock_t relfenceseq = rel_fence->get_seq_number();
@@
-1814,6
+1828,7
@@
void ModelExecution::collectActions() {
act->set_last_fence_release(NULL);
}
}
act->set_last_fence_release(NULL);
}
}
+ //Now we are in the window of old actions that we remove if possible
for (;it != NULL;) {
ModelAction *act = it->getVal();
//Do iteration early since we may delete node...
for (;it != NULL;) {
ModelAction *act = it->getVal();
//Do iteration early since we may delete node...
@@
-1892,6
+1907,8
@@
void ModelExecution::collectActions() {
delete act;
continue;
}
delete act;
continue;
}
+
+ //If we don't delete the action, we should remove references to release fences
const ModelAction *rel_fence =act->get_last_fence_release();
if (rel_fence != NULL) {
modelclock_t relfenceseq = rel_fence->get_seq_number();
const ModelAction *rel_fence =act->get_last_fence_release();
if (rel_fence != NULL) {
modelclock_t relfenceseq = rel_fence->get_seq_number();
@@
-1909,8
+1926,6
@@
void ModelExecution::collectActions() {
delete queue;
}
delete queue;
}
-
-
Fuzzer * ModelExecution::getFuzzer() {
return fuzzer;
}
Fuzzer * ModelExecution::getFuzzer() {
return fuzzer;
}