From e759b60e0b2dc31623ba3b03303a9d0d204fdd4c Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Sat, 5 May 2012 00:25:57 -0700 Subject: [PATCH] action: split ModelAction off into action.cc --- Makefile | 4 +-- action.cc | 100 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ model.cc | 96 --------------------------------------------------- 3 files changed, 102 insertions(+), 98 deletions(-) create mode 100644 action.cc diff --git a/Makefile b/Makefile index 3de1869..0f9bf00 100644 --- a/Makefile +++ b/Makefile @@ -8,8 +8,8 @@ LIB_SO=lib$(LIB_NAME).so USER_O=userprog.o USER_H=libthreads.h libatomic.h -MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc malloc.c threads.cc tree.cc librace.cc main.cc -MODEL_O=libthreads.o schedule.o libatomic.o model.o malloc.o threads.o tree.o librace.o main.o +MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc malloc.c threads.cc tree.cc librace.cc action.cc main.cc +MODEL_O=libthreads.o schedule.o libatomic.o model.o malloc.o threads.o tree.o librace.o action.o main.o MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h tree.h librace.h action.h CPPFLAGS=-Wall -g diff --git a/action.cc b/action.cc new file mode 100644 index 0000000..bd9e29f --- /dev/null +++ b/action.cc @@ -0,0 +1,100 @@ +#include + +#include "model.h" +#include "action.h" + +ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value) +{ + Thread *t = thread_current(); + ModelAction *act = this; + + act->type = type; + act->order = order; + act->location = loc; + act->tid = t->get_id(); + act->value = value; + act->seq_number = model->get_next_seq_num(); +} + +bool ModelAction::is_read() +{ + return type == ATOMIC_READ; +} + +bool ModelAction::is_write() +{ + return type == ATOMIC_WRITE; +} + +bool ModelAction::is_acquire() +{ + switch (order) { + case memory_order_acquire: + case memory_order_acq_rel: + case memory_order_seq_cst: + return true; + default: + return false; + } +} + +bool ModelAction::is_release() +{ + switch (order) { + case memory_order_release: + case memory_order_acq_rel: + case memory_order_seq_cst: + return true; + default: + return false; + } +} + +bool ModelAction::same_var(ModelAction *act) +{ + return location == act->location; +} + +bool ModelAction::same_thread(ModelAction *act) +{ + return tid == act->tid; +} + +bool ModelAction::is_dependent(ModelAction *act) +{ + if (!is_read() && !is_write()) + return false; + if (!act->is_read() && !act->is_write()) + return false; + if (same_var(act) && !same_thread(act) && + (is_write() || act->is_write())) + return true; + return false; +} + +void ModelAction::print(void) +{ + const char *type_str; + switch (this->type) { + case THREAD_CREATE: + type_str = "thread create"; + break; + case THREAD_YIELD: + type_str = "thread yield"; + break; + case THREAD_JOIN: + type_str = "thread join"; + break; + case ATOMIC_READ: + type_str = "atomic read"; + break; + case ATOMIC_WRITE: + type_str = "atomic write"; + break; + default: + type_str = "unknown type"; + } + + printf("(%4d) Thread: %d\tAction: %s\tMO: %d\tLoc: %14p\tValue: %d\n", + seq_number, id_to_int(tid), type_str, order, location, value); +} diff --git a/model.cc b/model.cc index 2c74047..643ad95 100644 --- a/model.cc +++ b/model.cc @@ -300,99 +300,3 @@ int ModelChecker::switch_to_master(ModelAction *act) old->set_state(THREAD_READY); return Thread::swap(old, get_system_context()); } - -ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value) -{ - Thread *t = thread_current(); - ModelAction *act = this; - - act->type = type; - act->order = order; - act->location = loc; - act->tid = t->get_id(); - act->value = value; - act->seq_number = model->get_next_seq_num(); -} - -bool ModelAction::is_read() -{ - return type == ATOMIC_READ; -} - -bool ModelAction::is_write() -{ - return type == ATOMIC_WRITE; -} - -bool ModelAction::is_acquire() -{ - switch (order) { - case memory_order_acquire: - case memory_order_acq_rel: - case memory_order_seq_cst: - return true; - default: - return false; - } -} - -bool ModelAction::is_release() -{ - switch (order) { - case memory_order_release: - case memory_order_acq_rel: - case memory_order_seq_cst: - return true; - default: - return false; - } -} - -bool ModelAction::same_var(ModelAction *act) -{ - return location == act->location; -} - -bool ModelAction::same_thread(ModelAction *act) -{ - return tid == act->tid; -} - -bool ModelAction::is_dependent(ModelAction *act) -{ - if (!is_read() && !is_write()) - return false; - if (!act->is_read() && !act->is_write()) - return false; - if (same_var(act) && !same_thread(act) && - (is_write() || act->is_write())) - return true; - return false; -} - -void ModelAction::print(void) -{ - const char *type_str; - switch (this->type) { - case THREAD_CREATE: - type_str = "thread create"; - break; - case THREAD_YIELD: - type_str = "thread yield"; - break; - case THREAD_JOIN: - type_str = "thread join"; - break; - case ATOMIC_READ: - type_str = "atomic read"; - break; - case ATOMIC_WRITE: - type_str = "atomic write"; - break; - default: - type_str = "unknown type"; - } - - printf("(%4d) Thread: %d\tAction: %s\tMO: %d\tLoc: %14p\tValue: %d\n", - seq_number, id_to_int(tid), type_str, order, location, value); -} -- 2.34.1