Index: kernel/arch/abs32le/include/atomic.h
===================================================================
--- kernel/arch/abs32le/include/atomic.h	(revision 4fe907b9451912ec457f50c02ea022c9fd7bab92)
+++ kernel/arch/abs32le/include/atomic.h	(revision e3038b41e1f6e1ef905bbc80916933e18d3e3008)
@@ -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));
 }
Index: kernel/arch/abs32le/include/interrupt.h
===================================================================
--- kernel/arch/abs32le/include/interrupt.h	(revision 4fe907b9451912ec457f50c02ea022c9fd7bab92)
+++ kernel/arch/abs32le/include/interrupt.h	(revision e3038b41e1f6e1ef905bbc80916933e18d3e3008)
@@ -54,4 +54,5 @@
 
 static inline int istate_from_uspace(istate_t *istate)
+    REQUIRES_EXTENT_MUTABLE(istate)
 {
 	/* On real hardware this checks whether the interrupted
@@ -62,4 +63,5 @@
 
 static inline void istate_set_retaddr(istate_t *istate, uintptr_t retaddr)
+    WRITES(&istate->ip)
 {
 	/* On real hardware this sets the instruction pointer. */
@@ -69,4 +71,5 @@
 
 static inline unative_t istate_get_pc(istate_t *istate)
+    REQUIRES_EXTENT_MUTABLE(istate)
 {
 	/* On real hardware this returns the instruction pointer. */
@@ -76,4 +79,5 @@
 
 static inline unative_t istate_get_fp(istate_t *istate)
+    REQUIRES_EXTENT_MUTABLE(istate)
 {
 	/* On real hardware this returns the frame pointer. */
Index: kernel/arch/abs32le/include/mm/page.h
===================================================================
--- kernel/arch/abs32le/include/mm/page.h	(revision 4fe907b9451912ec457f50c02ea022c9fd7bab92)
+++ kernel/arch/abs32le/include/mm/page.h	(revision e3038b41e1f6e1ef905bbc80916933e18d3e3008)
@@ -140,4 +140,5 @@
 
 static inline unsigned int get_pt_flags(pte_t *pt, size_t i)
+    REQUIRES_ARRAY_MUTABLE(pt, PTL0_ENTRIES_ARCH)
 {
 	pte_t *p = &pt[i];
@@ -155,4 +156,6 @@
 
 static inline void set_pt_flags(pte_t *pt, size_t i, int flags)
+    WRITES(ARRAY_RANGE(pt, PTL0_ENTRIES_ARCH))
+    REQUIRES_ARRAY_MUTABLE(pt, PTL0_ENTRIES_ARCH)
 {
 	pte_t *p = &pt[i];