diff --git a/repos/base-hw/lib/mk/spec/cortex_a9/core.inc b/repos/base-hw/lib/mk/spec/cortex_a9/core.inc
index 8ea7a4cbd..b50f1ff5d 100644
--- a/repos/base-hw/lib/mk/spec/cortex_a9/core.inc
+++ b/repos/base-hw/lib/mk/spec/cortex_a9/core.inc
@@ -11,6 +11,7 @@ INC_DIR += $(REP_DIR)/src/core/include/spec/arm_gic
 # add C++ sources
 SRC_CC += spec/cortex_a9/kernel/cpu.cc
 SRC_CC += spec/cortex_a9/cpu.cc
+SRC_CC += spec/cortex_a9/fpu.cc
 SRC_CC += spec/arm/smp/kernel/thread_update_pd.cc
 SRC_CC += spec/arm/smp/kernel/cpu.cc
 SRC_CC += spec/arm/kernel/cpu_context.cc
diff --git a/repos/base-hw/lib/mk/spec/x86/core.inc b/repos/base-hw/lib/mk/spec/x86/core.inc
index e6e929068..6dfe2beb0 100644
--- a/repos/base-hw/lib/mk/spec/x86/core.inc
+++ b/repos/base-hw/lib/mk/spec/x86/core.inc
@@ -16,6 +16,7 @@ SRC_CC += spec/x86/kernel/cpu.cc
 SRC_CC += spec/x86/kernel/thread.cc
 SRC_CC += spec/x86/platform_support.cc
 SRC_CC += spec/x86/cpu.cc
+SRC_CC += spec/x86/fpu.cc
 SRC_CC += spec/x86/bios_data_area.cc
 SRC_CC += spec/x86/io_port_session_component.cc
 SRC_CC += spec/x86/platform_services.cc
diff --git a/repos/base-hw/src/core/include/kernel/cpu.h b/repos/base-hw/src/core/include/kernel/cpu.h
index 9bcb85e02..435a2460a 100644
--- a/repos/base-hw/src/core/include/kernel/cpu.h
+++ b/repos/base-hw/src/core/include/kernel/cpu.h
@@ -117,12 +117,11 @@ class Kernel::Cpu_domain_update : public Double_list_item
 		virtual void _cpu_domain_update_unblocks() = 0;
 };
 
-class Kernel::Cpu_job : public Cpu_share
+class Kernel::Cpu_job : public Genode::Cpu::User_context, public Cpu_share
 {
 	protected:
 
-		Cpu *          _cpu;
-		Cpu_lazy_state _lazy_state;
+		Cpu * _cpu;
 
 		/**
 		 * Handle interrupt exception that occured during execution on CPU 'id'
@@ -196,10 +195,9 @@ class Kernel::Cpu_job : public Cpu_share
 		 ***************/
 
 		void cpu(Cpu * const cpu) { _cpu = cpu; }
-		Cpu_lazy_state * lazy_state() { return &_lazy_state; }
 };
 
-class Kernel::Cpu_idle : public Genode::Cpu::User_context, public Cpu_job
+class Kernel::Cpu_idle : public Cpu_job
 {
 	private:
 
diff --git a/repos/base-hw/src/core/include/kernel/thread.h b/repos/base-hw/src/core/include/kernel/thread.h
index 719b88fd3..f48928584 100644
--- a/repos/base-hw/src/core/include/kernel/thread.h
+++ b/repos/base-hw/src/core/include/kernel/thread.h
@@ -77,9 +77,8 @@ class Kernel::Thread_event : public Signal_ack_handler
  */
 class Kernel::Thread
 :
-	public Kernel::Object, public Cpu::User_context, public Cpu_domain_update,
-	public Ipc_node, public Signal_context_killer, public Signal_handler,
-	public Cpu_job
+	public Kernel::Object, public Cpu_job, public Cpu_domain_update,
+	public Ipc_node, public Signal_context_killer, public Signal_handler
 {
 	friend class Thread_event;
 	friend class Core_thread;
@@ -190,7 +189,7 @@ class Kernel::Thread
 		void _call();
 
 		/**
-		 * Return amount of timer tics that 'quota' is worth 
+		 * Return amount of timer tics that 'quota' is worth
 		 */
 		size_t _core_to_kernel_quota(size_t const quota) const;
 
diff --git a/repos/base-hw/src/core/include/spec/arm/cpu_support.h b/repos/base-hw/src/core/include/spec/arm/cpu_support.h
index 8d52bdd00..3350caf91 100644
--- a/repos/base-hw/src/core/include/spec/arm/cpu_support.h
+++ b/repos/base-hw/src/core/include/spec/arm/cpu_support.h
@@ -28,13 +28,8 @@ namespace Kernel { class Pd; }
 
 namespace Genode
 {
-	/**
-	 * CPU driver for core
-	 */
 	class Arm;
 
-	class Cpu_lazy_state;
-
 	typedef Genode::uint64_t sizet_arithm_t;
 }
 
@@ -544,8 +539,8 @@ class Genode::Arm
 		 ** Dummies **
 		 *************/
 
-		void prepare_proceeding(Cpu_lazy_state *, Cpu_lazy_state *) { }
-		bool retry_undefined_instr(Cpu_lazy_state *) { return false; }
+		void switch_to(User_context&) { }
+		bool retry_undefined_instr(Context&) { return false; }
 
 		/**
 		 * Return kernel name of the executing CPU
diff --git a/repos/base-hw/src/core/include/spec/arm/fpu.h b/repos/base-hw/src/core/include/spec/arm/fpu.h
new file mode 100644
index 000000000..fb5ca9f3c
--- /dev/null
+++ b/repos/base-hw/src/core/include/spec/arm/fpu.h
@@ -0,0 +1,246 @@
+/*
+ * \brief  ARM-specific FPU driver for core
+ * \author Stefan Kalkowski
+ * \author Martin stein
+ * \date   2016-01-19
+ */
+
+/*
+ * Copyright (C) 2016 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+#ifndef _SPEC__ARM__FPU_H_
+#define _SPEC__ARM__FPU_H_
+
+#include <util/register.h>
+
+namespace Genode { class Fpu; }
+
+/**
+ * FPU driver for the ARM VFPv3-D16 architecture
+ */
+class Genode::Fpu
+{
+	private:
+
+		/**
+		 * Floating-point Status and Control Register
+		 */
+		struct Fpscr : Register<32>
+		{
+			/**
+			 * Read register value
+			 */
+			static access_t read()
+			{
+				/* FIXME: See annotation 1. */
+				access_t v;
+				asm volatile ("mrc p10, 7, %[v], cr1, cr0, 0" : [v] "=r" (v) ::);
+				return v;
+			}
+
+			/**
+			 * Override register value
+			 *
+			 * \param v  write value
+			 */
+			static void write(access_t const v)
+			{
+				/* FIXME: See annotation 1. */
+				asm volatile ("mcr p10, 7, %[v], cr1, cr0, 0" :: [v] "r" (v) :);
+			}
+		};
+
+		/**
+		 * Floating-Point Exception Control register
+		 */
+		struct Fpexc : Register<32>
+		{
+			struct En  : Bitfield<30, 1> { };
+
+			/**
+			 * Read register value
+			 */
+			static access_t read()
+			{
+				/* FIXME: See annotation 1. */
+				access_t v;
+				asm volatile ("mrc p10, 7, %[v], cr8, cr0, 0" : [v] "=r" (v) ::);
+				return v;
+			}
+
+			/**
+			 * Override register value
+			 *
+			 * \param v  write value
+			 */
+			static void write(access_t const v)
+			{
+				/* FIXME: See annotation 1. */
+				asm volatile ("mcr p10, 7, %[v], cr8, cr0, 0" :: [v] "r" (v) :);
+			}
+		};
+
+	public:
+
+		class Context
+		{
+			private:
+
+				friend class Fpu;
+
+				/* advanced FP/SIMD - system registers */
+				uint32_t fpscr;
+				uint32_t fpexc;
+
+				/* advanced FP/SIMD - general purpose registers d0-d15 */
+				uint64_t d0, d1, d2,  d3,  d4,  d5,  d6,  d7;
+				uint64_t d8, d9, d10, d11, d12, d13, d14, d15;
+
+				Fpu * _fpu = nullptr;
+
+			public:
+
+				Context() : fpexc(Fpexc::En::bits(1)) { }
+
+				~Context() { if (_fpu) _fpu->unset(*this); }
+		};
+
+	private:
+
+		Context * _context = nullptr;
+
+		/**
+		 * Enable FPU
+		 */
+		void _enable()
+		{
+			Fpexc::access_t fpexc = Fpexc::read();
+			Fpexc::En::set(fpexc, 1);
+			Fpexc::write(fpexc);
+		}
+
+		/**
+		 * Disable FPU
+		 */
+		void _disable()
+		{
+			Fpexc::access_t fpexc = Fpexc::read();
+			Fpexc::En::set(fpexc, 0);
+			Fpexc::write(fpexc);
+		}
+
+		/**
+		 * Save FPU context
+		 */
+		void _save()
+		{
+			/* save system registers */
+			_context->fpexc = Fpexc::read();
+			_context->fpscr = Fpscr::read();
+
+			/*
+			 * Save D0 - D15
+			 *
+			 * FIXME: See annotation 2.
+			 */
+			void * const d0_d15_base = &_context->d0;
+			asm volatile (
+				"stc p11, cr0, [%[d0_d15_base]], #128"
+				:: [d0_d15_base] "r" (d0_d15_base) : );
+		}
+
+		/**
+		 * Load context to FPU
+		 */
+		void _load()
+		{
+			/* load system registers */
+			Fpexc::write(_context->fpexc);
+			Fpscr::write(_context->fpscr);
+
+			/*
+			 * Load D0 - D15
+			 *
+			 * FIXME: See annotation 2.
+			 */
+			void * const d0_d15_base = &_context->d0;
+			asm volatile (
+				"ldc p11, cr0, [%[d0_d15_base]], #128"
+				:: [d0_d15_base] "r" (d0_d15_base) : );
+		}
+
+		/**
+		 * Return wether the FPU is enabled
+		 */
+		bool _enabled()
+		{
+			Fpexc::access_t fpexc = Fpexc::read();
+			return Fpexc::En::get(fpexc);
+		}
+
+	public:
+
+		/**
+		 * Initialize FPU
+		 */
+		void init();
+
+		void switch_to(Context & context)
+		{
+			if (_context == &context) return;
+			_disable();
+		}
+
+		/**
+		 * Return wether the FPU fault can be solved
+		 *
+		 * \param state  CPU state of the user
+		 */
+		bool fault(Context & context)
+		{
+			if (_enabled()) { return false; }
+			_enable();
+			if (_context != &context) {
+				if (_context) {
+					_save();
+					_context->_fpu = nullptr;
+				}
+				_context = &context;
+				_context->_fpu = this;
+				_load();
+			}
+			return true;
+		}
+
+		/**
+		 * Unset FPU context
+		 */
+		void unset(Context &context) {
+			if (_context == &context) _context = nullptr; }
+};
+
+/*
+ * Annotation 1
+ *
+ *  According to the ARMv7 manual this should be done via vmsr/vmrs instruction
+ *  but it seems that binutils 2.22 doesn't fully support this yet. Hence, we
+ *  use a co-processor instruction instead. The parameters to target the
+ *  register this way can be determined via 'sys/arm/include/vfp.h' and
+ *  'sys/arm/arm/vfp.c' of the FreeBSD head branch as from 2014.04.17.
+ */
+
+/*
+ * Annotation 2
+ *
+ *  According to the ARMv7 manual this should be done via vldm/vstm instruction
+ *  but it seems that binutils 2.22 doesn't fully support this yet. Hence, we
+ *  use a co-processor instruction instead. The parameters to target the
+ *  register this way can be determined via 'sys/arm/arm/vfp.c' of the FreeBSD
+ *  head branch as from 2014.04.17.
+ */
+
+#endif /* _SPEC__ARM__FPU_H_ */
diff --git a/repos/base-hw/src/core/include/spec/arm_v6/cpu.h b/repos/base-hw/src/core/include/spec/arm_v6/cpu.h
index 38e3def49..201746183 100644
--- a/repos/base-hw/src/core/include/spec/arm_v6/cpu.h
+++ b/repos/base-hw/src/core/include/spec/arm_v6/cpu.h
@@ -20,22 +20,8 @@
 #include <assert.h>
 #include <board.h>
 
-namespace Genode
-{
-	/**
-	 * Part of CPU state that is not switched on every mode transition
-	 */
-	class Cpu_lazy_state { };
+namespace Genode { class Cpu; }
 
-	/**
-	 * CPU driver for core
-	 */
-	class Cpu;
-}
-
-namespace Kernel {
-	using Genode::Cpu_lazy_state;
-}
 
 class Genode::Cpu : public Arm
 {
@@ -90,11 +76,6 @@ class Genode::Cpu : public Arm
 			invalidate_tlb();
 		}
 
-		/**
-		 * Return wether to retry an undefined user instruction after this call
-		 */
-		bool retry_undefined_instr(Cpu_lazy_state *) { return false; }
-
 		/**
 		 * Post processing after a translation was added to a translation table
 		 *
@@ -108,7 +89,6 @@ class Genode::Cpu : public Arm
 		 ** Dummies **
 		 *************/
 
-		static void prepare_proceeding(Cpu_lazy_state *, Cpu_lazy_state *) { }
 		static void wait_for_interrupt() { /* FIXME */ }
 		static void data_synchronization_barrier() { /* FIXME */ }
 		static void invalidate_control_flow_predictions() { /* FIXME */ }
diff --git a/repos/base-hw/src/core/include/spec/cortex_a15/cpu.h b/repos/base-hw/src/core/include/spec/cortex_a15/cpu.h
index 3054bd161..fba697282 100644
--- a/repos/base-hw/src/core/include/spec/cortex_a15/cpu.h
+++ b/repos/base-hw/src/core/include/spec/cortex_a15/cpu.h
@@ -18,20 +18,8 @@
 /* core includes */
 #include <spec/arm_v7/cpu_support.h>
 
-namespace Genode
-{
-	/**
-	 * Part of CPU state that is not switched on every mode transition
-	 */
-	class Cpu_lazy_state { };
+namespace Genode { class Cpu; }
 
-	/**
-	 * CPU driver for core
-	 */
-	class Cpu;
-}
-
-namespace Kernel { using Genode::Cpu_lazy_state; }
 
 class Genode::Cpu : public Arm_v7
 {
@@ -408,11 +396,6 @@ class Genode::Cpu : public Arm_v7
 		};
 
 
-		/**
-		 * Return wether to retry an undefined user instruction after this call
-		 */
-		bool retry_undefined_instr(Cpu_lazy_state *) { return false; }
-
 		/**
 		 * Return kernel name of the executing CPU
 		 */
@@ -455,7 +438,8 @@ class Genode::Cpu : public Arm_v7
 		 ** Dummies **
 		 *************/
 
-		static void prepare_proceeding(Cpu_lazy_state *, Cpu_lazy_state *) { }
+		void switch_to(User_context&) { }
+		bool retry_undefined_instr(Context&) { return false; }
 };
 
 #endif /* _CPU_H_ */
diff --git a/repos/base-hw/src/core/include/spec/cortex_a8/cpu.h b/repos/base-hw/src/core/include/spec/cortex_a8/cpu.h
index 82e041436..46fb44db9 100644
--- a/repos/base-hw/src/core/include/spec/cortex_a8/cpu.h
+++ b/repos/base-hw/src/core/include/spec/cortex_a8/cpu.h
@@ -18,20 +18,8 @@
 /* core includes */
 #include <spec/arm_v7/cpu_support.h>
 
-namespace Genode
-{
-	/**
-	 * Part of CPU state that is not switched on every mode transition
-	 */
-	class Cpu_lazy_state { };
+namespace Genode { class Cpu; }
 
-	/**
-	 * CPU driver for core
-	 */
-	class Cpu;
-}
-
-namespace Kernel { using Genode::Cpu_lazy_state; }
 
 class Genode::Cpu : public Arm_v7
 {
diff --git a/repos/base-hw/src/core/include/spec/cortex_a9/cpu_support.h b/repos/base-hw/src/core/include/spec/cortex_a9/cpu_support.h
index 92a2ae462..2ff8d6913 100644
--- a/repos/base-hw/src/core/include/spec/cortex_a9/cpu_support.h
+++ b/repos/base-hw/src/core/include/spec/cortex_a9/cpu_support.h
@@ -16,51 +16,19 @@
 #define _SPEC__CORTEX_A9__CPU_SUPPORT_H_
 
 /* core includes */
+#include <spec/arm/fpu.h>
 #include <spec/arm_v7/cpu_support.h>
 #include <board.h>
 
-namespace Genode
-{
-	/**
-	 * Part of CPU state that is not switched on every mode transition
-	 */
-	class Cpu_lazy_state;
-
-	/**
-	 * CPU driver for core
-	 */
-	class Cortex_a9;
-}
-
-namespace Kernel { using Genode::Cpu_lazy_state; }
-
-class Genode::Cpu_lazy_state
-{
-	friend class Cortex_a9;
-
-	private:
-
-		/* advanced FP/SIMD - system registers */
-		uint32_t fpscr;
-		uint32_t fpexc;
-
-		/* advanced FP/SIMD - general purpose registers d0-d15 */
-		uint64_t d0, d1, d2,  d3,  d4,  d5,  d6,  d7;
-		uint64_t d8, d9, d10, d11, d12, d13, d14, d15;
-
-	public:
-
-		/**
-		 * Constructor
-		 */
-		inline Cpu_lazy_state();
-};
+namespace Genode { class Cortex_a9; }
 
 class Genode::Cortex_a9 : public Arm_v7
 {
-	friend class Cpu_lazy_state;
+	protected:
 
-	private:
+		Fpu _fpu;
+
+	public:
 
 		/**
 		 * Coprocessor Access Control Register
@@ -85,135 +53,10 @@ class Genode::Cortex_a9 : public Arm_v7
 			 *
 			 * \param v  write value
 			 */
-			static void write(access_t const v)
-			{
-				asm volatile ("mcr p15, 0, %[v], c1, c0, 2" :: [v]"r"(v) :);
-			}
+			static void write(access_t const v) {
+				asm volatile ("mcr p15, 0, %[v], c1, c0, 2" :: [v]"r"(v) :); }
 		};
 
-		/**
-		 * Floating-point Status and Control Register
-		 */
-		struct Fpscr : Register<32>
-		{
-			/**
-			 * Read register value
-			 */
-			static access_t read()
-			{
-				/* FIXME: See annotation 1. */
-				access_t v;
-				asm volatile ("mrc p10, 7, %[v], cr1, cr0, 0" : [v] "=r" (v) ::);
-				return v;
-			}
-
-			/**
-			 * Override register value
-			 *
-			 * \param v  write value
-			 */
-			static void write(access_t const v)
-			{
-				/* FIXME: See annotation 1. */
-				asm volatile ("mcr p10, 7, %[v], cr1, cr0, 0" :: [v] "r" (v) :);
-			}
-		};
-
-		/**
-		 * Floating-Point Exception Control register
-		 */
-		struct Fpexc : Register<32>
-		{
-			struct En  : Bitfield<30, 1> { };
-
-			/**
-			 * Read register value
-			 */
-			static access_t read()
-			{
-				/* FIXME: See annotation 1. */
-				access_t v;
-				asm volatile ("mrc p10, 7, %[v], cr8, cr0, 0" : [v] "=r" (v) ::);
-				return v;
-			}
-
-			/**
-			 * Override register value
-			 *
-			 * \param v  write value
-			 */
-			static void write(access_t const v)
-			{
-				/* FIXME: See annotation 1. */
-				asm volatile ("mcr p10, 7, %[v], cr8, cr0, 0" :: [v] "r" (v) :);
-			}
-		};
-
-		Cpu_lazy_state * _advanced_fp_simd_state;
-
-		/**
-		 * Enable or disable the advanced FP/SIMD extension
-		 *
-		 * \param enabled  wether to enable or to disable advanced FP/SIMD
-		 */
-		static void _toggle_advanced_fp_simd(bool const enabled)
-		{
-			Fpexc::access_t fpexc = Fpexc::read();
-			Fpexc::En::set(fpexc, enabled);
-			Fpexc::write(fpexc);
-		}
-
-		/**
-		 * Save state of the advanced FP/SIMD extension into 'state'
-		 */
-		static void _save_advanced_fp_simd_state(Cpu_lazy_state * const state)
-		{
-			/* save system registers */
-			state->fpexc = Fpexc::read();
-			state->fpscr = Fpscr::read();
-
-			/*
-			 * Save D0 - D15
-			 *
-			 * FIXME: See annotation 2.
-			 */
-			void * const d0_d15_base = &state->d0;
-			asm volatile (
-				"stc p11, cr0, [%[d0_d15_base]], #128"
-				:: [d0_d15_base] "r" (d0_d15_base) : );
-		}
-
-		/**
-		 * Load state of the advanced FP/SIMD extension from 'state'
-		 */
-		static void _load_advanced_fp_simd_state(Cpu_lazy_state * const state)
-		{
-			/* load system registers */
-			Fpexc::write(state->fpexc);
-			Fpscr::write(state->fpscr);
-
-			/*
-			 * Load D0 - D15
-			 *
-			 * FIXME: See annotation 2.
-			 */
-			void * const d0_d15_base = &state->d0;
-			asm volatile (
-				"ldc p11, cr0, [%[d0_d15_base]], #128"
-				:: [d0_d15_base] "r" (d0_d15_base) : );
-		}
-
-		/**
-		 * Return wether the advanced FP/SIMD extension is enabled
-		 */
-		static bool _advanced_fp_simd_enabled()
-		{
-			Fpexc::access_t fpexc = Fpexc::read();
-			return Fpexc::En::get(fpexc);
-		}
-
-	public:
-
 		/**
 		 * Auxiliary Control Register
 		 */
@@ -239,54 +82,22 @@ class Genode::Cortex_a9 : public Arm_v7
 			}
 		};
 
-		/**
-		 * Constructor
-		 */
-		Cortex_a9() : _advanced_fp_simd_state(0) { }
+		struct User_context : Arm::User_context, Fpu::Context { };
 
 		/**
-		 * Initialize advanced FP/SIMD extension
-		 */
-		static void init_advanced_fp_simd()
-		{
-			Cpacr::access_t cpacr = Cpacr::read();
-			Cpacr::Cp10::set(cpacr, 3);
-			Cpacr::Cp11::set(cpacr, 3);
-			Cpacr::write(cpacr);
-			_toggle_advanced_fp_simd(false);
-		}
-
-		/**
-		 * Prepare for the proceeding of a user
+		 * Next cpu context to switch to
 		 *
-		 * \param old_state  CPU state of the last user
-		 * \param new_state  CPU state of the next user
+		 * \param context  context to switch to
 		 */
-		static void prepare_proceeding(Cpu_lazy_state * const old_state,
-		                               Cpu_lazy_state * const new_state)
-		{
-			if (old_state == new_state) { return; }
-			_toggle_advanced_fp_simd(false);
-		}
+		void switch_to(User_context & context) { _fpu.switch_to(context); }
 
 		/**
 		 * Return wether to retry an undefined user instruction after this call
 		 *
 		 * \param state  CPU state of the user
 		 */
-		bool retry_undefined_instr(Cpu_lazy_state * const state)
-		{
-			if (_advanced_fp_simd_enabled()) { return false; }
-			_toggle_advanced_fp_simd(true);
-			if (_advanced_fp_simd_state != state) {
-				if (_advanced_fp_simd_state) {
-					_save_advanced_fp_simd_state(_advanced_fp_simd_state);
-				}
-				_load_advanced_fp_simd_state(state);
-				_advanced_fp_simd_state = state;
-			}
-			return true;
-		}
+		bool retry_undefined_instr(User_context & context) {
+			return _fpu.fault(context); }
 
 		/**
 		 * Write back dirty cache lines and invalidate whole data cache
@@ -329,26 +140,4 @@ class Genode::Cortex_a9 : public Arm_v7
 		static void translation_added(addr_t, size_t) { }
 };
 
-Genode::Cpu_lazy_state::Cpu_lazy_state() { fpexc = Cortex_a9::Fpexc::En::bits(1); }
-
-/*
- * Annotation 1
- *
- *  According to the ARMv7 manual this should be done via vmsr/vmrs instruction
- *  but it seems that binutils 2.22 doesn't fully support this yet. Hence, we
- *  use a co-processor instruction instead. The parameters to target the
- *  register this way can be determined via 'sys/arm/include/vfp.h' and
- *  'sys/arm/arm/vfp.c' of the FreeBSD head branch as from 2014.04.17.
- */
-
-/*
- * Annotation 2
- *
- *  According to the ARMv7 manual this should be done via vldm/vstm instruction
- *  but it seems that binutils 2.22 doesn't fully support this yet. Hence, we
- *  use a co-processor instruction instead. The parameters to target the
- *  register this way can be determined via 'sys/arm/arm/vfp.c' of the FreeBSD
- *  head branch as from 2014.04.17.
- */
-
 #endif /* _SPEC__CORTEX_A9__CPU_SUPPORT_H_ */
diff --git a/repos/base-hw/src/core/include/spec/x86/cpu_support.h b/repos/base-hw/src/core/include/spec/x86/cpu_support.h
index 92979d5fd..3b9206170 100644
--- a/repos/base-hw/src/core/include/spec/x86/cpu_support.h
+++ b/repos/base-hw/src/core/include/spec/x86/cpu_support.h
@@ -25,6 +25,7 @@
 #include <unmanaged_singleton.h>
 
 /* core includes */
+#include <fpu.h>
 #include <gdt.h>
 #include <idt.h>
 #include <tss.h>
@@ -33,214 +34,19 @@
 extern int _mt_idt;
 extern int _mt_tss;
 
-namespace Genode
-{
-	/**
-	 * Part of CPU state that is not switched on every mode transition
-	 */
-	class Cpu_lazy_state;
-
-	/**
-	 * CPU driver for core
-	 */
-	class Cpu;
-}
-
-namespace Kernel
-{
-	using Genode::Cpu_lazy_state;
-
-	class Pd;
-}
-
-class Genode::Cpu_lazy_state
-{
-	friend class Cpu;
-
-	private:
-
-		enum { MXCSR_DEFAULT = 0x1f80 };
-
-		/*
-		 * FXSAVE area providing storage for x87 FPU, MMX, XMM, and MXCSR
-		 * registers.
-		 *
-		 * For further details see Intel SDM Vol. 2A, 'FXSAVE instruction'.
-		 */
-		char fxsave_area[527];
-
-		/* 16-byte aligned start of FXSAVE area. */
-		char *start;
-
-		/**
-		 * Load x87 FPU State from fxsave area.
-		 */
-		inline void load()
-		{
-			if (!start) {
-				set_start();
-				init();
-				return;
-			}
-			asm volatile ("fxrstor %0" : : "m" (*start));
-		}
-
-		/**
-		 * Save x87 FPU State to fxsave area.
-		 */
-		inline void save() { asm volatile ("fxsave %0" : "=m" (*start)); }
-
-		/**
-		 * Return current value of MXCSR register.
-		 */
-		static inline unsigned get_mxcsr()
-		{
-			unsigned value;
-			asm volatile ("stmxcsr %0" : "=m" (value));
-			return value;
-		}
-
-		/**
-		 * Set MXCSR register to given value.
-		 */
-		static inline void set_mxcsr(unsigned value)
-		{
-			asm volatile ("ldmxcsr %0" : : "m" (value));
-		}
-
-		/**
-		 * Initialize FPU
-		 *
-		 * Doesn't check for pending unmasked floating-point exceptions and
-		 * explicitly sets the MXCSR to the default value.
-		 */
-		inline void init()
-		{
-			asm volatile ("fninit");
-			set_mxcsr(MXCSR_DEFAULT);
-		};
-
-		/**
-		 * Set 16-byte aligned start of fxsave area.
-		 */
-		inline void set_start()
-		{
-			start = fxsave_area;
-			if((addr_t)start & 15)
-				start = (char *)((addr_t)start & ~15) + 16;
-		};
-
-	public:
-
-		/**
-		 * Constructor
-		 */
-		inline Cpu_lazy_state() : start(0) { };
-
-} __attribute__((aligned(16)));
+namespace Genode { class Cpu; }
 
 
 class Genode::Cpu
 {
-	friend class Cpu_lazy_state;
-
-	protected:
-
-		Idt *_idt;
-		Tss *_tss;
-		Cpu_lazy_state *_fpu_state;
-
-		struct Cr0; /* Control register 0 */
-		struct Cr4; /* Control register 4 */
-
-		/**
-		 * Disable FPU by setting the TS flag in CR0.
-		 */
-		static void _disable_fpu();
-
-		/**
-		 * Enable FPU by clearing the TS flag in CR0.
-		 */
-		static void _enable_fpu() { asm volatile ("clts"); }
-
-		/**
-		 * Initialize all FPU-related CR flags
-		 *
-		 * Initialize FPU with SSE extensions by setting required CR0 and CR4
-		 * bits to configure the FPU environment according to Intel SDM Vol.
-		 * 3A, sections 9.2 and 9.6.
-		 */
-		static void _init_fpu();
-
-		/**
-		 * Returns True if the FPU is enabled.
-		 */
-		static bool _fpu_enabled();
-
 	public:
 
-		Cpu() : _fpu_state(0)
-		{
-			if (primary_id() == executing_id()) {
-				_idt = new (&_mt_idt) Idt();
-				_idt->setup(Cpu::exception_entry);
+		struct Pd {};
 
-				_tss = new (&_mt_tss) Tss();
-				_tss->load();
-			}
-			_idt->load(Cpu::exception_entry);
-			_tss->setup(Cpu::exception_entry);
-		}
-
-		static constexpr addr_t exception_entry = 0xffff0000;
-		static constexpr addr_t mtc_size        = 1 << 13;
-
-		/**
-		 * Control register 2: Page-fault linear address
-		 *
-		 * See Intel SDM Vol. 3A, section 2.5.
-		 */
-		struct Cr2 : Register<64>
-		{
-			struct Addr : Bitfield<0, 63> { };
-
-			static access_t read()
-			{
-				access_t v;
-				asm volatile ("mov %%cr2, %0" : "=r" (v) :: );
-				return v;
-			}
-		};
-
-		/**
-		 * Control register 3: Page-Directory base register
-		 *
-		 * See Intel SDM Vol. 3A, section 2.5.
-		 */
-		struct Cr3 : Register<64>
-		{
-			struct Pwt : Bitfield<3,1> { };    /* Page-level write-through    */
-			struct Pcd : Bitfield<4,1> { };    /* Page-level cache disable    */
-			struct Pdb : Bitfield<12, 36> { }; /* Page-directory base address */
-
-			static void write(access_t const v) {
-				asm volatile ("mov %0, %%cr3" :: "r" (v) : ); }
-
-			static access_t read()
-			{
-				access_t v;
-				asm volatile ("mov %%cr3, %0" : "=r" (v) :: );
-				return v;
-			}
-
-			/**
-			 * Return initialized value
-			 *
-			 * \param table  base of targeted translation table
-			 */
-			static access_t init(addr_t const table) {
-				return Pdb::masked(table); }
-		};
+		struct Cr0; /* Control register 0 */
+		struct Cr2; /* Control register 2 */
+		struct Cr3; /* Control register 3 */
+		struct Cr4; /* Control register 4 */
 
 		/**
 		 * Extend basic CPU state by members relevant for 'base-hw' only
@@ -263,32 +69,14 @@ class Genode::Cpu
 			 * \param table  physical base of appropriate translation table
 			 * \param core   whether it is a core thread or not
 			 */
-			void init(addr_t const table, bool core)
-			{
-				/* Constants to handle IF, IOPL values */
-				enum {
-					EFLAGS_IF_SET = 1 << 9,
-					EFLAGS_IOPL_3 = 3 << 12,
-				};
-
-				cr3 = Cr3::init(table);
-
-				/*
-				 * Enable interrupts for all threads, set I/O privilege level
-				 * (IOPL) to 3 for core threads to allow UART access.
-				 */
-				eflags = EFLAGS_IF_SET;
-				if (core) eflags |= EFLAGS_IOPL_3;
-				else Gdt::load(Cpu::exception_entry);
-			}
+			void init(addr_t const table, bool core);
 		};
 
-		struct Pd {};
 
 		/**
 		 * An usermode execution state
 		 */
-		struct User_context : Context
+		struct User_context : Context, Fpu::Context
 		{
 			/**
 			 * Support for kernel calls
@@ -311,6 +99,21 @@ class Genode::Cpu
 			Kernel::Call_arg user_arg_7() const { return r11; }
 		};
 
+	protected:
+
+		Fpu   _fpu;
+		Idt * _idt;
+		Tss * _tss;
+
+	public:
+
+		Cpu();
+
+		Fpu & fpu() { return _fpu; }
+
+		static constexpr addr_t exception_entry = 0xffff0000;
+		static constexpr addr_t mtc_size        = 1 << 13;
+
 		/**
 		 * Wait for the next interrupt as cheap as possible
 		 */
@@ -319,26 +122,8 @@ class Genode::Cpu
 		/**
 		 * Return wether to retry an undefined user instruction after this call
 		 */
-		bool retry_undefined_instr(Cpu_lazy_state *) { return false; }
+		bool retry_undefined_instr(Context&) { return false; }
 
-		/**
-		 * Return whether to retry an FPU instruction after this call
-		 */
-		bool retry_fpu_instr(Cpu_lazy_state * const state)
-		{
-			if (_fpu_enabled())
-				return false;
-
-			_enable_fpu();
-			if (_fpu_state != state) {
-				if (_fpu_state)
-					_fpu_state->save();
-
-				state->load();
-				_fpu_state = state;
-			}
-			return true;
-		}
 
 		/**
 		 * Return kernel name of the executing CPU
@@ -351,21 +136,14 @@ class Genode::Cpu
 		static unsigned primary_id() { return 0; }
 
 		/**
-		 * Prepare for the proceeding of a user
+		 * Switch to new context
 		 *
-		 * \param old_state  CPU state of the last user
-		 * \param new_state  CPU state of the next user
+		 * \param context  next CPU context
 		 */
-		static void prepare_proceeding(Cpu_lazy_state * const old_state,
-		                               Cpu_lazy_state * const new_state)
-		{
-			if (old_state == new_state)
-				return;
-
-			_disable_fpu();
-		}
+		void switch_to(User_context &context) { _fpu.switch_to(context); }
 };
 
+
 struct Genode::Cpu::Cr0 : Register<64>
 {
 	struct Pe : Bitfield< 0, 1> { }; /* Protection Enable   */
@@ -391,6 +169,56 @@ struct Genode::Cpu::Cr0 : Register<64>
 	}
 };
 
+
+/**
+ * Control register 2: Page-fault linear address
+ *
+ * See Intel SDM Vol. 3A, section 2.5.
+ */
+struct Genode::Cpu::Cr2 : Register<64>
+{
+	struct Addr : Bitfield<0, 63> { };
+
+	static access_t read()
+	{
+		access_t v;
+		asm volatile ("mov %%cr2, %0" : "=r" (v) :: );
+		return v;
+	}
+};
+
+
+/**
+ * Control register 3: Page-Directory base register
+ *
+ * See Intel SDM Vol. 3A, section 2.5.
+ */
+struct Genode::Cpu::Cr3 : Register<64>
+{
+	struct Pwt : Bitfield<3,1> { };    /* Page-level write-through    */
+	struct Pcd : Bitfield<4,1> { };    /* Page-level cache disable    */
+	struct Pdb : Bitfield<12, 36> { }; /* Page-directory base address */
+
+	static void write(access_t const v) {
+		asm volatile ("mov %0, %%cr3" :: "r" (v) : ); }
+
+	static access_t read()
+	{
+		access_t v;
+		asm volatile ("mov %%cr3, %0" : "=r" (v) :: );
+		return v;
+	}
+
+	/**
+	 * Return initialized value
+	 *
+	 * \param table  base of targeted translation table
+	 */
+	static access_t init(addr_t const table) {
+		return Pdb::masked(table); }
+};
+
+
 struct Genode::Cpu::Cr4 : Register<64>
 {
 	struct Vme        : Bitfield< 0, 1> { }; /* Virtual-8086 Mode Extensions */
diff --git a/repos/base-hw/src/core/include/spec/x86/fpu.h b/repos/base-hw/src/core/include/spec/x86/fpu.h
new file mode 100644
index 000000000..81c1ef6c3
--- /dev/null
+++ b/repos/base-hw/src/core/include/spec/x86/fpu.h
@@ -0,0 +1,145 @@
+/*
+ * \brief  x86 FPU driver for core
+ * \author Adrian-Ken Rueegsegger
+ * \author Martin stein
+ * \author Reto Buerki
+ * \author Stefan Kalkowski
+ * \date   2016-01-19
+ */
+
+/*
+ * Copyright (C) 2016 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+#ifndef _SPEC__X86__FPU_H_
+#define _SPEC__X86__FPU_H_
+
+/* Genode includes */
+#include <base/stdint.h>
+
+namespace Genode { class Fpu; }
+
+class Genode::Fpu
+{
+	public:
+
+		class Context
+		{
+			private:
+
+				friend class Fpu;
+
+				/*
+				 * FXSAVE area providing storage for x87 FPU, MMX, XMM,
+				 * and MXCSR registers.
+				 *
+				 * For further details see Intel SDM Vol. 2A,
+				 * 'FXSAVE instruction'.
+				 */
+				char _fxsave_area[527];
+
+				/* 16-byte aligned start of FXSAVE area. */
+				char * _start = nullptr;
+
+				Fpu * _fpu = nullptr;
+
+				bool _init()
+				{
+					if (_start) return true;
+
+					_start = ((addr_t)_fxsave_area & 15)
+						? (char *)((addr_t)_fxsave_area & ~15) + 16
+						: _fxsave_area;
+					return false;
+				}
+
+			public:
+
+				~Context() { if (_fpu) _fpu->unset(*this); }
+		} __attribute__((aligned(16)));
+
+	private:
+
+		enum { MXCSR_DEFAULT = 0x1f80 };
+
+		Context * _context = nullptr;
+
+		/**
+		 * Reset FPU
+		 *
+		 * Doesn't check for pending unmasked floating-point
+		 * exceptions and explicitly sets the MXCSR to the
+		 * default value.
+		 */
+		void _reset()
+		{
+			unsigned value = MXCSR_DEFAULT;
+			asm volatile ("fninit");
+			asm volatile ("ldmxcsr %0" : : "m" (value));
+		}
+
+		/**
+		 * Load x87 FPU context
+		 */
+		void _load()
+		{
+			if (!_context->_init()) _reset();
+			else asm volatile ("fxrstor %0" : : "m" (*_context->_start));
+		}
+
+		/**
+		 * Save x87 FPU context
+		 */
+		void _save() {
+			asm volatile ("fxsave %0" : "=m" (*_context->_start)); }
+
+	public:
+
+		/**
+		 * Disable FPU by setting the TS flag in CR0.
+		 */
+		void disable();
+
+		/**
+		 * Enable FPU by clearing the TS flag in CR0.
+		 */
+		void enable() { asm volatile ("clts"); }
+
+		/**
+		 * Initialize all FPU-related CR flags
+		 *
+		 * Initialize FPU with SSE extensions by setting required CR0 and CR4
+		 * bits to configure the FPU environment according to Intel SDM Vol.
+		 * 3A, sections 9.2 and 9.6.
+		 */
+		void init();
+
+		/**
+		 * Returns True if the FPU is enabled.
+		 */
+		bool enabled();
+
+		/**
+		 * Switch to new context
+		 *
+		 * \param context  next FPU context
+		 */
+		void switch_to(Context &context) {
+			if (_context != &context) disable(); }
+
+		/**
+		 * Return whether to retry an FPU instruction after this call
+		 */
+		bool fault(Context &context);
+
+		/**
+		 * Unset FPU context
+		 */
+		void unset(Context &context) {
+			if (_context == &context) _context = nullptr; }
+};
+
+#endif /* _SPEC__X86__FPU_H_ */
diff --git a/repos/base-hw/src/core/kernel/cpu.cc b/repos/base-hw/src/core/kernel/cpu.cc
index f94f67c8f..3c74ba727 100644
--- a/repos/base-hw/src/core/kernel/cpu.cc
+++ b/repos/base-hw/src/core/kernel/cpu.cc
@@ -146,10 +146,8 @@ Cpu_job & Cpu::schedule()
 	assert(quota);
 	_timer->start_one_shot(quota, _id);
 
-	/* switch between lazy state of old and new job */
-	Cpu_lazy_state * const old_state = old_job.lazy_state();
-	Cpu_lazy_state * const new_state = new_job.lazy_state();
-	prepare_proceeding(old_state, new_state);
+	/* switch to new job */
+	switch_to(new_job);
 
 	/* return new job */
 	return new_job;
diff --git a/repos/base-hw/src/core/spec/arm/kernel/thread.cc b/repos/base-hw/src/core/spec/arm/kernel/thread.cc
index a11c5d787..25d09c203 100644
--- a/repos/base-hw/src/core/spec/arm/kernel/thread.cc
+++ b/repos/base-hw/src/core/spec/arm/kernel/thread.cc
@@ -38,7 +38,7 @@ void Thread::exception(unsigned const cpu)
 		_interrupt(cpu);
 		return;
 	case UNDEFINED_INSTRUCTION:
-		if (_cpu->retry_undefined_instr(&_lazy_state)) { return; }
+		if (_cpu->retry_undefined_instr(*this)) { return; }
 		PWRN("%s -> %s: undefined instruction at ip=%p",
 		     pd_label(), label(), (void*)ip);
 		_stop();
diff --git a/repos/base-hw/src/core/spec/cortex_a9/cpu.cc b/repos/base-hw/src/core/spec/cortex_a9/cpu.cc
index b2a974fa2..1b8be0426 100644
--- a/repos/base-hw/src/core/spec/cortex_a9/cpu.cc
+++ b/repos/base-hw/src/core/spec/cortex_a9/cpu.cc
@@ -25,4 +25,3 @@ void Genode::Arm_v7::enable_mmu_and_caches(Kernel::Pd & pd)
 	Cpu::Sctlr::enable_mmu_and_caches();
 	invalidate_branch_predicts();
 }
-
diff --git a/repos/base-hw/src/core/spec/cortex_a9/fpu.cc b/repos/base-hw/src/core/spec/cortex_a9/fpu.cc
new file mode 100644
index 000000000..b49da8c11
--- /dev/null
+++ b/repos/base-hw/src/core/spec/cortex_a9/fpu.cc
@@ -0,0 +1,24 @@
+/*
+ * \brief  CPU driver for core
+ * \author Martin stein
+ * \author Stefan Kalkowski
+ * \date   2016-01-19
+ */
+
+/*
+ * Copyright (C) 2016 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+#include <cpu.h>
+
+void Genode::Fpu::init()
+{
+	Cpu::Cpacr::access_t cpacr = Cpu::Cpacr::read();
+	Cpu::Cpacr::Cp10::set(cpacr, 3);
+	Cpu::Cpacr::Cp11::set(cpacr, 3);
+	Cpu::Cpacr::write(cpacr);
+	_disable();
+}
diff --git a/repos/base-hw/src/core/spec/cortex_a9/kernel/cpu.cc b/repos/base-hw/src/core/spec/cortex_a9/kernel/cpu.cc
index dd6203459..a39fe448e 100644
--- a/repos/base-hw/src/core/spec/cortex_a9/kernel/cpu.cc
+++ b/repos/base-hw/src/core/spec/cortex_a9/kernel/cpu.cc
@@ -114,7 +114,7 @@ void Kernel::Cpu::init(Kernel::Pic &pic, Kernel::Pd & core_pd, Genode::Board & b
 	/* wait for other cores' coherency activation */
 	smp_coherency_enabled.wait_for(NR_OF_CPUS);
 
-	init_advanced_fp_simd();
+	_fpu.init();
 
 	{
 		Lock::Guard guard(data_lock());
diff --git a/repos/base-hw/src/core/spec/imx6/platform_support.cc b/repos/base-hw/src/core/spec/imx6/platform_support.cc
index c06079026..5ce1f46fb 100644
--- a/repos/base-hw/src/core/spec/imx6/platform_support.cc
+++ b/repos/base-hw/src/core/spec/imx6/platform_support.cc
@@ -56,7 +56,7 @@ Native_region * Platform::_core_only_mmio_regions(unsigned const i)
 }
 
 
-Cpu::User_context::User_context() { cpsr = Psr::init_user(); }
+Genode::Arm::User_context::User_context() { cpsr = Psr::init_user(); }
 
 
 bool Cortex_a9::Board::errata(Cortex_a9::Board::Errata err)
diff --git a/repos/base-hw/src/core/spec/panda/platform_support.cc b/repos/base-hw/src/core/spec/panda/platform_support.cc
index 7e6fb290e..2dd72d26b 100644
--- a/repos/base-hw/src/core/spec/panda/platform_support.cc
+++ b/repos/base-hw/src/core/spec/panda/platform_support.cc
@@ -71,7 +71,7 @@ void Cortex_a9::Board::wake_up_all_cpus(void * const ip)
 	             "sev\n");
 }
 
-Cpu::User_context::User_context() { cpsr = Psr::init_user(); }
+Genode::Arm::User_context::User_context() { cpsr = Psr::init_user(); }
 
 
 void Cpu::Actlr::enable_smp() {
diff --git a/repos/base-hw/src/core/spec/pbxa9/platform_support.cc b/repos/base-hw/src/core/spec/pbxa9/platform_support.cc
index 96713237e..982062197 100644
--- a/repos/base-hw/src/core/spec/pbxa9/platform_support.cc
+++ b/repos/base-hw/src/core/spec/pbxa9/platform_support.cc
@@ -59,4 +59,4 @@ Native_region * Platform::_core_only_mmio_regions(unsigned const i)
 }
 
 
-Cpu::User_context::User_context() { cpsr = Psr::init_user(); }
+Genode::Arm::User_context::User_context() { cpsr = Psr::init_user(); }
diff --git a/repos/base-hw/src/core/spec/x86/cpu.cc b/repos/base-hw/src/core/spec/x86/cpu.cc
index d6f27528e..6e8362825 100644
--- a/repos/base-hw/src/core/spec/x86/cpu.cc
+++ b/repos/base-hw/src/core/spec/x86/cpu.cc
@@ -15,24 +15,35 @@
 #include <cpu.h>
 #include <kernel/pd.h>
 
-void Genode::Cpu::_init_fpu()
+Genode::Cpu::Cpu()
 {
-	Cr0::access_t cr0_value = Cr0::read();
-	Cr4::access_t cr4_value = Cr4::read();
+	if (primary_id() == executing_id()) {
+		_idt = new (&_mt_idt) Idt();
+		_idt->setup(Cpu::exception_entry);
 
-	Cr0::Mp::set(cr0_value);
-	Cr0::Em::clear(cr0_value);
-	Cr0::Ts::set(cr0_value);
-	Cr0::Ne::set(cr0_value);
-	Cr0::write(cr0_value);
-
-	Cr4::Osfxsr::set(cr4_value);
-	Cr4::Osxmmexcpt::set(cr4_value);
-	Cr4::write(cr4_value);
+		_tss = new (&_mt_tss) Tss();
+		_tss->load();
+	}
+	_idt->load(Cpu::exception_entry);
+	_tss->setup(Cpu::exception_entry);
 }
 
 
-void Genode::Cpu::_disable_fpu() { Cr0::write(Cr0::read() | Cr0::Ts::bits(1)); }
+void Genode::Cpu::Context::init(addr_t const table, bool core)
+{
+	/* Constants to handle IF, IOPL values */
+	enum {
+		EFLAGS_IF_SET = 1 << 9,
+		EFLAGS_IOPL_3 = 3 << 12,
+	};
 
+	cr3 = Cr3::init(table);
 
-bool Genode::Cpu::_fpu_enabled() { return !Cr0::Ts::get(Cr0::read()); }
+	/*
+	 * Enable interrupts for all threads, set I/O privilege level
+	 * (IOPL) to 3 for core threads to allow UART access.
+	 */
+	eflags = EFLAGS_IF_SET;
+	if (core) eflags |= EFLAGS_IOPL_3;
+	else Gdt::load(Cpu::exception_entry);
+}
diff --git a/repos/base-hw/src/core/spec/x86/fpu.cc b/repos/base-hw/src/core/spec/x86/fpu.cc
new file mode 100644
index 000000000..4bd782f2b
--- /dev/null
+++ b/repos/base-hw/src/core/spec/x86/fpu.cc
@@ -0,0 +1,56 @@
+/*
+ * \brief   FPU implementation specific to x86
+ * \author  Stefan Kalkowski
+ * \date    2016-01-19
+ */
+
+/*
+ * Copyright (C) 2016 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+/* core includes */
+#include <cpu.h>
+
+void Genode::Fpu::init()
+{
+	Cpu::Cr0::access_t cr0_value = Cpu::Cr0::read();
+	Cpu::Cr4::access_t cr4_value = Cpu::Cr4::read();
+
+	Cpu::Cr0::Mp::set(cr0_value);
+	Cpu::Cr0::Em::clear(cr0_value);
+	Cpu::Cr0::Ts::set(cr0_value);
+	Cpu::Cr0::Ne::set(cr0_value);
+	Cpu::Cr0::write(cr0_value);
+
+	Cpu::Cr4::Osfxsr::set(cr4_value);
+	Cpu::Cr4::Osxmmexcpt::set(cr4_value);
+	Cpu::Cr4::write(cr4_value);
+}
+
+
+void Genode::Fpu::disable() {
+	Cpu::Cr0::write(Cpu::Cr0::read() | Cpu::Cr0::Ts::bits(1)); }
+
+
+bool Genode::Fpu::enabled() { return !Cpu::Cr0::Ts::get(Cpu::Cr0::read()); }
+
+
+bool Genode::Fpu::fault(Context &context)
+{
+	if (enabled()) return false;
+
+	enable();
+	if (_context == &context) return true;
+
+	if (_context) {
+		_save();
+		_context->_fpu = nullptr;
+	}
+	_context = &context;
+	_context->_fpu = this;
+	_load();
+	return true;
+}
diff --git a/repos/base-hw/src/core/spec/x86/kernel/cpu.cc b/repos/base-hw/src/core/spec/x86/kernel/cpu.cc
index 84d363646..cc1e5cabd 100644
--- a/repos/base-hw/src/core/spec/x86/kernel/cpu.cc
+++ b/repos/base-hw/src/core/spec/x86/kernel/cpu.cc
@@ -33,7 +33,7 @@ void Kernel::Cpu::init(Pic &pic, Kernel::Pd &core_pd, Genode::Board&)
 {
 	Timer::disable_pit();
 
-	_init_fpu();
+	fpu().init();
 
 	/*
 	 * Please do not remove the PINF(), because the serial constructor requires
diff --git a/repos/base-hw/src/core/spec/x86/kernel/thread_exception.cc b/repos/base-hw/src/core/spec/x86/kernel/thread_exception.cc
index c479e570e..5a2c3e392 100644
--- a/repos/base-hw/src/core/spec/x86/kernel/thread_exception.cc
+++ b/repos/base-hw/src/core/spec/x86/kernel/thread_exception.cc
@@ -25,7 +25,7 @@ void Thread::exception(unsigned const cpu)
 		_mmu_exception();
 		return;
 	case NO_MATH_COPROC:
-		if (_cpu->retry_fpu_instr(&_lazy_state)) { return; }
+		if (_cpu->fpu().fault(*this)) { return; }
 		PWRN("%s -> %s: FPU error", pd_label(), label());
 		_stop();
 		return;
diff --git a/repos/base-hw/src/core/spec/x86_64/muen/kernel/thread_exception.cc b/repos/base-hw/src/core/spec/x86_64/muen/kernel/thread_exception.cc
index bb19b7491..8c4326e79 100644
--- a/repos/base-hw/src/core/spec/x86_64/muen/kernel/thread_exception.cc
+++ b/repos/base-hw/src/core/spec/x86_64/muen/kernel/thread_exception.cc
@@ -25,7 +25,7 @@ void Thread::exception(unsigned const cpu)
 		_mmu_exception();
 		return;
 	case NO_MATH_COPROC:
-		if (_cpu->retry_fpu_instr(&_lazy_state)) { return; }
+		if (_cpu->fpu().fault(*this)) { return; }
 		PWRN("%s -> %s: FPU error", pd_label(), label());
 		_stop();
 		return;
diff --git a/repos/base-hw/src/core/spec/zynq/platform_support.cc b/repos/base-hw/src/core/spec/zynq/platform_support.cc
index 5417cd5ee..e84d9db34 100644
--- a/repos/base-hw/src/core/spec/zynq/platform_support.cc
+++ b/repos/base-hw/src/core/spec/zynq/platform_support.cc
@@ -64,7 +64,7 @@ Native_region * Platform::_core_only_mmio_regions(unsigned const i)
 }
 
 
-Cpu::User_context::User_context() { cpsr = Psr::init_user(); }
+Genode::Arm::User_context::User_context() { cpsr = Psr::init_user(); }
 
 
 bool Cortex_a9::Board::errata(Cortex_a9::Board::Errata err) {