I did look into Renode a couple months ago and it seems like it definitely has the potential to be a better simulator than QEMU (at least for seL4-related purposes). However, I found that the support for ARM was lacking, e.g there is no 64-bit Cortex-A CPU support. For RISC-V, the support seems to be better but I found it difficult to just get sel4test working and eventually gave up. Is your Renode script public anywhere? I'd be very keen to have a look! Ivan ________________________________ From: Sam Leffler Sent: Wednesday, 11 January 2023 4:06 PM To: Ivan Velickovic Cc: devel Subject: Re: [seL4] sel4test:nested timeout fault test flaky? Thanks. FWIW our riscv32 mcs tests run reliably under renode should you be interested in using a different simulator. It appears the 64-bit aarch64/raspi qemu runs only fail on the cited test so I'll probably just disable the test. On Tue, Jan 10, 2023 at 6:58 PM Ivan Velickovic mailto:i.velickovic@unsw.edu.au> wrote: Hello Sam Myself and Gerwin attempted to get simulation platforms working with MCS for the CI and noticed that the MCS tests were not consistently passing. I don’t think it’s a bug with the kernel but rather to do with how QEMU emulates timers. There’s more details here: https://github.com/seL4/ci-actions/pull/233. Ivan On 6/01/2023, at 5:13 AM, Sam Leffler via Devel mailto:devel@sel4.systems> wrote: We run sel4test regularly for a 64-bit raspi target under qemu and occasionally see failures like this: Starting test 129: TIMEOUTFAULT0003 Running test TIMEOUTFAULT0003 (Nested timeout fault) Error: Check badge(3) == expected_badge(2) failed. at line 9 This is a stock sel4test https://github.com/AmbiML/sparrow-sel4test + dep libs but an older kernel https://github.com/AmbiML/sparrow-kernel. Anyone know if this is an old (presumably fixed) bug or known issue? -Sam _______________________________________________ Devel mailing list -- devel@sel4.systemsmailto:devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systemsmailto:devel-leave@sel4.systems

Great! Thanks Karol, I look forward to it getting mainlined. Ivan On 23/01/2023, at 10:21 PM, Karol Gugala mailto:kgugala@antmicro.com> wrote: You don't often get email from kgugala@antmicro.commailto:kgugala@antmicro.com. Learn why this is importanthttps://aka.ms/LearnAboutSenderIdentification Hi Ivan, Let me comment on Renode ARM64 support: ARM64 is coming to Renode, we're working on it currently. Right now we have it running Zephyr and Coreboot targets, seL4 is on our todo list as well. Indeed, tests in Renode should be fully reproducible, as we strictly control the virtual time flow and want the results not to be affected by the host machine performance or scheduling issues. We'll let you know as soon as we release the preliminary AArch64 support. Regarding tests on RISC-V - we have some internal configuration for an abstract RISC-V, we will publish it on GitHub. Best regards Karol On Thu, 19 Jan 2023 at 02:21, Ivan Velickovic mailto:i.velickovic@unsw.edu.au> wrote: I did look into Renode a couple months ago and it seems like it definitely has the potential to be a better simulator than QEMU (at least for seL4-related purposes). However, I found that the support for ARM was lacking, e.g there is no 64-bit Cortex-A CPU support. For RISC-V, the support seems to be better but I found it difficult to just get sel4test working and eventually gave up. Is your Renode script public anywhere? I'd be very keen to have a look! Ivan ________________________________ From: Sam Leffler mailto:sleffler@google.com> Sent: Wednesday, 11 January 2023 4:06 PM To: Ivan Velickovic mailto:i.velickovic@unsw.edu.au> Cc: devel mailto:devel@sel4.systems> Subject: Re: [seL4] sel4test:nested timeout fault test flaky? Thanks. FWIW our riscv32 mcs tests run reliably under renode should you be interested in using a different simulator. It appears the 64-bit aarch64/raspi qemu runs only fail on the cited test so I'll probably just disable the test. On Tue, Jan 10, 2023 at 6:58 PM Ivan Velickovic mailto:i.velickovic@unsw.edu.aumailto:i.velickovic@unsw.edu.au>> wrote: Hello Sam Myself and Gerwin attempted to get simulation platforms working with MCS for the CI and noticed that the MCS tests were not consistently passing. I don’t think it’s a bug with the kernel but rather to do with how QEMU emulates timers. There’s more details here: https://github.com/seL4/ci-actions/pull/233. Ivan On 6/01/2023, at 5:13 AM, Sam Leffler via Devel mailto:devel@sel4.systemsmailto:devel@sel4.systems>> wrote: We run sel4test regularly for a 64-bit raspi target under qemu and occasionally see failures like this: Starting test 129: TIMEOUTFAULT0003 Running test TIMEOUTFAULT0003 (Nested timeout fault) Error: Check badge(3) == expected_badge(2) failed. at line 9 This is a stock sel4test https://github.com/AmbiML/sparrow-sel4test + dep libs but an older kernel https://github.com/AmbiML/sparrow-kernel. Anyone know if this is an old (presumably fixed) bug or known issue? -Sam _______________________________________________ Devel mailing list -- devel@sel4.systemsmailto:devel@sel4.systemsmailto:devel@sel4.systems> To unsubscribe send an email to devel-leave@sel4.systemsmailto:devel-leave@sel4.systemsmailto:devel-leave@sel4.systems> _______________________________________________ Devel mailing list -- devel@sel4.systemsmailto:devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systemsmailto:devel-leave@sel4.systems -- Karol Gugala mobile +48 604 517 189 Antmicro Ltd | www.antmicro.comhttp://www.antmicro.com/ Zwierzyniecka 3, 60-813 Poznan, Poland