Index: src/include/cpu/x86/msr.h
===================================================================
--- src/include/cpu/x86/msr.h	(revision 5765)
+++ src/include/cpu/x86/msr.h	(working copy)
@@ -29,7 +29,7 @@
         msr_t msr;
 } msrinit_t;
 
-static inline msr_t rdmsr(unsigned index)
+static inline __attribute__((always_inline)) msr_t rdmsr(unsigned index)
 {
 	msr_t result;
 	__asm__ __volatile__ (
@@ -40,7 +40,7 @@
 	return result;
 }
 
-static inline void wrmsr(unsigned index, msr_t msr)
+static inline __attribute__((always_inline)) void wrmsr(unsigned index, msr_t msr)
 {
 	__asm__ __volatile__ (
 		"wrmsr"
Index: src/include/cpu/x86/cache.h
===================================================================
--- src/include/cpu/x86/cache.h	(revision 5765)
+++ src/include/cpu/x86/cache.h	(working copy)
@@ -74,7 +74,7 @@
 	asm volatile("invd" ::: "memory");
 }
 
-static inline void enable_cache(void)
+static inline __attribute__((always_inline)) void enable_cache(void)
 {
 	unsigned long cr0;
 	cr0 = read_cr0();
@@ -82,7 +82,7 @@
 	write_cr0(cr0);
 }
 
-static inline void disable_cache(void)
+static inline __attribute__((always_inline)) void disable_cache(void)
 {
 	/* Disable and write back the cache */
 	unsigned long cr0;