diff --git a/include/nuttx/spinlock.h b/include/nuttx/spinlock.h
index 3ce3391b01..544facfef9 100644
--- a/include/nuttx/spinlock.h
+++ b/include/nuttx/spinlock.h
@@ -42,7 +42,7 @@
 
 #include <nuttx/config.h>
 
-#include <sys/type.h>
+#include <sys/types.h>
 #include <stdint.h>
 
 #ifdef CONFIG_SPINLOCK
diff --git a/include/sys/types.h b/include/sys/types.h
index cc6672d2c0..a818cc2a80 100644
--- a/include/sys/types.h
+++ b/include/sys/types.h
@@ -244,6 +244,20 @@ typedef uint32_t     clock_t;
 typedef uint32_t     useconds_t;
 typedef int32_t      suseconds_t;
 
+#ifdef CONFIG_SMP
+/* This is the smallest integer type that will hold a bitset of all CPUs */
+
+#if (CONFIG_SMP_NCPUS <= 8)
+typedef volatile uint8_t cpu_set_t;
+#elif (CONFIG_SMP_NCPUS <= 16)
+typedef volatile uint16_t cpu_set_t;
+#elif (CONFIG_SMP_NCPUS <= 32)
+typedef volatile uint32_t cpu_set_t;
+#else
+#  error SMP: Extensions needed to support this number of CPUs
+#endif
+#endif /* CONFIG_SMP */
+
 /* BSD types provided only to support porting to NuttX. */
 
 typedef unsigned char  u_char;