Indan Zupancic
Indan Zupancic
Any reason why a standard, unmodified libc like newlib isn't used, instead of taking on the burden of keeping a fork up-to-date? That's what we used at my previous work...
It's the second check that fails, on line 153: ``` /* Counter should have moved. */ test_check(counter != old_counter); ``` Does increasing the busy sleep from 10ms to something higher...
Without https://github.com/seL4/seL4/pull/847 this fails with 2498 and 2494 for SMP instead of the expected 2500 on tqma8xqp1gb.
Correct. The test can be made less strict by reducing the sleep time.
This seems a duplicate/extension of #65 btw.
I'm not sure if it's a new failure mode, the others happened for release builds. In the test the tasks on other cores are calling `seL4_Yield()` in a loop, while...
All that you say seems to confirm what I suspect: The locking code is broken (sometimes miscompiled?), and whether that causes problems or not is timing dependent, so any small...
> Not sure if it's the same issue (might be relevant), but there was similar behaviour that we had to do [this](https://github.com/seL4/seL4/commit/3d2ae69f9cb184c34b6b56d1365e57693e832db4). The code has changed since then That commit...
That's that dodgy Odroid board again, isn't it? I don't trust that hardware, and hence won't spend timing debugging problems on it. Could you change CI so it's using `odroidxu4_2`...
> One observation is that the kernel doesn't track whether a mapping is cached or uncached. I wouldn't expect the architecture to have a problem with cache maintenance operations on...