diff --git a/repos/base-hw/include/kernel/interface.h b/repos/base-hw/include/kernel/interface.h
index a99db6997..8fc169e44 100644
--- a/repos/base-hw/include/kernel/interface.h
+++ b/repos/base-hw/include/kernel/interface.h
@@ -40,7 +40,6 @@ namespace Kernel
 	constexpr Call_arg call_id_ack_cap()                  { return 14; }
 	constexpr Call_arg call_id_delete_cap()               { return 15; }
 	constexpr Call_arg call_id_timeout()                  { return 16; }
-	constexpr Call_arg call_id_timeout_age_us()           { return 17; }
 	constexpr Call_arg call_id_timeout_max_us()           { return 18; }
 	constexpr Call_arg call_id_time()                     { return 19; }
 
@@ -80,6 +79,8 @@ namespace Kernel
 	              Call_arg arg_4,
 	              Call_arg arg_5);
 
+	Call_ret_64 call64(Call_arg arg_0);
+
 
 	/**
 	 * Install timeout for calling thread
@@ -90,23 +91,12 @@ namespace Kernel
 	 * This call always overwrites the last timeout installed by the thread
 	 * if any.
 	 */
-	inline int timeout(time_t const duration_us, capid_t const sigid)
+	inline int timeout(timeout_t const duration_us, capid_t const sigid)
 	{
 		return call(call_id_timeout(), duration_us, sigid);
 	}
 
 
-	/**
-	 * Return time in microseconds since the caller installed its last timeout
-	 *
-	 * Must not be called if the installation is older than 'timeout_max_us'.
-	 */
-	inline time_t timeout_age_us()
-	{
-		return call(call_id_timeout_age_us());
-	}
-
-
 	/**
 	 * Return value of a free-running, uniform counter
 	 *
@@ -115,7 +105,7 @@ namespace Kernel
 	 */
 	inline time_t time()
 	{
-		return call(call_id_time());
+		return call64(call_id_time());
 	}
 
 
@@ -127,7 +117,7 @@ namespace Kernel
 	 */
 	inline time_t timeout_max_us()
 	{
-		return call(call_id_timeout_max_us());
+		return call64(call_id_timeout_max_us());
 	}
 
 
diff --git a/repos/base-hw/include/kernel/types.h b/repos/base-hw/include/kernel/types.h
index b2cb9c20f..a07a052c9 100644
--- a/repos/base-hw/include/kernel/types.h
+++ b/repos/base-hw/include/kernel/types.h
@@ -20,10 +20,11 @@
 
 namespace Kernel
 {
-	using addr_t  = Genode::addr_t;
-	using size_t  = Genode::size_t;
-	using capid_t = Genode::uint16_t;
-	using time_t  = unsigned long;
+	using addr_t    = Genode::addr_t;
+	using size_t    = Genode::size_t;
+	using capid_t   = Genode::uint16_t;
+	using time_t    = Genode::uint64_t;
+	using timeout_t = Genode::uint32_t;
 
 	constexpr capid_t cap_id_invalid() { return 0; }
 }
diff --git a/repos/base-hw/include/spec/arm/kernel/interface_support.h b/repos/base-hw/include/spec/arm/kernel/interface_support.h
index 7286f1dfc..3ffca0f4c 100644
--- a/repos/base-hw/include/spec/arm/kernel/interface_support.h
+++ b/repos/base-hw/include/spec/arm/kernel/interface_support.h
@@ -21,6 +21,7 @@ namespace Kernel
 {
 	typedef Genode::uint32_t Call_arg;
 	typedef Genode::uint32_t Call_ret;
+	typedef Genode::uint64_t Call_ret_64;
 }
 
 #endif /* _INCLUDE__SPEC__ARM__KERNEL__INTERFACE_SUPPORT_H_ */
diff --git a/repos/base-hw/include/spec/riscv/kernel/interface_support.h b/repos/base-hw/include/spec/riscv/kernel/interface_support.h
index 7d9781cb6..0fe140d76 100644
--- a/repos/base-hw/include/spec/riscv/kernel/interface_support.h
+++ b/repos/base-hw/include/spec/riscv/kernel/interface_support.h
@@ -21,6 +21,7 @@ namespace Kernel
 {
 	typedef Genode::uint64_t Call_arg;
 	typedef Genode::uint64_t Call_ret;
+	typedef Genode::uint64_t Call_ret_64;
 }
 
 #endif /* _KERNEL__INTERFACE_SUPPORT_H_ */
diff --git a/repos/base-hw/include/spec/x86_64/kernel/interface_support.h b/repos/base-hw/include/spec/x86_64/kernel/interface_support.h
index f1bf8cb13..a8a2a4835 100644
--- a/repos/base-hw/include/spec/x86_64/kernel/interface_support.h
+++ b/repos/base-hw/include/spec/x86_64/kernel/interface_support.h
@@ -21,6 +21,7 @@ namespace Kernel
 {
 	typedef Genode::uint64_t Call_arg;
 	typedef Genode::uint64_t Call_ret;
+	typedef Genode::uint64_t Call_ret_64;
 }
 
 #endif /* _INCLUDE__SPEC__X86_64__KERNEL__INTERFACE_SUPPORT_H_ */
diff --git a/repos/base-hw/src/core/kernel/cpu.cc b/repos/base-hw/src/core/kernel/cpu.cc
index e8bcf8287..b03739df1 100644
--- a/repos/base-hw/src/core/kernel/cpu.cc
+++ b/repos/base-hw/src/core/kernel/cpu.cc
@@ -34,27 +34,6 @@ Kernel::Cpu_pool &Kernel::cpu_pool() { return *unmanaged_singleton<Cpu_pool>();
  ** Cpu_job **
  *************/
 
-time_t Cpu_job::timeout_age_us(Timeout const * const timeout) const
-{
-	return _cpu->timeout_age_us(timeout);
-}
-
-
-time_t Cpu_job::time() const { return _cpu->time(); }
-
-
-time_t Cpu_job::timeout_max_us() const
-{
-	return _cpu->timeout_max_us();
-}
-
-
-void Cpu_job::timeout(Timeout * const timeout, time_t const us)
-{
-	_cpu->set_timeout(timeout, us);
-}
-
-
 void Cpu_job::_activate_own_share() { _cpu->schedule(this); }
 
 
@@ -134,17 +113,6 @@ Cpu::Idle_thread::Idle_thread(Cpu &cpu)
 }
 
 
-void Cpu::set_timeout(Timeout * const timeout, time_t const duration_us) {
-	_timer.set_timeout(timeout, _timer.us_to_ticks(duration_us)); }
-
-
-time_t Cpu::timeout_age_us(Timeout const * const timeout) const {
-	return _timer.timeout_age_us(timeout); }
-
-
-time_t Cpu::timeout_max_us() const { return _timer.timeout_max_us(); }
-
-
 void Cpu::schedule(Job * const job)
 {
 	if (_id == executing_id()) { _scheduler.ready(&job->share()); }
@@ -168,11 +136,10 @@ Cpu_job & Cpu::schedule()
 	old_job.exception(*this);
 
 	if (_scheduler.need_to_schedule()) {
-		time_t quota = _timer.update_time();
 		_timer.process_timeouts();
-		_scheduler.update(quota);
-		quota = _scheduler.head_quota();
-		_timer.set_timeout(this, quota);
+		_scheduler.update(_timer.time());
+		time_t t = _scheduler.head_quota();
+		_timer.set_timeout(this, t);
 		_timer.schedule_timeout();
 	}
 
diff --git a/repos/base-hw/src/core/kernel/cpu.h b/repos/base-hw/src/core/kernel/cpu.h
index 4ddac6b3e..dc6141d42 100644
--- a/repos/base-hw/src/core/kernel/cpu.h
+++ b/repos/base-hw/src/core/kernel/cpu.h
@@ -157,13 +157,7 @@ class Kernel::Cpu : public Genode::Cpu, private Irq::Pool, private Timeout
 		 */
 		Cpu_job& schedule();
 
-		void set_timeout(Timeout * const timeout, time_t const duration_us);
-
-		time_t timeout_age_us(Timeout const * const timeout) const;
-
-		time_t timeout_max_us() const;
-
-		time_t time() const { return _timer.time(); }
+		Timer & timer() { return _timer; }
 
 		addr_t stack_start();
 
@@ -176,10 +170,6 @@ class Kernel::Cpu : public Genode::Cpu, private Irq::Pool, private Timeout
 		unsigned id() const { return _id; }
 		Cpu_scheduler &scheduler() { return _scheduler; }
 
-		time_t us_to_ticks(time_t const us) const { return _timer.us_to_ticks(us); };
-
-		unsigned timer_interrupt_id() const { return _timer.interrupt_id(); }
-
 		Irq::Pool &irq_pool() { return *this; }
 
 		Inter_processor_work_list & work_list() {
diff --git a/repos/base-hw/src/core/kernel/cpu_context.h b/repos/base-hw/src/core/kernel/cpu_context.h
index 20f9939c3..aaf5384a5 100644
--- a/repos/base-hw/src/core/kernel/cpu_context.h
+++ b/repos/base-hw/src/core/kernel/cpu_context.h
@@ -112,13 +112,6 @@ class Kernel::Cpu_job : private Cpu_share
 		 */
 		bool own_share_active() { return Cpu_share::ready(); }
 
-		void timeout(Timeout * const timeout, time_t const duration_us);
-
-		time_t timeout_age_us(Timeout const * const timeout) const;
-
-		time_t timeout_max_us() const;
-
-		time_t time() const;
 
 		/***************
 		 ** Accessors **
diff --git a/repos/base-hw/src/core/kernel/cpu_scheduler.cc b/repos/base-hw/src/core/kernel/cpu_scheduler.cc
index 1a378f924..c8ef27c02 100644
--- a/repos/base-hw/src/core/kernel/cpu_scheduler.cc
+++ b/repos/base-hw/src/core/kernel/cpu_scheduler.cc
@@ -127,16 +127,18 @@ void Cpu_scheduler::_quota_adaption(Share * const s, unsigned const q)
 }
 
 
-void Cpu_scheduler::update(unsigned q)
+void Cpu_scheduler::update(time_t time)
 {
+	unsigned duration = (unsigned) (time - _last_time);
+	_last_time        = time;
 	_need_to_schedule = false;
 
 	/* do not detract the quota if the head context was removed even now */
 	if (_head) {
-		unsigned const r = _trim_consumption(q);
+		unsigned const r = _trim_consumption(duration);
 		if (_head_claims) { _head_claimed(r); }
 		else              { _head_filled(r);  }
-		_consumed(q);
+		_consumed(duration);
 	}
 
 	if (_claim_for_head()) { return; }
diff --git a/repos/base-hw/src/core/kernel/cpu_scheduler.h b/repos/base-hw/src/core/kernel/cpu_scheduler.h
index 8d53bc0d2..d6ec38345 100644
--- a/repos/base-hw/src/core/kernel/cpu_scheduler.h
+++ b/repos/base-hw/src/core/kernel/cpu_scheduler.h
@@ -133,6 +133,7 @@ class Kernel::Cpu_scheduler
 		unsigned       _residual;
 		unsigned const _fill;
 		bool           _need_to_schedule { true };
+		time_t         _last_time { 0 };
 
 		template <typename F> void _for_each_prio(F f) {
 			for (signed p = Prio::MAX; p > Prio::MIN - 1; p--) { f(p); } }
@@ -184,9 +185,9 @@ class Kernel::Cpu_scheduler
 		void timeout()          { _need_to_schedule = true; }
 
 		/**
-		 * Update head according to the consumption of quota 'q'
+		 * Update head according to the consumed time
 		 */
-		void update(unsigned q);
+		void update(time_t time);
 
 		/**
 		 * Set 's1' ready and return wether this outdates current head
diff --git a/repos/base-hw/src/core/kernel/thread.cc b/repos/base-hw/src/core/kernel/thread.cc
index 5ae9c29a7..deb17e870 100644
--- a/repos/base-hw/src/core/kernel/thread.cc
+++ b/repos/base-hw/src/core/kernel/thread.cc
@@ -187,7 +187,7 @@ size_t Thread::_core_to_kernel_quota(size_t const quota) const
 {
 	using Genode::Cpu_session;
 	using Genode::sizet_arithm_t;
-	size_t const ticks = _cpu->us_to_ticks(Kernel::cpu_quota_us);
+	size_t const ticks = _cpu->timer().us_to_ticks(Kernel::cpu_quota_us);
 	return Cpu_session::quota_lim_downscale<sizet_arithm_t>(quota, ticks);
 }
 
@@ -370,19 +370,22 @@ void Thread::_call_await_request_msg()
 
 void Thread::_call_timeout()
 {
+	Timer & t = _cpu->timer();
 	_timeout_sigid = user_arg_2();
-	Cpu_job::timeout(this, user_arg_1());
+	t.set_timeout(this, t.us_to_ticks(user_arg_1()));
 }
 
 
-void Thread::_call_timeout_age_us()
-{
-	user_arg_0(Cpu_job::timeout_age_us(this));
-}
-
 void Thread::_call_timeout_max_us()
 {
-	user_arg_0(Cpu_job::timeout_max_us());
+	user_ret_time(_cpu->timer().timeout_max_us());
+}
+
+
+void Thread::_call_time()
+{
+	Timer & t = _cpu->timer();
+	user_ret_time(t.ticks_to_us(t.time()));
 }
 
 
@@ -634,9 +637,8 @@ void Thread::_call()
 	case call_id_ack_cap():                  _call_ack_cap(); return;
 	case call_id_delete_cap():               _call_delete_cap(); return;
 	case call_id_timeout():                  _call_timeout(); return;
-	case call_id_timeout_age_us():           _call_timeout_age_us(); return;
 	case call_id_timeout_max_us():           _call_timeout_max_us(); return;
-	case call_id_time():                     user_arg_0(Cpu_job::time()); return;
+	case call_id_time():                     _call_time(); return;
 	default:
 		/* check wether this is a core thread */
 		if (!_core) {
diff --git a/repos/base-hw/src/core/kernel/thread.h b/repos/base-hw/src/core/kernel/thread.h
index fe351147e..e1ba29060 100644
--- a/repos/base-hw/src/core/kernel/thread.h
+++ b/repos/base-hw/src/core/kernel/thread.h
@@ -232,8 +232,8 @@ class Kernel::Thread
 		void _call_ack_cap();
 		void _call_delete_cap();
 		void _call_timeout();
-		void _call_timeout_age_us();
 		void _call_timeout_max_us();
+		void _call_time();
 
 		template <typename T, typename... ARGS>
 		void _call_new(ARGS &&... args)
@@ -307,6 +307,8 @@ class Kernel::Thread
 		 ** Support for syscalls **
 		 **************************/
 
+		void user_ret_time(Kernel::time_t const t);
+
 		void user_arg_0(Kernel::Call_arg const arg);
 		void user_arg_1(Kernel::Call_arg const arg);
 		void user_arg_2(Kernel::Call_arg const arg);
diff --git a/repos/base-hw/src/core/kernel/timer.cc b/repos/base-hw/src/core/kernel/timer.cc
index d9f26e0df..eff51b0ec 100644
--- a/repos/base-hw/src/core/kernel/timer.cc
+++ b/repos/base-hw/src/core/kernel/timer.cc
@@ -27,22 +27,9 @@ Timer::Irq::Irq(unsigned id, Cpu &cpu)
 : Kernel::Irq(id, cpu.irq_pool()), _cpu(cpu) {}
 
 
-time_t Timer::timeout_age_us(Timeout const * const timeout) const
-{
-	time_t const age = (time_t)_time - timeout->_start;
-	return _ticks_to_us(age);
-}
-
-
 time_t Timer::timeout_max_us() const
 {
-	return _ticks_to_us(_max_value());
-}
-
-
-bool Timer::_time_overflow(time_t const duration) const
-{
-	return duration > ~(time_t)0 - _time;
+	return ticks_to_us(_max_value());
 }
 
 
@@ -53,70 +40,36 @@ void Timer::set_timeout(Timeout * const timeout, time_t const duration)
 	 * result of an update.
 	 */
 	if (timeout->_listed) {
-		_timeout_list[timeout->_end_period].remove(timeout);
+		_timeout_list.remove(timeout);
 	} else {
 		timeout->_listed = true; }
 
 	/* set timeout parameters */
-	timeout->_start      = _time;
-	timeout->_end        = _time + duration;
-	timeout->_end_period = _time_overflow(duration) ? !_time_period :
-	                                                   _time_period;
+	timeout->_end = time() + duration;
 
 	/*
 	 * Insert timeout. Timeouts are ordered ascending according to their end
 	 * time to be able to quickly determine the nearest timeout.
 	 */
-	Genode::List<Timeout> & list = _timeout_list[timeout->_end_period];
 	Timeout * t1 = 0;
-	for (Timeout * t2 = list.first(); t2 && t2->_end < timeout->_end;
+	for (Timeout * t2 = _timeout_list.first();
+	     t2 && t2->_end < timeout->_end;
 	     t1 = t2, t2 = t2->next()) { }
 
-	list.insert(timeout, t1);
+	_timeout_list.insert(timeout, t1);
 }
 
 
 void Timer::schedule_timeout()
 {
 	/* get the timeout with the nearest end time */
-	Timeout * timeout = _timeout_list[_time_period].first();
-	if (!timeout) {
-		timeout = _timeout_list[!_time_period].first();
-		assert(timeout);
-	}
+	Timeout * timeout = _timeout_list.first();
+	assert(timeout);
+
 	/* install timeout at timer hardware */
-	time_t const duration = (time_t)timeout->_end - _time;
-	_last_timeout_duration = duration;
-	_start_one_shot(duration);
-}
-
-
-time_t Timer::update_time()
-{
-	/* determine how much time has passed */
-	time_t const old_value = _last_timeout_duration;
-	time_t const new_value = _value();
-	time_t const duration  = old_value > new_value ? old_value - new_value : 1;
-
-	/* is this the end of the current period? */
-	if (_time_overflow(duration)) {
-
-		/* flush all timeouts of current period */
-		Genode::List<Timeout> & list = _timeout_list[_time_period];
-		while (true) {
-			Timeout * const timeout = list.first();
-			if (!timeout) { break; }
-			list.remove(timeout);
-			timeout->_listed = false;
-			timeout->timeout_triggered();
-		}
-		/* switch to next period */
-		_time_period = !_time_period;
-
-	}
-	/* update time */
-	_time += duration;
-	return duration;
+	_time += _duration();
+	_last_timeout_duration = (timeout->_end > _time) ? timeout->_end - _time : 1;
+	_start_one_shot(_last_timeout_duration);
 }
 
 
@@ -124,15 +77,13 @@ void Timer::process_timeouts()
 {
 	/*
 	 * Walk through timeouts until the first whose end time is in the future.
-	 * Consider only the current periods list as all timeouts of the next
-	 * period must be in the future.
 	 */
-	Genode::List<Timeout> & list = _timeout_list[_time_period];
+	time_t t = time();
 	while (true) {
-		Timeout * const timeout = list.first();
+		Timeout * const timeout = _timeout_list.first();
 		if (!timeout) { break; }
-		if (timeout->_end > _time) { break; }
-		list.remove(timeout);
+		if (timeout->_end > t) { break; }
+		_timeout_list.remove(timeout);
 		timeout->_listed = false;
 		timeout->timeout_triggered();
 	}
@@ -140,13 +91,14 @@ void Timer::process_timeouts()
 
 
 Timer::Timer(Cpu & cpu)
-: _driver(cpu.id()), _irq(interrupt_id(), cpu)
+: _driver(cpu.id()), _irq(interrupt_id(), cpu),
+  _last_timeout_duration(_max_value())
 {
 	/*
 	 * The timer frequency should allow a good accuracy on the smallest
 	 * timeout syscall value (1 us).
 	 */
-	assert(_ticks_to_us(1) < 1 || _ticks_to_us(_max_value()) == _max_value());
+	assert(ticks_to_us(1) < 1 || ticks_to_us(_max_value()) == _max_value());
 
 	/*
 	 * The maximum measurable timeout is also the maximum age of a timeout
@@ -158,5 +110,5 @@ Timer::Timer(Cpu & cpu)
 	 * said, the maximum timeout should be at least two times the super
 	 * period).
 	 */
-	assert(_ticks_to_us(_max_value()) > 2 * cpu_quota_us);
+	assert(ticks_to_us(_max_value()) > 2 * cpu_quota_us);
 }
diff --git a/repos/base-hw/src/core/kernel/timer.h b/repos/base-hw/src/core/kernel/timer.h
index 8ea8c7004..4116c8750 100644
--- a/repos/base-hw/src/core/kernel/timer.h
+++ b/repos/base-hw/src/core/kernel/timer.h
@@ -42,9 +42,7 @@ class Kernel::Timeout : Genode::List<Timeout>::Element
 	private:
 
 		bool   _listed     = false;
-		time_t _start      = 0;
 		time_t _end        = 0;
-		bool   _end_period = false;
 
 	public:
 
@@ -81,35 +79,30 @@ class Kernel::Timer
 		Driver                _driver;
 		Irq                   _irq;
 		time_t                _time = 0;
-		bool                  _time_period = false;
-		Genode::List<Timeout> _timeout_list[2];
-		time_t                _last_timeout_duration = 0;
-
-		bool _time_overflow(time_t const duration) const;
+		time_t                _last_timeout_duration;
+		Genode::List<Timeout> _timeout_list {};
 
 		void _start_one_shot(time_t const ticks);
 
-		time_t _ticks_to_us(time_t const ticks) const;
-
 		time_t _value();
 
 		time_t _max_value() const;
 
+		time_t _duration() const;
+
 	public:
 
 		Timer(Cpu & cpu);
 
 		void schedule_timeout();
 
-		time_t update_time();
-
 		void process_timeouts();
 
 		void set_timeout(Timeout * const timeout, time_t const duration);
 
 		time_t us_to_ticks(time_t const us) const;
 
-		time_t timeout_age_us(Timeout const * const timeout) const;
+		time_t ticks_to_us(time_t const ticks) const;
 
 		time_t timeout_max_us() const;
 
@@ -117,7 +110,7 @@ class Kernel::Timer
 
 		static void init_cpu_local();
 
-		time_t time() const { return _time; }
+		time_t time() const { return _time + _duration(); }
 };
 
 #endif /* _CORE__KERNEL__TIMER_H_ */
diff --git a/repos/base-hw/src/core/platform.cc b/repos/base-hw/src/core/platform.cc
index 526448e9c..814758472 100644
--- a/repos/base-hw/src/core/platform.cc
+++ b/repos/base-hw/src/core/platform.cc
@@ -117,8 +117,8 @@ Platform::Platform()
 	/* make all non-kernel interrupts available to the interrupt allocator */
 	for (unsigned i = 0; i < Kernel::Pic::NR_OF_IRQ; i++) {
 		bool kernel_resource = false;
-		Kernel::cpu_pool().for_each_cpu([&] (Kernel::Cpu const &cpu) {
-			if (i == cpu.timer_interrupt_id()) {
+		Kernel::cpu_pool().for_each_cpu([&] (Kernel::Cpu & cpu) {
+			if (i == cpu.timer().interrupt_id()) {
 				kernel_resource = true;
 			}
 		});
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 79126e9b3..a2b6fb2ec 100644
--- a/repos/base-hw/src/core/spec/arm/kernel/thread.cc
+++ b/repos/base-hw/src/core/spec/arm/kernel/thread.cc
@@ -120,6 +120,12 @@ void Thread::proceed(Cpu & cpu)
 }
 
 
+void Thread::user_ret_time(Kernel::time_t const t)
+{
+	regs->r0 = t >> 32UL;
+	regs->r1 = t & ~0UL;
+}
+
 void Thread::user_arg_0(Kernel::Call_arg const arg) { regs->r0 = arg; }
 void Thread::user_arg_1(Kernel::Call_arg const arg) { regs->r1 = arg; }
 void Thread::user_arg_2(Kernel::Call_arg const arg) { regs->r2 = arg; }
diff --git a/repos/base-hw/src/core/spec/cortex_a9/timer.cc b/repos/base-hw/src/core/spec/cortex_a9/timer.cc
index f211748a5..6e0a7ce49 100644
--- a/repos/base-hw/src/core/spec/cortex_a9/timer.cc
+++ b/repos/base-hw/src/core/spec/cortex_a9/timer.cc
@@ -16,6 +16,7 @@
 #include <drivers/timer/util.h>
 
 /* core includes */
+#include <kernel/cpu.h>
 #include <kernel/timer.h>
 #include <platform.h>
 
@@ -26,30 +27,36 @@ using namespace Kernel;
 Timer_driver::Timer_driver(unsigned)
 : Mmio(Platform::mmio_to_virt(Board::Cpu_mmio::PRIVATE_TIMER_MMIO_BASE))
 {
-	static_assert(TICS_PER_MS >= (unsigned)TIMER_MIN_TICKS_PER_MS,
-	              "Bad TICS_PER_MS value");
-	write<Control::Timer_enable>(0);
+	enum { PRESCALER = Board::CORTEX_A9_PRIVATE_TIMER_DIV - 1 };
+
+	static_assert((TICS_PER_MS >= 1000) /*&&
+	              (TICS_PER_US * 1000000 *
+	               Board::CORTEX_A9_PRIVATE_TIMER_DIV) ==
+	               Board::CORTEX_A9_PRIVATE_TIMER_CLK*/,
+	              "Bad TICS_PER_US value");
+
+	write<Load>(0xffffffff);
+	Control::access_t control = 0;
+	Control::Irq_enable::set(control, 1);
+	Control::Prescaler::set(control, PRESCALER);
+	Control::Auto_reload::set(control, 1);
+	Control::Timer_enable::set(control, 1);
+	write<Control>(control);
 }
 
 
 void Timer::_start_one_shot(time_t const ticks)
 {
-	enum { PRESCALER = Board::CORTEX_A9_PRIVATE_TIMER_DIV - 1 };
-
-	/* reset timer */
+	/*
+	 * First unset the interrupt flag,
+	 * otherwise if the tick is small enough, we loose an interrupt
+	 */
 	_driver.write<Driver::Interrupt_status::Event>(1);
-	Driver::Control::access_t control = 0;
-	Driver::Control::Irq_enable::set(control, 1);
-	Driver::Control::Prescaler::set(control, PRESCALER);
-	_driver.write<Driver::Control>(control);
-
-	/* load timer and start decrementing */
-	_driver.write<Driver::Load>(ticks);
-	_driver.write<Driver::Control::Timer_enable>(1);
+	_driver.write<Driver::Counter>(ticks);
 }
 
 
-time_t Timer::_ticks_to_us(time_t const ticks) const {
+time_t Timer::ticks_to_us(time_t const ticks) const {
 	return timer_ticks_to_us(ticks, Driver::TICS_PER_MS); }
 
 
@@ -61,9 +68,14 @@ time_t Timer::us_to_ticks(time_t const us) const {
 	return (us / 1000) * Driver::TICS_PER_MS; }
 
 
-time_t Timer::_value() {
-	return _driver.read<Driver::Counter>(); }
+time_t Timer::_duration() const
+{
+	Driver::Counter::access_t last = _last_timeout_duration;
+	Driver::Counter::access_t cnt  = _driver.read<Driver::Counter>();
+	Driver::Counter::access_t ret  = (_driver.read<Driver::Interrupt_status::Event>())
+		? _max_value() - cnt + last : last - cnt;
+	return ret;
+}
 
 
-time_t Timer::_max_value() const {
-	return (Driver::Load::access_t)~0; }
+time_t Timer::_max_value() const { return 0xfffffffe; }
diff --git a/repos/base-hw/src/core/spec/cortex_a9/timer_driver.h b/repos/base-hw/src/core/spec/cortex_a9/timer_driver.h
index 99f341a0d..540928265 100644
--- a/repos/base-hw/src/core/spec/cortex_a9/timer_driver.h
+++ b/repos/base-hw/src/core/spec/cortex_a9/timer_driver.h
@@ -49,6 +49,7 @@ struct Kernel::Timer_driver : Genode::Mmio
 	struct Control : Register<0x8, 32>
 	{
 		struct Timer_enable : Bitfield<0,1> { }; /* enable counting */
+		struct Auto_reload  : Bitfield<1,1> { };
 		struct Irq_enable   : Bitfield<2,1> { }; /* unmask interrupt */
 		struct Prescaler    : Bitfield<8,8> { };
 	};
diff --git a/repos/base-hw/src/core/spec/exynos5/timer.cc b/repos/base-hw/src/core/spec/exynos5/timer.cc
index fa0125063..4167cbb8c 100644
--- a/repos/base-hw/src/core/spec/exynos5/timer.cc
+++ b/repos/base-hw/src/core/spec/exynos5/timer.cc
@@ -17,6 +17,8 @@
 #include <board.h>
 #include <platform.h>
 
+#include <drivers/timer/util.h>
+
 using namespace Genode;
 using namespace Kernel;
 
@@ -34,50 +36,55 @@ unsigned Timer::interrupt_id() const
 Timer_driver::Timer_driver(unsigned cpu_id)
 :
 	Mmio(Platform::mmio_to_virt(Board::MCT_MMIO_BASE)),
+	local(Platform::mmio_to_virt(Board::MCT_MMIO_BASE)
+	      + (cpu_id ? L1 : L0)),
 	ticks_per_ms(calc_ticks_per_ms(Board::MCT_CLOCK)),
 	cpu_id(cpu_id)
 {
+	static unsigned initialized = 0;
+	if (initialized++) return;
+
 	Mct_cfg::access_t mct_cfg = 0;
 	Mct_cfg::Prescaler::set(mct_cfg, PRESCALER);
 	Mct_cfg::Div_mux::set(mct_cfg, DIV_MUX);
 	write<Mct_cfg>(mct_cfg);
-	write<L0_int_enb>(L0_int_enb::Frceie::bits(1));
-	write<L1_int_enb>(L1_int_enb::Frceie::bits(1));
+}
+
+
+Timer_driver::Local::Local(Genode::addr_t base)
+: Mmio(base)
+{
+	write<Int_enb>(Int_enb::Frceie::bits(1));
+
+	acked_write<Tcntb, Wstat::Tcntb>(0xffffffff);
+	acked_write<Frcntb, Wstat::Frcntb>(0xffffffff);
+
+	Tcon::access_t tcon = 0;
+	Tcon::Frc_start::set(tcon, 1);
+	Tcon::Timer_start::set(tcon, 1);
+	acked_write<Tcon, Wstat::Tcon>(tcon);
 }
 
 
 void Timer::_start_one_shot(time_t const ticks)
 {
-	switch (_driver.cpu_id) {
-	case 0:
-		_driver.write<Driver::L0_int_cstat::Frcnt>(1);
-		_driver.run_0(0);
-		_driver.acked_write<Driver::L0_frcntb, Driver::L0_wstat::Frcntb>(ticks);
-		_driver.run_0(1);
-		return;
-	case 1:
-		_driver.write<Driver::L1_int_cstat::Frcnt>(1);
-		_driver.run_1(0);
-		_driver.acked_write<Driver::L1_frcntb, Driver::L1_wstat::Frcntb>(ticks);
-		_driver.run_1(1);
-		return;
-	default: return;
-	}
+	_driver.local.cnt = _driver.local.read<Driver::Local::Tcnto>();
+	_driver.local.write<Driver::Local::Int_cstat::Frccnt>(1);
+	_driver.local.acked_write<Driver::Local::Frcntb,
+	                          Driver::Local::Wstat::Frcntb>(ticks);
 }
 
 
-time_t Timer::_value()
+time_t Timer::_duration() const
 {
-	switch (_driver.cpu_id) {
-	case 0: return _driver.read<Driver::L0_int_cstat::Frcnt>() ? 0 : _driver.read<Driver::L0_frcnto>();
-	case 1: return _driver.read<Driver::L1_int_cstat::Frcnt>() ? 0 : _driver.read<Driver::L1_frcnto>();
-	default: return 0;
-	}
+	unsigned long ret =  _driver.local.cnt - _driver.local.read<Driver::Local::Tcnto>();
+	return ret;
 }
 
 
-time_t Timer::_ticks_to_us(time_t const ticks) const {
-	return (ticks / _driver.ticks_per_ms) * 1000; }
+
+time_t Timer::ticks_to_us(time_t const ticks) const {
+	return timer_ticks_to_us(ticks, _driver.ticks_per_ms); }
 
 
 time_t Timer::us_to_ticks(time_t const us) const {
@@ -85,4 +92,4 @@ time_t Timer::us_to_ticks(time_t const us) const {
 
 
 time_t Timer::_max_value() const {
-	return (Driver::L0_frcnto::access_t)~0; }
+	return 0xffffffff; }
diff --git a/repos/base-hw/src/core/spec/exynos5/timer_driver.h b/repos/base-hw/src/core/spec/exynos5/timer_driver.h
index 5cffa4ba4..e13f39d18 100644
--- a/repos/base-hw/src/core/spec/exynos5/timer_driver.h
+++ b/repos/base-hw/src/core/spec/exynos5/timer_driver.h
@@ -40,131 +40,69 @@ struct Kernel::Timer_driver : Genode::Mmio
 	};
 
 
-	/*******************
-	 ** Local timer 0 **
-	 *******************/
+	/*****************
+	 ** Local timer **
+	 *****************/
 
-	/**
-	 * Free running counter buffer
-	 */
-	struct L0_frcntb : Register<0x310, 32> { };
+	enum Local_timer_offset { L0 = 0x300, L1 = 0x400 };
 
-	/**
-	 * Configuration
-	 */
-	struct L0_tcon : Register<0x320, 32>
-	{
-		struct Frc_start : Bitfield<3, 1> { };
+	struct Local : Genode::Mmio {
+
+		struct Tcntb  : Register<0x0, 32> { };
+		struct Tcnto  : Register<0x4, 32> { };
+		struct Icntb  : Register<0x8, 32> { };
+		struct Icnto  : Register<0xc, 32> { };
+		struct Frcntb : Register<0x10, 32> { };
+		struct Frcnto : Register<0x14, 32> { };
+
+		struct Tcon : Register<0x20, 32>
+		{
+			struct Timer_start : Bitfield<0, 1> { };
+			struct Irq_start   : Bitfield<1, 1> { };
+			struct Irq_type    : Bitfield<2, 1> { };
+			struct Frc_start   : Bitfield<3, 1> { };
+		};
+
+		struct Int_cstat : Register<0x30, 32, true>
+		{
+			struct Intcnt : Bitfield<0, 1> { };
+			struct Frccnt : Bitfield<1, 1> { };
+		};
+
+		struct Int_enb : Register<0x34, 32>
+		{
+			struct Inteie : Bitfield<0, 1> { };
+			struct Frceie : Bitfield<1, 1> { };
+		};
+
+		struct Wstat : Register<0x40, 32, true>
+		{
+			struct Tcntb  : Bitfield<0, 1> { };
+			struct Icntb  : Bitfield<1, 1> { };
+			struct Frcntb : Bitfield<2, 1> { };
+			struct Tcon   : Bitfield<3, 1> { };
+		};
+
+		Tcnto::access_t cnt = { 0 };
+
+		/**
+		 * Write to reg that replies via ack bit and clear ack bit
+		 */
+		template <typename DEST, typename ACK>
+		void acked_write(typename DEST::Register_base::access_t const v)
+		{
+			typedef typename DEST::Register_base Dest;
+			typedef typename ACK::Bitfield_base  Ack;
+			write<Dest>(v);
+			while (!read<Ack>());
+			write<Ack>(1);
+		}
+
+		void update_cnt() { cnt = read<Tcnto>(); }
+
+		Local(Genode::addr_t base);
 	};
 
-	/**
-	 * Expired status
-	 */
-	struct L0_int_cstat : Register<0x330, 32, true>
-	{
-		struct Frcnt : Bitfield<1, 1> { };
-	};
-
-	/**
-	 * Interrupt enable
-	 */
-	struct L0_int_enb : Register<0x334, 32>
-	{
-		struct Frceie : Bitfield<1, 1> { };
-	};
-
-	/**
-	 * Write status
-	 */
-	struct L0_wstat : Register<0x340, 32, true>
-	{
-		struct Frcntb : Bitfield<2, 1> { };
-		struct Tcon   : Bitfield<3, 1> { };
-	};
-
-	struct L0_frcnto : Register<0x314, 32> { };
-
-	/**
-	 * Start and stop counting
-	 */
-	void run_0(bool const run)
-	{
-		acked_write<L0_tcon, L0_wstat::Tcon>
-			(L0_tcon::Frc_start::bits(run));
-	}
-
-
-	/*******************
-	 ** Local timer 1 **
-	 *******************/
-
-	/**
-	 * Free running counter buffer
-	 */
-	struct L1_frcntb : Register<0x410, 32> { };
-
-	/**
-	 * Configuration
-	 */
-	struct L1_tcon : Register<0x420, 32>
-	{
-		struct Frc_start : Bitfield<3, 1> { };
-	};
-
-	/**
-	 * Expired status
-	 */
-	struct L1_int_cstat : Register<0x430, 32, true>
-	{
-		struct Frcnt : Bitfield<1, 1> { };
-	};
-
-	/**
-	 * Interrupt enable
-	 */
-	struct L1_int_enb : Register<0x434, 32>
-	{
-		struct Frceie : Bitfield<1, 1> { };
-	};
-
-	/**
-	 * Write status
-	 */
-	struct L1_wstat : Register<0x440, 32, true>
-	{
-		struct Frcntb : Bitfield<2, 1> { };
-		struct Tcon   : Bitfield<3, 1> { };
-	};
-
-	struct L1_frcnto : Register<0x414, 32> { };
-
-	/**
-	 * Start and stop counting
-	 */
-	void run_1(bool const run)
-	{
-		acked_write<L1_tcon, L1_wstat::Tcon>
-			(L1_tcon::Frc_start::bits(run));
-	}
-
-
-	/********************
-	 ** Helper methods **
-	 ********************/
-
-	/**
-	 * Write to reg that replies via ack bit and clear ack bit
-	 */
-	template <typename DEST, typename ACK>
-	void acked_write(typename DEST::Register_base::access_t const v)
-	{
-		typedef typename DEST::Register_base Dest;
-		typedef typename ACK::Bitfield_base  Ack;
-		write<Dest>(v);
-		while (!read<Ack>());
-		write<Ack>(1);
-	}
-
 	/**
 	 * Calculate amount of ticks per ms for specific input clock
 	 *
@@ -173,6 +111,7 @@ struct Kernel::Timer_driver : Genode::Mmio
 	time_t static calc_ticks_per_ms(unsigned const clock) {
 		return clock / (PRESCALER + 1) / (1 << DIV_MUX) / 1000; }
 
+	Local          local;
 	unsigned const ticks_per_ms;
 	unsigned const cpu_id;
 
diff --git a/repos/base-hw/src/core/spec/imx53/timer.cc b/repos/base-hw/src/core/spec/imx53/timer.cc
index 15cef4832..3a15c78cd 100644
--- a/repos/base-hw/src/core/spec/imx53/timer.cc
+++ b/repos/base-hw/src/core/spec/imx53/timer.cc
@@ -17,6 +17,8 @@
 #include <board.h>
 #include <platform.h>
 
+#include <drivers/timer/util.h>
+
 using namespace Genode;
 using namespace Kernel;
 
@@ -25,26 +27,38 @@ unsigned Timer::interrupt_id() const { return Board::EPIT_1_IRQ; }
 
 
 Timer_driver::Timer_driver(unsigned)
-: Mmio(Platform::mmio_to_virt(Board::EPIT_1_MMIO_BASE)) { }
+: Mmio(Platform::mmio_to_virt(Board::EPIT_1_MMIO_BASE))
+{
+	reset();
+
+	Cr::access_t cr = read<Cr>();
+	Cr::En_mod::set(cr, Cr::En_mod::RELOAD);
+	Cr::Oci_en::set(cr, 1);
+	Cr::Prescaler::set(cr, Cr::Prescaler::DIVIDE_BY_1);
+	Cr::Clk_src::set(cr, Cr::Clk_src::HIGH_FREQ_REF_CLK);
+	Cr::Iovw::set(cr, 1);
+	write<Cr>(cr);
+
+	write<Cmpr>(0xffffffff);
+	write<Cr::En>(1);
+
+	write<Lr>(0xffffffff);
+}
 
 
 void Timer::_start_one_shot(time_t const ticks)
 {
-	/* stop timer */
-	_driver.reset();
-
-	/* configure timer for a one-shot */
-	_driver.write<Driver::Cr>(Driver::Cr::prepare_one_shot());
-	_driver.write<Driver::Lr>(ticks);
-	_driver.write<Driver::Cmpr>(0);
-
-	/* start timer */
-	_driver.write<Driver::Cr::En>(1);
+	/*
+	 * First unset the interrupt flag,
+	 * otherwise if the tick is small enough, we loose an interrupt
+	 */
+	_driver.write<Driver::Sr::Ocif>(1);
+	_driver.write<Driver::Lr>(ticks - 1);
 }
 
 
-time_t Timer::_ticks_to_us(time_t const ticks) const {
-	return (ticks / Driver::TICS_PER_MS) * 1000UL; }
+time_t Timer::ticks_to_us(time_t const ticks) const {
+	return timer_ticks_to_us(ticks, Driver::TICS_PER_MS); }
 
 
 time_t Timer::us_to_ticks(time_t const us) const {
@@ -52,8 +66,14 @@ time_t Timer::us_to_ticks(time_t const us) const {
 
 
 time_t Timer::_max_value() const {
-	return (Driver::Cnt::access_t)~0; }
+	return 0xffffffff; }
 
 
-time_t Timer::_value() {
-	return _driver.read<Driver::Sr::Ocif>() ? 0 : _driver.read<Driver::Cnt>(); }
+time_t Timer::_duration() const
+{
+	Driver::Cnt::access_t last = _last_timeout_duration;
+	Driver::Cnt::access_t cnt  = _driver.read<Driver::Cnt>();
+	Driver::Cnt::access_t ret  = (_driver.read<Driver::Sr::Ocif>())
+		? _max_value() - cnt + last : last - cnt;
+	return ret;
+}
diff --git a/repos/base-hw/src/core/spec/imx53/timer_driver.h b/repos/base-hw/src/core/spec/imx53/timer_driver.h
index 09a2ad87b..02cb1a48f 100644
--- a/repos/base-hw/src/core/spec/imx53/timer_driver.h
+++ b/repos/base-hw/src/core/spec/imx53/timer_driver.h
@@ -52,40 +52,11 @@ struct Kernel::Timer_driver : Genode::Mmio
 
 		struct Swr     : Bitfield<16, 1> { }; /* software reset bit */
 		struct Iovw    : Bitfield<17, 1> { }; /* enable overwrite */
-		struct Dbg_en  : Bitfield<18, 1> { }; /* enable in debug mode */
-		struct Wait_en : Bitfield<19, 1> { }; /* enable in wait mode */
-		struct Doz_en  : Bitfield<20, 1> { }; /* enable in doze mode */
-		struct Stop_en : Bitfield<21, 1> { }; /* enable in stop mode */
-
-		struct Om : Bitfield<22, 2>           /* mode of the output pin */
-		{
-			enum { DISCONNECTED = 0 };
-		};
 
 		struct Clk_src : Bitfield<24, 2>      /* select clock input */
 		{
 			enum { HIGH_FREQ_REF_CLK = 2 };
 		};
-
-		/**
-		 * Register value that configures the timer for a one-shot run
-		 */
-		static access_t prepare_one_shot()
-		{
-			return En::bits(0) |
-			       En_mod::bits(En_mod::RELOAD) |
-			       Oci_en::bits(1) |
-			       Rld::bits(Rld::RELOAD_FROM_LR) |
-			       Prescaler::bits(Prescaler::DIVIDE_BY_1) |
-			       Swr::bits(0) |
-			       Iovw::bits(0) |
-			       Dbg_en::bits(0) |
-			       Wait_en::bits(0) |
-			       Doz_en::bits(0) |
-			       Stop_en::bits(0) |
-			       Om::bits(Om::DISCONNECTED) |
-			       Clk_src::bits(Clk_src::HIGH_FREQ_REF_CLK);
-		}
 	};
 
 	/**
diff --git a/repos/base-hw/src/core/spec/riscv/kernel/thread.cc b/repos/base-hw/src/core/spec/riscv/kernel/thread.cc
index c0be06654..da6e4a935 100644
--- a/repos/base-hw/src/core/spec/riscv/kernel/thread.cc
+++ b/repos/base-hw/src/core/spec/riscv/kernel/thread.cc
@@ -27,7 +27,7 @@ void Thread::exception(Cpu & cpu)
 
 	if (regs->is_irq()) {
 		/* there are only cpu-local timer interrupts right now */
-		cpu.interrupt(5);
+		cpu.interrupt(cpu.timer().interrupt_id());
 		return;
 	}
 
@@ -78,6 +78,7 @@ void Kernel::Thread::proceed(Cpu & cpu)
 }
 
 
+void Thread::user_ret_time(Kernel::time_t const t)  { regs->a0  = t;   }
 void Thread::user_arg_0(Kernel::Call_arg const arg) { regs->a0  = arg; }
 void Thread::user_arg_1(Kernel::Call_arg const arg) { regs->a1  = arg; }
 void Thread::user_arg_2(Kernel::Call_arg const arg) { regs->a2  = arg; }
diff --git a/repos/base-hw/src/core/spec/riscv/timer.cc b/repos/base-hw/src/core/spec/riscv/timer.cc
index d82852f02..1b1982e8e 100644
--- a/repos/base-hw/src/core/spec/riscv/timer.cc
+++ b/repos/base-hw/src/core/spec/riscv/timer.cc
@@ -26,7 +26,7 @@ Timer_driver::Timer_driver(unsigned)
 	asm volatile ("csrs sie, %0" : : "r"(STIE));
 }
 
-addr_t Timer_driver::stime() { return Hw::get_sys_timer(); }
+time_t Timer_driver::stime() const { return Hw::get_sys_timer(); }
 
 void Timer::_start_one_shot(time_t const ticks)
 {
@@ -35,22 +35,23 @@ void Timer::_start_one_shot(time_t const ticks)
 }
 
 
-time_t Timer::_ticks_to_us(time_t const ticks) const {
-	return (ticks / Driver::TICS_PER_MS) * 1000; }
+time_t Timer::ticks_to_us(time_t const ticks) const {
+	return ticks / Driver::TICS_PER_US; }
 
 
 time_t Timer::us_to_ticks(time_t const us) const {
-	return (us / 1000) * Driver::TICS_PER_MS; }
+	return us * Driver::TICS_PER_MS; }
 
 
 time_t Timer::_max_value() const {
-	return (addr_t)~0; }
+	return 0xffffffff; }
 
 
-time_t Timer::_value()
+time_t Timer::_duration() const
 {
 	addr_t time = _driver.stime();
-	return time < _driver.timeout ? _driver.timeout - time : 0;
+	return time < _driver.timeout ? _driver.timeout - time
+	                              : _last_timeout_duration + (time - _driver.timeout);
 }
 
 
diff --git a/repos/base-hw/src/core/spec/riscv/timer_driver.h b/repos/base-hw/src/core/spec/riscv/timer_driver.h
index 3ad4cde92..616d4c1a4 100644
--- a/repos/base-hw/src/core/spec/riscv/timer_driver.h
+++ b/repos/base-hw/src/core/spec/riscv/timer_driver.h
@@ -28,11 +28,12 @@ struct Kernel::Timer_driver
 	enum {
 		SPIKE_TIMER_HZ = 1000000,
 		TICS_PER_MS    = SPIKE_TIMER_HZ / 1000,
+		TICS_PER_US    = TICS_PER_MS / 1000,
 	};
 
-	addr_t timeout = 0;
+	time_t timeout = 0;
 
-	addr_t stime();
+	time_t stime() const;
 
 	Timer_driver(unsigned);
 };
diff --git a/repos/base-hw/src/core/spec/rpi/timer.cc b/repos/base-hw/src/core/spec/rpi/timer.cc
index d3066e469..ee0c711b2 100644
--- a/repos/base-hw/src/core/spec/rpi/timer.cc
+++ b/repos/base-hw/src/core/spec/rpi/timer.cc
@@ -29,12 +29,12 @@ void Timer::_start_one_shot(time_t const ticks)
 {
 	_driver.write<Driver::Cs::M1>(1);
 	_driver.read<Driver::Cs>();
-	_driver.write<Driver::Clo>(0);
-	_driver.write<Driver::Cmp>(_driver.read<Driver::Clo>() + ticks);
+	_driver.write<Driver::Cmp>(_driver.read<Driver::Clo>()
+	                           + (ticks < 2 ? 2 : ticks));
 }
 
 
-time_t Timer::_ticks_to_us(time_t const ticks) const {
+time_t Timer::ticks_to_us(time_t const ticks) const {
 	return ticks / Driver::TICS_PER_US; }
 
 
@@ -43,14 +43,17 @@ time_t Timer::us_to_ticks(time_t const us) const {
 
 
 time_t Timer::_max_value() const {
-	return (Driver::Clo::access_t)~0; }
+	return 0xffffffff; }
 
 
-time_t Timer::_value()
+time_t Timer::_duration() const
 {
-	Driver::Cmp::access_t const cmp = _driver.read<Driver::Cmp>();
 	Driver::Clo::access_t const clo = _driver.read<Driver::Clo>();
-	return cmp > clo ? cmp - clo : 0;
+	Driver::Cmp::access_t const cmp = _driver.read<Driver::Cmp>();
+	Driver::Cs::access_t  const irq = _driver.read<Driver::Cs::M1>();
+	uint32_t d = (irq) ? (uint32_t)_last_timeout_duration + (clo - cmp)
+	                   : clo - (cmp - _last_timeout_duration);
+	return d;
 }
 
 
diff --git a/repos/base-hw/src/core/spec/x86_64/kernel/thread.cc b/repos/base-hw/src/core/spec/x86_64/kernel/thread.cc
index f0d701fbf..f6310770c 100644
--- a/repos/base-hw/src/core/spec/x86_64/kernel/thread.cc
+++ b/repos/base-hw/src/core/spec/x86_64/kernel/thread.cc
@@ -62,6 +62,7 @@ void Kernel::Thread::proceed(Cpu & cpu)
 }
 
 
+void Kernel::Thread::user_ret_time(Kernel::time_t const t)  { regs->rdi = t;   }
 void Kernel::Thread::user_arg_0(Kernel::Call_arg const arg) { regs->rdi = arg; }
 void Kernel::Thread::user_arg_1(Kernel::Call_arg const arg) { regs->rsi = arg; }
 void Kernel::Thread::user_arg_2(Kernel::Call_arg const arg) { regs->rdx = arg; }
diff --git a/repos/base-hw/src/core/spec/x86_64/muen/timer.cc b/repos/base-hw/src/core/spec/x86_64/muen/timer.cc
index 7bccaac1d..7534ab2f1 100644
--- a/repos/base-hw/src/core/spec/x86_64/muen/timer.cc
+++ b/repos/base-hw/src/core/spec/x86_64/muen/timer.cc
@@ -14,6 +14,7 @@
 
 /* base includes */
 #include <base/log.h>
+#include <drivers/timer/util.h>
 
 /* core includes */
 #include <kernel/timer.h>
@@ -25,7 +26,7 @@ using namespace Genode;
 using namespace Kernel;
 
 
-Timer_driver::Timer_driver(unsigned) : ticks_per_ms(sinfo()->get_tsc_khz())
+Timer_driver::Timer_driver(unsigned) : ticks_per_ms(sinfo()->get_tsc_khz()), start(0)
 {
 	/* first sinfo instance, output status */
 	sinfo()->log_status();
@@ -64,7 +65,10 @@ unsigned Timer::interrupt_id() const {
 
 void Timer::_start_one_shot(time_t const ticks)
 {
-	const uint64_t t = _driver.rdtsc() + ticks;
+	static const time_t MIN_TICKS = 10UL;
+
+	_driver.start = _driver.rdtsc();
+	uint64_t t    = _driver.start + ((ticks > MIN_TICKS) ? ticks : MIN_TICKS);
 	_driver.event_page->tsc_trigger = t;
 
 	if (_driver.guest_event_page)
@@ -72,25 +76,18 @@ void Timer::_start_one_shot(time_t const ticks)
 }
 
 
-time_t Timer::_ticks_to_us(time_t const ticks) const {
-	return (ticks / _driver.ticks_per_ms) * 1000; }
+time_t Timer::ticks_to_us(time_t const ticks) const {
+	return timer_ticks_to_us(ticks, _driver.ticks_per_ms); }
 
 
 time_t Timer::us_to_ticks(time_t const us) const {
-	return (us / 1000) * _driver.ticks_per_ms; }
+	return us * (_driver.ticks_per_ms / 1000); }
 
 
-time_t Timer::_max_value() const {
-	return (time_t)~0; }
+time_t Timer::_max_value() const { return ~0UL; }
 
 
-time_t Timer::_value()
+time_t Timer::_duration() const
 {
-	const uint64_t now = _driver.rdtsc();
-	if (_driver.event_page->tsc_trigger != Driver::TIMER_DISABLED
-	    && _driver.event_page->tsc_trigger > now)
-	{
-		return _driver.event_page->tsc_trigger - now;
-	}
-	return 0;
+	return _driver.rdtsc() - _driver.start;
 }
diff --git a/repos/base-hw/src/core/spec/x86_64/muen/timer_driver.h b/repos/base-hw/src/core/spec/x86_64/muen/timer_driver.h
index 46a9e367a..d3f949810 100644
--- a/repos/base-hw/src/core/spec/x86_64/muen/timer_driver.h
+++ b/repos/base-hw/src/core/spec/x86_64/muen/timer_driver.h
@@ -25,6 +25,7 @@ struct Kernel::Timer_driver
 	enum { TIMER_DISABLED = ~0ULL };
 
 	Genode::uint64_t ticks_per_ms;
+	Genode::uint64_t start;
 
 	struct Subject_timed_event
 	{
@@ -35,7 +36,7 @@ struct Kernel::Timer_driver
 	struct Subject_timed_event * event_page = 0;
 	struct Subject_timed_event * guest_event_page = 0;
 
-	inline Genode::uint64_t rdtsc()
+	inline Genode::uint64_t rdtsc() const
 	{
 		Genode::uint32_t lo, hi;
 		asm volatile("rdtsc" : "=a" (lo), "=d" (hi));
diff --git a/repos/base-hw/src/core/spec/x86_64/timer.cc b/repos/base-hw/src/core/spec/x86_64/timer.cc
index 1a36b430d..7df4f63f0 100644
--- a/repos/base-hw/src/core/spec/x86_64/timer.cc
+++ b/repos/base-hw/src/core/spec/x86_64/timer.cc
@@ -94,7 +94,7 @@ void Timer::_start_one_shot(time_t const ticks) {
 	_driver.write<Driver::Tmr_initial>(ticks); }
 
 
-time_t Timer::_ticks_to_us(time_t const ticks) const {
+time_t Timer::ticks_to_us(time_t const ticks) const {
 	return timer_ticks_to_us(ticks, _driver.ticks_per_ms); }
 
 
@@ -106,8 +106,8 @@ time_t Timer::_max_value() const {
 	return (Driver::Tmr_initial::access_t)~0; }
 
 
-time_t Timer::_value() {
-	return _driver.read<Driver::Tmr_current>(); }
+time_t Timer::_duration() const {
+	return _last_timeout_duration - _driver.read<Driver::Tmr_current>(); }
 
 
 unsigned Timer::interrupt_id() const {
diff --git a/repos/base-hw/src/lib/base/arm/kernel/interface.cc b/repos/base-hw/src/lib/base/arm/kernel/interface.cc
index 03bc2ad0e..ecd90f3f8 100644
--- a/repos/base-hw/src/lib/base/arm/kernel/interface.cc
+++ b/repos/base-hw/src/lib/base/arm/kernel/interface.cc
@@ -56,6 +56,15 @@ using namespace Kernel;
  ** Kernel calls **
  ******************/
 
+Call_ret_64 Kernel::call64(Call_arg arg_0)
+{
+	register Call_arg arg_0_reg asm("r0") = arg_0;
+	register Call_arg arg_1_reg asm("r1");
+	asm volatile(CALL_1_SWI);
+	return ((Call_ret_64)arg_0_reg) << 32 | (Call_ret_64)arg_1_reg;
+}
+
+
 Call_ret Kernel::call(Call_arg arg_0)
 {
 	CALL_1_FILL_ARG_REGS
@@ -116,4 +125,4 @@ Call_ret Kernel::call(Call_arg arg_0,
 	CALL_6_FILL_ARG_REGS
 	asm volatile(CALL_6_SWI);
 	return arg_0_reg;
-}
\ No newline at end of file
+}
diff --git a/repos/base-hw/src/lib/base/riscv/kernel/interface.cc b/repos/base-hw/src/lib/base/riscv/kernel/interface.cc
index 248a89b0c..5690c466f 100644
--- a/repos/base-hw/src/lib/base/riscv/kernel/interface.cc
+++ b/repos/base-hw/src/lib/base/riscv/kernel/interface.cc
@@ -51,6 +51,14 @@ using namespace Kernel;
  ** Kernel calls **
  ******************/
 
+Call_ret Kernel::call64(Call_arg arg_0)
+{
+	CALL_1_FILL_ARG_REGS
+	asm volatile(CALL_1_SWI);
+	return arg_0_reg;
+}
+
+
 Call_ret Kernel::call(Call_arg arg_0)
 {
 	CALL_1_FILL_ARG_REGS
diff --git a/repos/base-hw/src/lib/base/x86_64/kernel/interface.cc b/repos/base-hw/src/lib/base/x86_64/kernel/interface.cc
index e33e5399c..26aa7aaee 100644
--- a/repos/base-hw/src/lib/base/x86_64/kernel/interface.cc
+++ b/repos/base-hw/src/lib/base/x86_64/kernel/interface.cc
@@ -68,6 +68,14 @@ Call_ret Kernel::call(Call_arg arg_0)
 }
 
 
+Call_ret_64 Kernel::call64(Call_arg arg_0)
+{
+	CALL_1_FILL_ARG_REGS
+	asm volatile(CALL_1_SYSCALL);
+	return arg_0_reg;
+}
+
+
 Call_ret Kernel::call(Call_arg arg_0,
                       Call_arg arg_1)
 {
diff --git a/repos/base-hw/src/timer/hw/time_source.cc b/repos/base-hw/src/timer/hw/time_source.cc
index 1d2637a70..bc03eb424 100644
--- a/repos/base-hw/src/timer/hw/time_source.cc
+++ b/repos/base-hw/src/timer/hw/time_source.cc
@@ -19,9 +19,6 @@
 /* local includes */
 #include <time_source.h>
 
-/* base-hw includes */
-#include <kernel/interface.h>
-
 using namespace Genode;
 
 enum { MIN_TIMEOUT_US = 1000 };
@@ -42,15 +39,14 @@ Timer::Time_source::Time_source(Env &env)
 void Timer::Time_source::schedule_timeout(Microseconds     duration,
                                           Timeout_handler &handler)
 {
-	unsigned long duration_us = duration.value;
+	Kernel::timeout_t duration_us = duration.value;
 	if (duration_us < MIN_TIMEOUT_US) {
 		duration_us = MIN_TIMEOUT_US; }
 
-	if (duration_us > max_timeout().value) {
-		duration_us = max_timeout().value; }
+	if (duration_us > _max_timeout_us) {
+		duration_us = _max_timeout_us; }
 
 	_handler = &handler;
-	_last_timeout_age_us = 0;
 	Signal_context_capability cap = _signal_handler;
 	Kernel::timeout(duration_us, (addr_t)cap.data());
 }
@@ -58,12 +54,11 @@ void Timer::Time_source::schedule_timeout(Microseconds     duration,
 
 Duration Timer::Time_source::curr_time()
 {
-	unsigned long const timeout_age_us = Kernel::timeout_age_us();
-	if (timeout_age_us > _last_timeout_age_us) {
-
-		/* increment time by the difference since the last update */
-		_curr_time.add(Microseconds(timeout_age_us - _last_timeout_age_us));
-		_last_timeout_age_us = timeout_age_us;
-	}
-	return _curr_time;
+	/*
+	 * FIXME: the `Microseconds` constructor takes a machine-word as value
+	 * thereby limiting the possible value to something ~1.19 hours.
+	 * must be changed when the timeout framework internally does not use
+	 * machine-word wide microseconds values anymore.
+	 */
+	return Duration(Microseconds(Kernel::time()));
 }
diff --git a/repos/base-hw/src/timer/hw/time_source.h b/repos/base-hw/src/timer/hw/time_source.h
index 7a5d76880..7abcdd635 100644
--- a/repos/base-hw/src/timer/hw/time_source.h
+++ b/repos/base-hw/src/timer/hw/time_source.h
@@ -17,6 +17,9 @@
 /* Genode includes */
 #include <base/duration.h>
 
+/* base-hw includes */
+#include <kernel/interface.h>
+
 /* local includes */
 #include <signalled_time_source.h>
 
@@ -32,10 +35,7 @@ class Timer::Time_source : public Genode::Signalled_time_source
 {
 	private:
 
-
-		Duration      mutable _curr_time { Microseconds(0) };
-		unsigned long mutable _last_timeout_age_us = 0;
-		unsigned long const   _max_timeout_us;
+		Kernel::time_t const _max_timeout_us;
 
 	public: