init: add hooks for hpet emulation

[chrisguikema]

This allows VMs to emulate the HPET for higher-precision timing.

Test with: seL4/seL4_projects_libs#117, seL4/camkes-vm-examples#51

[chrisguikema]

The build only seems to be failing because the "Test with" isn't working. Did I mess something up?

[lsf37]

The build only seems to be failing because the "Test with" isn't working. Did I mess something up?

The "Test with" has to be in the PR description, not in a comment. I'll update.

[chrisguikema]

Thanks, Gerwin! I'll remember that for next time.

[abrandnewusername]

Looks great to me. It will be nice to have a VM example that demonstrates/tests HPET emulation.

[chrisguikema]

Looks great to me. It will be nice to have a VM example that demonstrates/tests HPET emulation.

Do we even have a test application for a 64-bit guest? If not, I can make one, and have it use the HPET emulation.

[chrisguikema]

For what its worth, I added a flag to the minimal application that enables 64-bit guests and emulates the HPET. I don't know how to add that flag to the gitlab test runner, but it would be a good thing to add to the CI! @lsf37

[chrisguikema]

Alright, so y'all will have to manually test the HPET emulation.

CI testing doesn't work because 64-bit VMs have a different file name than the Runner is expecting: https://github.com/seL4/camkes-vm/actions/runs/6697978462/job/18199249921#step:4:1299

And I can't test 32-bit VMs because they don't have HPET support compiled in.

[chrisguikema]

@abrandnewusername Have you been able to look at this?

[chrisguikema]

I updated the 32-bit Linux image to support the HPET, and it looks like the tests are failing. The minimal example does seem to use the HPET at least, so there is a chance that I messed something up.

[email protected]:426 invalid HPET_CFG + 4

@abrandnewusername do you want me to update the UseHPET variable to only be used with 64-bit guests? That way we can get this merged, and 32-bit support can be added later if anyone needs it?

[chrisguikema]

@abrandnewusername I was able to work with @lsf37 to create a 64-bit guest test. The minimal_64 test worked on a hardware run, with the clocksource switching to the hpet: https://github.com/seL4/camkes-vm/actions/runs/6869868181/job/18683754338?pr=113#step:4:2791

What needs to happen to get this feature merged? Do I need to update the dependency to be a 64-bit guest?

[abrandnewusername]

I don't have much experience with HPET so I can't comment on the actual HPET emulation code. Apart from that, everything else is good to go.