Indan Zupancic

Except for time-outs, IMX8MQ_EVK fails with: `seL4 failed assertion 'NODE_STATE(ksCurTime) < MAX_RELEASE_TIME' at /github/workspace/kernel/include/kernel/thread.h:235 in function updateTimestamp` Perhaps we should add a check early at boot to catch any `ksCurTime`...

[HW Run (ODROID_XU4, armv7a, clang)](https://github.com/seL4/seL4/runs/7293526359?check_suite_focus=true#logs) fails with: > Running test CACHEFLUSH0001 (Test a cache maintenance on pages) > *ptrc == 0xBEEFCAFE at line 104 of file /github/workspace/projects/sel4test/apps/sel4test-tests/src/tests/cache.c I'm not convinced...

> The downside is, that accessing invalid device memory can lead to undefined behavior. Is this the only reason, or are there other advantages to change how it currently is?...

We would like to use DMA on cached memory for performance reasons, and doing cache maintenance from EL0 would help here. Perhaps add an (advanced) kernel build option to allow...

70-80% of original performance with high IRQ or latency sensitive loads (small transactions) seems pretty good to me. Step 3 can be optimised away by letting the VMM handle guest...

> really? What are the performance data that you test? @Makebug: Personal experience with performance testing in general and just common sense really. Without more information what performance you are...

It does not make sense to run real-time things in any guest OS. Either run it in seL4, or run the OS native. That said, are those latencies in ms...

Thinking about it a bit more, I think the current behaviour is unwanted because it makes it possible for low priority tasks to postpone execution of higher priority periodic tasks...

> This is unrelated to moving the position of updateTimestamp right? Correct. The -1 in setDeadline is only needed to make the actual period exactly match the configured period. Without...

Hm, is ksDomainTime supposed to be per node or system-wide? I would expect it to be node state, not global state. Is MCS + SMP + numDomains > 1 supported?