Index: kernel/arch/abs32le/include/atomic.h
===================================================================
--- kernel/arch/abs32le/include/atomic.h	(revision 09a0bd4a4ab5a70550f327984b135164b05aa58d)
+++ kernel/arch/abs32le/include/atomic.h	(revision 33c4f72505a3c4729684b213f04c3c7feb9c842b)
@@ -42,4 +42,6 @@
 
 ATOMIC static inline void atomic_inc(atomic_t *val)
+    WRITES(&val->count)
+    REQUIRES_EXTENT_MUTABLE(val)
     REQUIRES(val->count < ATOMIC_COUNT_MAX)
 {
@@ -51,4 +53,6 @@
 
 ATOMIC static inline void atomic_dec(atomic_t *val)
+    WRITES(&val->count)
+    REQUIRES_EXTENT_MUTABLE(val)
     REQUIRES(val->count > ATOMIC_COUNT_MIN)
 {
@@ -60,4 +64,6 @@
 
 ATOMIC static inline atomic_count_t atomic_postinc(atomic_t *val)
+    WRITES(&val->count)
+    REQUIRES_EXTENT_MUTABLE(val)
     REQUIRES(val->count < ATOMIC_COUNT_MAX)
 {
@@ -73,4 +79,6 @@
 
 ATOMIC static inline atomic_count_t atomic_postdec(atomic_t *val)
+    WRITES(&val->count)
+    REQUIRES_EXTENT_MUTABLE(val)
     REQUIRES(val->count > ATOMIC_COUNT_MIN)
 {
@@ -89,4 +97,6 @@
 
 ATOMIC static inline atomic_count_t test_and_set(atomic_t *val)
+    WRITES(&val->count)
+    REQUIRES_EXTENT_MUTABLE(val)
 {
 	/* On real hardware the retrieving of the original
@@ -99,18 +109,10 @@
 }
 
-ATOMIC static inline atomic_count_t arch_atomic_get(atomic_t *val)
-{
-	/* This function is not needed on real hardware, it just
-	   duplicates the functionality of atomic_get(). It is
-	   defined here because atomic_get() is an inline function
-	   declared in a header file which we are included in. */
-	
-	return val->count;
-}
-
 static inline void atomic_lock_arch(atomic_t *val)
+    WRITES(&val->count)
+    REQUIRES_EXTENT_MUTABLE(val)
 {
 	do {
-		while (arch_atomic_get(val));
+		while (val->count);
 	} while (test_and_set(val));
 }