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
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 <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.systems To unsubscribe send an email to devel-leave@sel4.systemsmailto:devel-leave@sel4.systems
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 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 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.systems To unsubscribe send an email to devel-leave@sel4.systems
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 sleffler@google.com Sent: Wednesday, 11 January 2023 4:06 PM To: Ivan Velickovic i.velickovic@unsw.edu.au Cc: devel 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 <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 <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.systems To unsubscribe send an email to devel-leave@sel4.systemsmailto:devel-leave@sel4.systems
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 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 sleffler@google.com Sent: Wednesday, 11 January 2023 4:06 PM To: Ivan Velickovic i.velickovic@unsw.edu.au Cc: devel 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 <i.velickovic@unsw.edu.au 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 <devel@sel4.systems 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
Devel mailing list -- devel@sel4.systems To unsubscribe send an email to 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 <kgugala@antmicro.commailto: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 <i.velickovic@unsw.edu.aumailto: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 <sleffler@google.commailto:sleffler@google.com> Sent: Wednesday, 11 January 2023 4:06 PM To: Ivan Velickovic <i.velickovic@unsw.edu.aumailto:i.velickovic@unsw.edu.au> Cc: devel <devel@sel4.systemsmailto: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 <i.velickovic@unsw.edu.aumailto:i.velickovic@unsw.edu.au<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 <devel@sel4.systemsmailto:devel@sel4.systems<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.systems<mailto:devel@sel4.systemsmailto:devel@sel4.systems> To unsubscribe send an email to devel-leave@sel4.systemsmailto:devel-leave@sel4.systems<mailto: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
-
Ivan Velickovic -
Karol Gugala -
Sam Leffler