projects
/
c11tester.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
model: wire up rest of release seq. resolution backtracking
[c11tester.git]
/
action.cc
diff --git
a/action.cc
b/action.cc
index c6504cd388d0f44f6ec72c038d36996b79fad882..c12165b0322a2beb4ff9c25fd33be05f1f7630f2 100644
(file)
--- a/
action.cc
+++ b/
action.cc
@@
-50,6
+50,11
@@
void ModelAction::set_seq_number(modelclock_t num)
seq_number = num;
}
seq_number = num;
}
+bool ModelAction::is_relseq_fixup() const
+{
+ return type == MODEL_FIXUP_RELSEQ;
+}
+
bool ModelAction::is_mutex_op() const
{
return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK;
bool ModelAction::is_mutex_op() const
{
return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK;
@@
-184,7
+189,7
@@
void ModelAction::process_rmw(ModelAction * act) {
* @param act is the action to consider exploring a reordering.
* @return tells whether we have to explore a reordering.
*/
* @param act is the action to consider exploring a reordering.
* @return tells whether we have to explore a reordering.
*/
-bool ModelAction::
is_synchronizing
(const ModelAction *act) const
+bool ModelAction::
could_synchronize_with
(const ModelAction *act) const
{
//Same thread can't be reordered
if (same_thread(act))
{
//Same thread can't be reordered
if (same_thread(act))
@@
-196,14
+201,12
@@
bool ModelAction::is_synchronizing(const ModelAction *act) const
// Explore interleavings of seqcst writes to guarantee total order
// of seq_cst operations that don't commute
// Explore interleavings of seqcst writes to guarantee total order
// of seq_cst operations that don't commute
- if (
is_write() && is_seqcst() && act->is_write
() && act->is_seqcst())
+ if (
(is_write() || act->is_write()) && is_seqcst
() && act->is_seqcst())
return true;
// Explore synchronizing read/write pairs
if (is_read() && is_acquire() && act->is_write() && act->is_release())
return true;
return true;
// Explore synchronizing read/write pairs
if (is_read() && is_acquire() && act->is_write() && act->is_release())
return true;
- if (is_write() && is_release() && act->is_read() && act->is_acquire())
- return true;
// Otherwise handle by reads_from relation
return false;
// Otherwise handle by reads_from relation
return false;
@@
-307,6
+310,9
@@
void ModelAction::print() const
{
const char *type_str, *mo_str;
switch (this->type) {
{
const char *type_str, *mo_str;
switch (this->type) {
+ case MODEL_FIXUP_RELSEQ:
+ type_str = "relseq fixup";
+ break;
case THREAD_CREATE:
type_str = "thread create";
break;
case THREAD_CREATE:
type_str = "thread create";
break;