Indan Zupancic

Does the problem occur with the newest QEMU version? There seem to have been some bugfixes last year that may be relevant.

Could you double check which assert is hit, the first one on line 283 or the second one on line 284? They check for different queues. And please double check...

I think it is the `postpone()` call on line 191 in [doReplyTransfer()](https://github.com/seL4/seL4/blob/61a8ccef44eeb08ecd20ad40296340c8319adee5/src/kernel/thread.c#L191) that triggers the assert. It can't be `schedContext_resume()` or `chargeBudget()`, as those guard the call with `isSchedulable()`, which...

@Kswin01 Any update on this from your end?

Can you try the newest kernel? The microkit branch is 2 years old. You may need to merge commits c8ef493d038b81cc43f82c0190788e4b3bdb4d9d and 92f0f3ab28f00c97851512216c855f4180534a60 manually.

> It's using the latest kernel the comment about using the `microkit` branch of seL4 is not quite correct. Is there a reason why there are no PRs for the...

@Kswin01, does it work if you replace line 183 with `if (isSchedulable(receiver))`? Not saying it's a proper fix, but perhaps it gives us more information.

Could you add an if-check before the assert with the same condition and print out what the actual values are? Perhaps it just overflows because it's not initialised correctly.

I think it got broken by [this](https://github.com/riscv-software-src/opensbi/commit/59a08cd7d632bb2394a29956497dfe7829099997) commit, which is part of [Split region permissions into M-mode and SU-mode](http://lists.infradead.org/pipermail/opensbi/2023-January/004127.html). Perhaps platforms are expected to add explicit S/U access to CLINT...

> I don't think it was broken by that commit since v1.2 of OpenSBI was released last year and that commit is from January this year. I don't know then,...