From: Brian Demsky <bdemsky@uci.edu>
Date: Fri, 20 Jul 2012 00:15:12 +0000 (-0700)
Subject: switch rest over to model checker...  might work now
X-Git-Tag: pldi2013~327
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=5a8ba5648b3b56f963bd6b165791631c4c5ff6be

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

diff --git a/include/impatomic.c b/include/impatomic.c
index b5de5c7..05de31c 100644
--- 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__;
-}
-
diff --git a/include/impatomic.h b/include/impatomic.h
index 466773d..472e663 100644
--- a/include/impatomic.h
+++ b/include/impatomic.h
@@ -51,9 +51,6 @@ extern void __atomic_flag_wait__
 ( volatile atomic_flag* );
 extern void __atomic_flag_wait_explicit__
 ( volatile atomic_flag*, memory_order );
-extern volatile atomic_flag* __atomic_flag_for_address__
-( const volatile void* __z__ )
-__attribute__((const));
 
 #ifdef __cplusplus
 }
@@ -123,7 +120,14 @@ inline void atomic_flag::fence( memory_order __x__ ) const volatile
 #define _ATOMIC_FENCE_( __a__, __x__ )					\
 	({ ASSERT(0);})
 
-#define ATOMIC_INTEGRAL_LOCK_FREE 1
+#define ATOMIC_CHAR_LOCK_FREE 1
+#define ATOMIC_CHAR16_T_LOCK_FREE 1
+#define ATOMIC_CHAR32_T_LOCK_FREE 1
+#define ATOMIC_WCHAR_T_LOCK_FREE 1
+#define ATOMIC_SHORT_LOCK_FREE 1
+#define ATOMIC_INT_LOCK_FREE 1
+#define ATOMIC_LONG_LOCK_FREE 1
+#define ATOMIC_LLONG_LOCK_FREE 1
 #define ATOMIC_ADDRESS_LOCK_FREE 1
 
 typedef struct atomic_bool