Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 7 additions & 1 deletion libplatsupport/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,13 @@ config_choice(
mark_as_advanced(CLEAR LibPlatSupportX86ConsoleDevice LibPlatSupportLPTMRclock)

# Some platforms don't have a platform timer.
if(KernelPlatformCheshire)
if(
(KernelPlatformQEMUArmVirt AND NOT (KernelArmExportPCNTUser AND KernelArmExportPTMRUser))
OR KernelPlatformRocketchip
OR KernelPlatformRocketchipZCU102
OR KernelPlatformCheshire
OR (SIMULATION AND (KernelArchRiscV OR KernelArchARM))
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@midnightveil for some reason this line breaks the camkes timer component build. For all Arm platforms we're getting:

  /github/workspace/projects/global-components/components/TimeServer/src/time_server.c: In function ‘post_init’:
  /github/workspace/projects/global-components/components/TimeServer/src/time_server.c:230:13: error: call to ‘ltimer_default_init’ declared with attribute error: no ltimer support for this platform
    230 |     error = ltimer_default_init(&ltimer, io_ops, time_server_ltimer_handle, NULL);
        |             ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

(e.g. https://github.com/seL4/camkes-tool/actions/runs/15923333523/job/45177979627)

If I remove this line, everything builds and works fine. Either SIMULATION does not mean what it says or it is on for those builds even though they are hardware images. It does seem to work if I explicitly provide -DSIMULATION=OFF on the command line.

Are we actually sure that it is true for all Arm platforms that qemu does not provide an ltimer device? I thought that some of them have fairly extensive device simulation (but maybe not timer, I have not checked).

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

SIMULATE does just seem to be on for those builds. It is actually generating a simulate script (which then says the platform is not supported for simulation).

So the right fix seems to be to make sure SIMULATE is not on for those builds, but it makes me wonder if we're braking other builds without intending to.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, so it does intentionally switch on SIMULATION by default in easy-settings.cmake

set(SIMULATION ON CACHE BOOL "Try and use simulable features")

So I'm not entirely sure how to proceed. Do we actually need to guard SIMULATION here in util_libs, or is it just to fail early?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This was copied from sel4test: https://github.com/seL4/sel4test/pull/142/files

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What the issue is probably that it was previously an

if (qemu arm virt)
    if (timers) enable
    else disable
else (check this bunch of other conditions)
    disable

Now it is

if (qemu arm virt OR these other conditions)
   disable

Copy link
Contributor Author

@midnightveil midnightveil Jul 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
OR (SIMULATION AND (KernelArchRiscV OR KernelArchARM))
OR ((NOT KernelPlatformQEMUArmVirt) AND SIMULATION AND (KernelArchRiscV OR KernelArchARM))

I think would be equivalent?

EDIT: Actually, no, it's still different. I'm going to go back to the original double if I guess.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

)
set(LibPlatSupportHaveTimer OFF)
else()
set(LibPlatSupportHaveTimer ON)
Expand Down
4 changes: 2 additions & 2 deletions libplatsupport/include/platsupport/ltimer.h
Original file line number Diff line number Diff line change
Expand Up @@ -325,15 +325,15 @@ static inline void ltimer_us_delay(ltimer_t *timer, uint64_t microseconds)
* with calling the ltimer functions inside the callback, the ltimer interface
* functions are not reentrant.
*/
#ifndef CONFIG_LIB_PLAT_SUPPORT_HAVE_TIMER
#if !defined(CONFIG_LIB_PLAT_SUPPORT_HAVE_TIMER) && __has_attribute(error)
__attribute__((error("no ltimer support for this platform")))
#endif
int ltimer_default_init(ltimer_t *timer, ps_io_ops_t ops, ltimer_callback_fn_t callback, void *callback_token);

/* initialise the subset of functions required to get
* the resources this ltimer needs without initialising the actual timer
* drivers*/
#ifndef CONFIG_LIB_PLAT_SUPPORT_HAVE_TIMER
#if !defined(CONFIG_LIB_PLAT_SUPPORT_HAVE_TIMER) && __has_attribute(error)
__attribute__((error("no ltimer support for this platform")))
#endif
int ltimer_default_describe(ltimer_t *timer, ps_io_ops_t ops);