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
