diff --git a/ada/mutime/hw-time-timer.adb b/ada/mutime/hw-time-timer.adb
index 272289c..c683d6f 100644
--- a/ada/mutime/hw-time-timer.adb
+++ b/ada/mutime/hw-time-timer.adb
@@ -17,8 +17,8 @@
 with Muschedinfo;
 
 package body HW.Time.Timer
-   with Refined_State => (Timer_State => null,
-                          Abstract_Time => (Sinfo, Sched_Info))
+   with Refined_State => (Timer_State => (Sinfo),
+                          Abstract_Time => (Sched_Info))
 is
    Sinfo_Base_Address : constant := 16#000e_0000_0000#;
    Sinfo_Page_Size    : constant
@@ -27,6 +27,8 @@
 
    Sinfo : Musinfo.Subject_Info_Type
    with
+      Volatile,
+      Async_Writers,
       Address => System'To_Address (Sinfo_Base_Address);
 
    Sched_Info : Muschedinfo.Scheduling_Info_Type
@@ -51,9 +53,11 @@
       return T (TSC_Schedule_End);
    end Raw_Value_Max;
 
-   function Hz return T is
+   function Hz return T
+   is
+      Khz : constant T := T (Sinfo.TSC_Khz);
    begin
-      return T (Sinfo.TSC_Khz) * 1000;
+      return Khz * 1000;
    end Hz;
 
 end HW.Time.Timer;
diff --git a/common/hw-time-timer.ads b/common/hw-time-timer.ads
index cfe2e0b..90978df 100644
--- a/common/hw-time-timer.ads
+++ b/common/hw-time-timer.ads
@@ -14,11 +14,12 @@
 
 private package HW.Time.Timer
    with
-      Abstract_State => ((Timer_State with Part_Of => HW.Time.State),
+      Abstract_State => ((Timer_State with
+                           Part_Of => HW.Time.State,
+                           External => Async_Writers),
                          (Abstract_Time with
                            Part_Of => HW.Time.State,
-                           External => Async_Writers)),
-      Initializes => (Timer_State)
+                           External => Async_Writers))
 is
 
    -- Returns the highest point in time that has definitely passed.
@@ -37,6 +38,7 @@
 
    function Hz return T
    with
+      Volatile_Function,
       Global => (Input => Timer_State);
 
 end HW.Time.Timer;
diff --git a/common/hw-time.adb b/common/hw-time.adb
index 28db95d..b81d343 100644
--- a/common/hw-time.adb
+++ b/common/hw-time.adb
@@ -34,25 +34,28 @@
    with
       Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
    is
+      Hz : constant T := Timer.Hz;
       Current : constant T := Timer.Raw_Value_Max;
    begin
-      return Current + (T (US) * Timer.Hz + 999_999) / 1_000_000;
+      return Current + (T (US) * Hz + 999_999) / 1_000_000;
    end US_From_Now;
 
    function MS_From_Now (MS : Natural) return T
    with
       Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
    is
+      Hz : constant T := Timer.Hz;
       Current : constant T := Timer.Raw_Value_Max;
    begin
-      return Current + (T (MS) * Timer.Hz + 999) / 1_000;
+      return Current + (T (MS) * Hz + 999) / 1_000;
    end MS_From_Now;
 
    function Now_US return Int64
    with
       Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
    is
-      MHz : constant T := Timer.Hz / 1_000_000;
+      Hz : constant T := Timer.Hz;
+      MHz : constant T := Hz / 1_000_000;
       Current : constant T := Timer.Raw_Value_Min;
    begin
       return Int64 (Current and (2 ** 63 - 1))
@@ -65,7 +68,7 @@
    with
       Refined_Global => (Input => (Timer.Abstract_Time))
    is
-      Current: T;
+      Current : T;
    begin
       loop
          Current := Timer.Raw_Value_Min;