Index: kernel/generic/include/atomic.h
===================================================================
--- kernel/generic/include/atomic.h	(revision 33c4f72505a3c4729684b213f04c3c7feb9c842b)
+++ kernel/generic/include/atomic.h	(revision 0e9b512035036713c382370cb570a3881afa4209)
@@ -40,5 +40,5 @@
 #include <verify.h>
 
-ATOMIC static inline void atomic_set(atomic_t *val, atomic_count_t i)
+NO_TRACE ATOMIC static inline void atomic_set(atomic_t *val, atomic_count_t i)
     WRITES(&val->count)
     REQUIRES_EXTENT_MUTABLE(val)
@@ -47,5 +47,5 @@
 }
 
-ATOMIC static inline atomic_count_t atomic_get(atomic_t *val)
+NO_TRACE ATOMIC static inline atomic_count_t atomic_get(atomic_t *val)
     REQUIRES_EXTENT_MUTABLE(val)
 {