switch rest over to model checker... might work now

[model-checker.git] / include / impatomic.c

diff --git a/include/impatomic.c b/include/impatomic.c
index b5de5c7384ba4a210fc61eaa4c712d464341f5d4..05de31c7a1378760753216f7f79772bf5c518dc5 100644 (file)
--- a/include/impatomic.c
+++ b/include/impatomic.c
@@ -1,26 +1,14 @@
-
 #include <stdint.h>
 #include "impatomic.h"
 
-
-#if defined(__GNUC__)
-#if __GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ > 0)
-#define USE_SYNC
-#endif
-#endif
-
 bool atomic_flag_test_and_set_explicit
 ( volatile atomic_flag* __a__, memory_order __x__ )
 {
-#ifdef USE_SYNC
-    if ( __x__ >= memory_order_acq_rel )
-        __sync_synchronize();
-    return __sync_lock_test_and_set( &(__a__->__f__), 1 );
-#else
-    bool result = __a__->__f__;
-    __a__->__f__ = true;
-    return result;
-#endif
+       bool * __p__ = &((__a__)->__f__);
+       model->switch_to_master(new ModelAction(ATOMIC_READ, __x__, __p__));
+       bool result = (void *) thread_current()->get_return_value();
+       model->switch_to_master(new ModelAction(ATOMIC_RMW, __x__, __p__, true));
+       return result;
 }
 
 bool atomic_flag_test_and_set( volatile atomic_flag* __a__ )
@@ -29,13 +17,8 @@ bool atomic_flag_test_and_set( volatile atomic_flag* __a__ )
 void atomic_flag_clear_explicit
 ( volatile atomic_flag* __a__, memory_order __x__ )
 {
-#ifdef USE_SYNC
-    __sync_lock_release( &(__a__->__f__) );
-    if ( __x__ >= memory_order_acq_rel )
-        __sync_synchronize();
-#else
-    __a__->__f__ = false;
-#endif
+       bool * __p__ = &((__a__)->__f__);
+       model->switch_to_master(new ModelAction(ATOMIC_WRITE, __x__, __p__, false));
 }
 
 void atomic_flag_clear( volatile atomic_flag* __a__ )
@@ -43,9 +26,7 @@ void atomic_flag_clear( volatile atomic_flag* __a__ )
 
 void atomic_flag_fence( const volatile atomic_flag* __a__, memory_order __x__ )
 {
-#ifdef USE_SYNC
-    __sync_synchronize();
-#endif
+       ASSERT(0);
 }
 
 void __atomic_flag_wait__( volatile atomic_flag* __a__ )
@@ -54,25 +35,3 @@ void __atomic_flag_wait__( volatile atomic_flag* __a__ )
 void __atomic_flag_wait_explicit__( volatile atomic_flag* __a__,
                                     memory_order __x__ )
 { while ( atomic_flag_test_and_set_explicit( __a__, __x__ ) ); }
-
-#define LOGSIZE 4
-
-static atomic_flag volatile __atomic_flag_anon_table__[ 1 << LOGSIZE ] =
-{
-    ATOMIC_FLAG_INIT, ATOMIC_FLAG_INIT, ATOMIC_FLAG_INIT, ATOMIC_FLAG_INIT,
-    ATOMIC_FLAG_INIT, ATOMIC_FLAG_INIT, ATOMIC_FLAG_INIT, ATOMIC_FLAG_INIT,
-    ATOMIC_FLAG_INIT, ATOMIC_FLAG_INIT, ATOMIC_FLAG_INIT, ATOMIC_FLAG_INIT,
-    ATOMIC_FLAG_INIT, ATOMIC_FLAG_INIT, ATOMIC_FLAG_INIT, ATOMIC_FLAG_INIT,
-};
-
-volatile atomic_flag* __atomic_flag_for_address__( const volatile void* __z__ )
-{
-    uintptr_t __u__ = (uintptr_t)__z__;
-    __u__ += (__u__ >> 2) + (__u__ << 4);
-    __u__ += (__u__ >> 7) + (__u__ << 5);
-    __u__ += (__u__ >> 17) + (__u__ << 13);
-    if ( sizeof(uintptr_t) > 4 ) __u__ += (__u__ >> 31);
-    __u__ &= ~((~(uintptr_t)0) << LOGSIZE);
-    return __atomic_flag_anon_table__ + __u__;
-}
-