2) Change is_dependent to is_synchronizing and make it capture actual synchronizing behavior...
3) Add more support for RMW operations.
12 files changed:
return type == ATOMIC_WRITE;
}
return type == ATOMIC_WRITE;
}
+bool ModelAction::is_rmw()
+{
+ return type == ATOMIC_RMW;
+}
+
bool ModelAction::is_acquire()
{
switch (order) {
bool ModelAction::is_acquire()
{
switch (order) {
+bool ModelAction::is_seqcst()
+{
+ return order==memory_order_seq_cst;
+}
+
bool ModelAction::same_var(ModelAction *act)
{
return location == act->location;
bool ModelAction::same_var(ModelAction *act)
{
return location == act->location;
return tid == act->tid;
}
return tid == act->tid;
}
-bool ModelAction::is_dependent(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.
+ *
+ * @param act is the action to consider exploring a reordering.
+ * @return tells whether we have to explore a reordering.
+ */
+
+bool ModelAction::is_synchronizing(ModelAction *act)
- if (!is_read() && !is_write())
+ //Same thread can't be reordered
+ if (same_thread(act))
- if (!act->is_read() && !act->is_write())
+
+ // Different locations commute
+ if (!same_var(act))
- if (same_var(act) && !same_thread(act) &&
- (is_write() || act->is_write()))
+
+ // 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())
+ return true;
+
+ // Explore synchronizing read/write pairs
+ if (is_read() && is_acquire() && act->is_write() && act->is_release())
+ if (is_write() && is_release() && act->is_read() && act->is_acquire())
+ return true;
+
+ // Otherwise handle by reads_from relation
+/** @file action.h
+ * @brief Models actions taken by threads.
+ */
+
#ifndef __ACTION_H__
#define __ACTION_H__
#ifndef __ACTION_H__
#define __ACTION_H__
bool is_read();
bool is_write();
bool is_read();
bool is_write();
bool is_acquire();
bool is_release();
bool is_acquire();
bool is_release();
bool same_var(ModelAction *act);
bool same_thread(ModelAction *act);
bool same_var(ModelAction *act);
bool same_thread(ModelAction *act);
- bool is_dependent(ModelAction *act);
+ bool is_synchronizing(ModelAction *act);
void create_cv(ModelAction *parent = NULL);
void read_from(ModelAction *act);
void create_cv(ModelAction *parent = NULL);
void read_from(ModelAction *act);
+/** @file clockvector.h
+ * @brief Implements a clock vector.
+ */
+
#ifndef __CLOCKVECTOR_H__
#define __CLOCKVECTOR_H__
#ifndef __CLOCKVECTOR_H__
#define __CLOCKVECTOR_H__
+/** @file common.h
+ * @brief General purpose macros.
+ */
+
#ifndef __COMMON_H__
#define __COMMON_H__
#ifndef __COMMON_H__
#define __COMMON_H__
+/** @file libatomic.h
+ * @brief Basic atomic operations to be exposed to user program.
+ */
+
#ifndef __LIBATOMIC_H__
#define __LIBATOMIC_H__
#ifndef __LIBATOMIC_H__
#define __LIBATOMIC_H__
+/** @file librace.h
+ * @brief Interface to check normal memory operations for data races.
+ */
+
#ifndef __LIBRACE_H__
#define __LIBRACE_H__
#ifndef __LIBRACE_H__
#define __LIBRACE_H__
+/** @file libthreads.h
+ * @brief Basic Thread Library Functionality.
+ */
+
#ifndef __LIBTHREADS_H__
#define __LIBTHREADS_H__
#ifndef __LIBTHREADS_H__
#define __LIBTHREADS_H__
action_list_t::reverse_iterator rit;
for (rit = action_trace->rbegin(); rit != action_trace->rend(); rit++) {
ModelAction *prev = *rit;
action_list_t::reverse_iterator rit;
for (rit = action_trace->rbegin(); rit != action_trace->rend(); rit++) {
ModelAction *prev = *rit;
- if (act->is_dependent(prev))
+ if (act->is_synchronizing(prev))
return prev;
}
return NULL;
return prev;
}
return NULL;
+/** @file model.h
+ * @brief Core model checker.
+ */
+
#ifndef __MODEL_H__
#define __MODEL_H__
#ifndef __MODEL_H__
#define __MODEL_H__
+/** @file nodestack.h
+ * @brief Stack of operations for use in backtracking.
+*/
+
#ifndef __NODESTACK_H__
#define __NODESTACK_H__
#ifndef __NODESTACK_H__
#define __NODESTACK_H__
+/** @file schedule.h
+ * @brief Thread scheduler.
+ */
+
#ifndef __SCHEDULE_H__
#define __SCHEDULE_H__
#ifndef __SCHEDULE_H__
#define __SCHEDULE_H__
+/** @file threads.h
+ * @brief Model Checker Thread class.
+ */
+
#ifndef __THREADS_H__
#define __THREADS_H__
#ifndef __THREADS_H__
#define __THREADS_H__