Index: kernel/generic/include/atomic.h
===================================================================
--- kernel/generic/include/atomic.h	(revision 33c4f72505a3c4729684b213f04c3c7feb9c842b)
+++ kernel/generic/include/atomic.h	(revision c621f4aa64c16cb4d9c2b20dbf5be59c66c25ed3)
@@ -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)
 {