fix CAS operation

diff --git a/cmodelint.cc b/cmodelint.cc
index 9e4923b9e61f07bf178b2e5e3b872247dd713d1d..348051a0f7f13fb736baf14f8a24c81bcfdbb4f9 100644 (file)
--- a/cmodelint.cc
+++ b/cmodelint.cc
@@ -59,7 +59,7 @@ void model_fence_action(memory_order ord) {
 }
 
 /* ---  helper functions --- */
-uint64_t model_rmwrcas_action_helper(void *obj, int atomic_index, const char *position) {
+uint64_t model_rmwrcas_action_helper(void *obj, int atomic_index, uint64_t oldval, int size, const char *position) {
        return model->switch_to_master(
                new ModelAction(ATOMIC_RMWRCAS, position, orders[atomic_index], obj)
                );
@@ -252,7 +252,7 @@ uint64_t cds_atomic_fetch_xor64(void* addr, uint64_t val, int atomic_index, cons
        ({                                                                                              \
                uint ## size ## _t _desired = desired;                                                            \
                uint ## size ## _t _expected = expected;                                                          \
-               uint ## size ## _t _old = model_rmwrcas_action_helper(addr, atomic_index, position);                           \
+               uint ## size ## _t _old = model_rmwrcas_action_helper(addr, atomic_index, _expected, sizeof(_expected), position); \
                if (_old == _expected) {                                                                    \
                        model_rmw_action_helper(addr, (uint64_t) _desired, atomic_index, position); return _expected; }      \
                else {                                                                                        \

diff --git a/execution.cc b/execution.cc
index 7b09871e4b5a73c335e04393c77b1667841ba04c..d75499f1349a4e24c69a1c01c90aa8bb599240d5 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -339,6 +339,8 @@ bool ModelExecution::process_mutex(ModelAction *curr)
        }
        case ATOMIC_WAIT:
        case ATOMIC_UNLOCK: {
+               //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME AS NORMAL WAITS...THINK ABOUT PROBABILITIES THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY FAILS AND IN THE CASE IT DOESN'T...  TIMED WAITS MUST EVENMTUALLY RELEASE...
+
                /* wake up the other threads */
                for (unsigned int i = 0;i < get_num_threads();i++) {
                        Thread *t = get_thread(int_to_id(i));

diff --git a/include/cmodelint.h b/include/cmodelint.h
index d6cd8f9bd8b104206f2efb3b976b270e28c3d713..8530827cfe39b5cf673efa3e047a8f987f7642a1 100644 (file)
--- a/include/cmodelint.h
+++ b/include/cmodelint.h
@@ -22,7 +22,7 @@ void model_rmwc_action(void *obj, memory_order ord);
 void model_fence_action(memory_order ord);
 
 uint64_t model_rmwr_action_helper(void *obj, int atomic_index, const char *position);
-uint64_t model_rmwrcas_action_helper(void *obj, int atomic_index, const char *position);
+  uint64_t model_rmwrcas_action_helper(void *obj, int atomic_index, uint64_t oval, int size, const char *position);
 void model_rmw_action_helper(void *obj, uint64_t val, int atomic_index, const char *position);
 void model_rmwc_action_helper(void *obj, int atomic_index, const char *position);
 // void model_fence_action_helper(int atomic_index);