Nico Huber has uploaded this change for review. ( https://review.coreboot.org/26838
Change subject: time: Revise state abstraction ......................................................................
time: Revise state abstraction
Make abstract state `State` of HW.Time.Timer, that's used to derive the Hz value for instance, External. This helps to fix flow issues in the mutime implementation and also matches real hardware better: The clock rate may be derived from the hardware state.
HW.Time.Timer.Hz had to be made a volatile function, therefore.
Change-Id: I35af2d0db1acbf9652ea00763aa288545746bb79 Signed-off-by: Nico Huber nico.huber@secunet.com --- M ada/mutime/hw-time-timer.adb M common/hw-time-timer.ads M common/hw-time.adb 3 files changed, 20 insertions(+), 11 deletions(-)
git pull ssh://review.coreboot.org:29418/libhwbase refs/changes/38/26838/1
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;