Index: kernel/arch/abs32le/include/atomic.h
===================================================================
--- kernel/arch/abs32le/include/atomic.h	(revision ccb426c40c1bb63880c8f1dd8edb16e9b19286f9)
+++ kernel/arch/abs32le/include/atomic.h	(revision 09a0bd4a4ab5a70550f327984b135164b05aa58d)
@@ -39,6 +39,9 @@
 #include <arch/barrier.h>
 #include <preemption.h>
+#include <verify.h>
 
-static inline void atomic_inc(atomic_t *val) {
+ATOMIC static inline void atomic_inc(atomic_t *val)
+    REQUIRES(val->count < ATOMIC_COUNT_MAX)
+{
 	/* On real hardware the increment has to be done
 	   as an atomic action. */
@@ -47,12 +50,15 @@
 }
 
-static inline void atomic_dec(atomic_t *val) {
+ATOMIC static inline void atomic_dec(atomic_t *val)
+    REQUIRES(val->count > ATOMIC_COUNT_MIN)
+{
 	/* On real hardware the decrement has to be done
 	   as an atomic action. */
 	
-	val->count++;
+	val->count--;
 }
 
-static inline atomic_count_t atomic_postinc(atomic_t *val)
+ATOMIC static inline atomic_count_t atomic_postinc(atomic_t *val)
+    REQUIRES(val->count < ATOMIC_COUNT_MAX)
 {
 	/* On real hardware both the storing of the previous
@@ -66,5 +72,6 @@
 }
 
-static inline atomic_count_t atomic_postdec(atomic_t *val)
+ATOMIC static inline atomic_count_t atomic_postdec(atomic_t *val)
+    REQUIRES(val->count > ATOMIC_COUNT_MIN)
 {
 	/* On real hardware both the storing of the previous
@@ -81,6 +88,10 @@
 #define atomic_predec(val)  (atomic_postdec(val) - 1)
 
-static inline atomic_count_t test_and_set(atomic_t *val)
+ATOMIC static inline atomic_count_t test_and_set(atomic_t *val)
 {
+	/* On real hardware the retrieving of the original
+	   value and storing 1 have to be done as a single
+	   atomic action. */
+	
 	atomic_count_t prev = val->count;
 	val->count = 1;
@@ -88,8 +99,18 @@
 }
 
+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)
 {
 	do {
-		while (val->count);
+		while (arch_atomic_get(val));
 	} while (test_and_set(val));
 }
Index: kernel/arch/abs32le/include/types.h
===================================================================
--- kernel/arch/abs32le/include/types.h	(revision ccb426c40c1bb63880c8f1dd8edb16e9b19286f9)
+++ kernel/arch/abs32le/include/types.h	(revision 09a0bd4a4ab5a70550f327984b135164b05aa58d)
@@ -35,4 +35,7 @@
 #ifndef KERN_abs32le_TYPES_H_
 #define KERN_abs32le_TYPES_H_
+
+#define ATOMIC_COUNT_MIN  UINT32_MIN
+#define ATOMIC_COUNT_MAX  UINT32_MAX
 
 typedef uint32_t size_t;