diff --git a/repos/base-hw/src/core/include/spec/x86/cpu.h b/repos/base-hw/src/core/include/spec/x86/cpu.h
index 51fc9ab8d..1b1bd8ac2 100644
--- a/repos/base-hw/src/core/include/spec/x86/cpu.h
+++ b/repos/base-hw/src/core/include/spec/x86/cpu.h
@@ -21,6 +21,7 @@
 #include <gdt.h>
 #include <idt.h>
 #include <tss.h>
+#include <timer.h>
 
 extern int _mt_idt;
 extern int _mt_tss;
@@ -264,8 +265,8 @@ class Genode::Cpu
 		/**
 		 * Configure this module appropriately for the first kernel run
 		 */
-		static void init_phys_kernel()
-		{ }
+		static void init_phys_kernel() {
+			Timer::disable_pit(); };
 
 		/**
 		 * Finish all previous data transfers
diff --git a/repos/base-hw/src/core/include/spec/x86/timer.h b/repos/base-hw/src/core/include/spec/x86/timer.h
index 67a81cf4e..31ee05dfb 100644
--- a/repos/base-hw/src/core/include/spec/x86/timer.h
+++ b/repos/base-hw/src/core/include/spec/x86/timer.h
@@ -14,47 +14,119 @@
 #ifndef _TIMER_H_
 #define _TIMER_H_
 
+#include <util/mmio.h>
 #include <base/stdint.h>
 #include <base/printf.h>
-
+#include <port_io.h>
+#include <board.h>
 
 namespace Genode
 {
 	/**
-	 * Timer driver for core
-	 *
-	 * Timer channel 0 apparently doesn't work on the RPI, so we use channel 1
+	 * LAPIC-based timer driver for core
 	 */
 	class Timer;
 }
 
-class Genode::Timer
+class Genode::Timer : public Mmio
 {
+	private:
+
+		enum {
+			/* PIT constants */
+			PIT_TICK_RATE  = 1193182ul,
+			PIT_SLEEP_MS   = 50,
+			PIT_SLEEP_TICS = (PIT_TICK_RATE / 1000) * PIT_SLEEP_MS,
+			PIT_CH0_DATA   = 0x40,
+			PIT_CH2_DATA   = 0x42,
+			PIT_CH2_GATE   = 0x61,
+			PIT_MODE       = 0x43,
+		};
+
+		/* Timer registers */
+		struct Tmr_lvt : Register<0x320, 32>
+		{
+			struct Vector     : Bitfield<0,  8> { };
+			struct Delivery   : Bitfield<8,  3> { };
+			struct Mask       : Bitfield<16, 1> { };
+			struct Timer_mode : Bitfield<17, 2> { };
+		};
+		struct Tmr_initial : Register <0x380, 32> { };
+		struct Tmr_current : Register <0x390, 32> { };
+
+		uint32_t _tics_per_ms = 0;
+
+		/* Measure LAPIC timer frequency using PIT channel 2 */
+		uint32_t pit_calc_timer_freq(void)
+		{
+			uint32_t t_start, t_end;
+
+			/* Set channel gate high and disable speaker */
+			outb(PIT_CH2_GATE, (inb(0x61) & ~0x02) | 0x01);
+
+			/* Set timer counter (mode 0, binary count) */
+			outb(PIT_MODE, 0xb0);
+			outb(PIT_CH2_DATA, PIT_SLEEP_TICS & 0xff);
+			outb(PIT_CH2_DATA, PIT_SLEEP_TICS >> 8);
+
+			write<Tmr_initial>(~0U);
+
+			t_start = read<Tmr_current>();
+			while ((inb(PIT_CH2_GATE) & 0x20) == 0)
+			{
+				asm volatile("pause" : : : "memory");
+			}
+			t_end = read<Tmr_current>();
+
+			write<Tmr_initial>(0);
+
+			return (t_start - t_end) / PIT_SLEEP_MS;
+		}
+
 	public:
 
-		Timer() { }
+		Timer() : Mmio(Board::MMIO_LAPIC_BASE)
+		{
+			/* Enable LAPIC timer in one-shot mode */
+			write<Tmr_lvt::Vector>(Board::TIMER_VECTOR_KERNEL);
+			write<Tmr_lvt::Delivery>(0);
+			write<Tmr_lvt::Mask>(0);
+			write<Tmr_lvt::Timer_mode>(0);
+
+			/* Calculate timer frequency */
+			_tics_per_ms = pit_calc_timer_freq();
+			PINF("LAPIC: timer frequency %u kHz", _tics_per_ms);
+		}
+
+		/**
+		 * Disable PIT timer channel. This is necessary since BIOS sets up
+		 * channel 0 to fire periodically.
+		 */
+		static void disable_pit(void)
+		{
+			outb(PIT_MODE, 0x30);
+			outb(PIT_CH0_DATA, 0);
+			outb(PIT_CH0_DATA, 0);
+		}
 
 		static unsigned interrupt_id(int)
 		{
-			PDBG("not implemented");
-			return 0;
+			return Board::TIMER_VECTOR_KERNEL;
 		}
 
 		inline void start_one_shot(uint32_t const tics, unsigned)
 		{
-			PDBG("not implemented");
+			write<Tmr_initial>(tics);
 		}
 
-		static uint32_t ms_to_tics(unsigned const ms)
+		uint32_t ms_to_tics(unsigned const ms)
 		{
-			PDBG("not implemented");
-			return 10000;
+			return ms * _tics_per_ms;
 		}
 
 		unsigned value(unsigned)
 		{
-			PDBG("not implemented");
-			return 0;
+			return read<Tmr_current>();
 		}
 };