Kurt Wu

> But also, that diff looks like a standard git diff in the output to me? It's got the @ notation for line numbers and everything, all as one. The...

> As in, CI doesn't have the SMP version of microkit installed, because it's in no official version. Otherwise with the SMP version it should work fine? Unless it doesn't?...

Furthermore, it is likely that the barrier here https://github.com/au-ts/sddf/blob/f3685158faa7f8f379fa918821186ae7667e0e87/drivers/network/imx/ethernet.c#L69-L72 is incorrect, either because it is too weak (compiled into a [`dmb ish`](https://godbolt.org/z/3c936x3Ge) on ARM64, but device interaction requires at least...

For interaction with non-coherent devices. In Cheng's driver, for example, barriers to order accesses to normal memory and device memory are likely missing.

I _suppose_ adding such a barrier has little effect on guaranteeing interrupt delivery. > Interestingly, the kernel when using the ARM timer only uses isb in certain cases. Could you...

Oh sorry. Without using the `isb` barrier, the timer tick value returned might be off by at most hundreds of cycles on existing hardware (I _guess_, based on the size...

> FEAT_ECV is mandatory from Armv8.6. Which implies Cortex-A520 or later. A520 was launched in 2023.

I am not familiar with either Rust or rust-sel4, but [this](https://godbolt.org/z/8fsacrfrz) is a simple case that illustrate the issue ```Rust pub fn f(x: &mut i32) -> i32 { *x =...

I am not sure about this. I cannot find an explicit reference in rust's [manual](https://doc.rust-lang.org/reference/inline-assembly.html) on this. I assume that even without the `asm`, the code will work because of...

To show the issue of our use of `THREAD_MEMORY_RELEASE` for the consumer on risc-v, consider [this](https://godbolt.org/z/1Y1YjxzKf) test, where it is desired that once the consumer observes the updated `flag`, it...