#include <stdio.h>
#define __STDC_FORMAT_MACROS
#include <inttypes.h>
+#include <stdlib.h>
#include "model.h"
#include "action.h"
#define ACTION_INITIAL_CLOCK 0
-/** A special value to represent a successful trylock */
+/** @brief A special value to represent a successful trylock */
#define VALUE_TRYSUCCESS 1
-/** A special value to represent a failed trylock */
+/** @brief A special value to represent a failed trylock */
#define VALUE_TRYFAILED 0
/**
return NULL;
}
-/** This method changes an existing read part of an RMW action into either:
- * (1) a full RMW action in case of the completed write or
- * (2) a READ action in case a failed action.
+/**
+ * @brief Convert the read portion of an RMW
+ *
+ * Changes an existing read part of an RMW action into either:
+ * -# a full RMW action in case of the completed write or
+ * -# a READ action in case a failed action.
+ *
* @todo If the memory_order changes, we may potentially need to update our
* clock vector.
+ *
+ * @param act The second half of the RMW (either RMWC or RMW)
*/
void ModelAction::process_rmw(ModelAction *act)
{
}
}
-/** The is_synchronizing method should only explore interleavings if:
- * (1) the operations are seq_cst and don't commute or
- * (2) the reordering may establish or break a synchronization relation.
- * Other memory operations will be dealt with by using the reads_from
- * relation.
+/**
+ * @brief Check if this action should be backtracked with another, due to
+ * potential synchronization
+ *
+ * The is_synchronizing method should only explore interleavings if:
+ * -# the operations are seq_cst and don't commute or
+ * -# the reordering may establish or break a synchronization relation.
+ *
+ * Other memory operations will be dealt with by using the reads_from relation.
*
- * @param act is the action to consider exploring a reordering.
- * @return tells whether we have to explore a reordering.
+ * @param act The action to consider exploring a reordering
+ * @return True, if we have to explore a reordering; otherwise false
*/
bool ModelAction::could_synchronize_with(const ModelAction *act) const
{
*/
bool ModelAction::synchronize_with(const ModelAction *act)
{
- if (*this < *act && type != THREAD_JOIN && type != ATOMIC_LOCK)
+ if (*this < *act)
return false;
- model->check_promises(act->get_tid(), cv, act->cv);
cv->merge(act->cv);
return true;
}
if (reads_from)
model_print(" Rf: %-3d", reads_from->get_seq_number());
else if (reads_from_promise) {
- int idx = model->get_promise_number(reads_from_promise);
+ int idx = reads_from_promise->get_index();
if (idx >= 0)
model_print(" Rf: P%-2d", idx);
else
if (reads_from)
hash ^= reads_from->get_seq_number();
else if (reads_from_promise)
- hash ^= model->get_promise_number(reads_from_promise);
+ hash ^= reads_from_promise->get_index();
hash ^= get_reads_from_value();
}
return hash;