Dear sel4 community,
yesterday I've started to develop a low-level platform test to stress several multi-processor aspects on top of the Genode API. Thereby, I've recognized that on sel4/x86_64 the TLB is practically not always cleaned properly in SMP systems.
The test spawns threads of one protection domain on each available cpu. Each thread accesses one of the first words of a shared dataspace. Afterwards the main thread on CPU 0 detaches and destroys the dataspace. Unfortunately, the threads on other CPUs still successfully access the corresponding memory instead of triggering a fault.
To be able to reproduce the problem, you might investigate the simple test case here:
https://github.com/skalk/genode/commit/2d2d7f982555f551227ad5dcbf9df46705d7d...
My colleague Alexander Boettcher already investigated the problem in part, and might share his insights with you.
Best regards Stefan
Hello,
On 15.11.18 13:20, Stefan Kalkowski wrote:
yesterday I've started to develop a low-level platform test to stress several multi-processor aspects on top of the Genode API. Thereby, I've recognized that on sel4/x86_64 the TLB is practically not always cleaned properly in SMP systems.
The test spawns threads of one protection domain on each available cpu. Each thread accesses one of the first words of a shared dataspace. Afterwards the main thread on CPU 0 detaches and destroys the dataspace. Unfortunately, the threads on other CPUs still successfully access the corresponding memory instead of triggering a fault.
To be able to reproduce the problem, you might investigate the simple test case here:
https://github.com/skalk/genode/commit/2d2d7f982555f551227ad5dcbf9df46705d7d...
My colleague Alexander Boettcher already investigated the problem in part, and might share his insights with you.
as far as I can tell, the invalidation is skipped at this line [0].
If one removes the conditional check, and ever do the invalidation call - then the test succeeds (so, the thread faults on the remote CPU as expected).
The line looks like a "optimization" attempt which breaks things. I have to point out that CONFIG_SUPPORT_PCID is unset in our kernel configuration. Nevertheless, on x86 SMP setups you have ever to notify remote CPUs to flush/invalidate the TLB, which seems to be avoided at [0].
Interestingly, on ARM [1], at least it seems, that you handle things unconditional in the unmapPage code handling.
I hope the information are helpful to fix the issue.
Cheers,
Alex.
[0] https://github.com/seL4/seL4/blob/9.0.1/src/arch/x86/kernel/vspace.c#L761 [1] https://github.com/seL4/seL4/blob/9.0.1/src/arch/arm/64/kernel/vspace.c#L140...
Hello,
since there are no converse suggestions/ideas by anyone, I opened up a pull request which fixes (according to our TLB flush test) this seL4 kernel bug on x86 in SMP setups. The patch is used with 9.0.0, however cleanly applies to latest seL4 release (10.1.1).
Cheers,
Alex.
https://github.com/seL4/seL4/pull/107
On 15.11.18 14:39, Alexander Boettcher wrote:
Hello,
On 15.11.18 13:20, Stefan Kalkowski wrote:
yesterday I've started to develop a low-level platform test to stress several multi-processor aspects on top of the Genode API. Thereby, I've recognized that on sel4/x86_64 the TLB is practically not always cleaned properly in SMP systems.
The test spawns threads of one protection domain on each available cpu. Each thread accesses one of the first words of a shared dataspace. Afterwards the main thread on CPU 0 detaches and destroys the dataspace. Unfortunately, the threads on other CPUs still successfully access the corresponding memory instead of triggering a fault.
To be able to reproduce the problem, you might investigate the simple test case here:
https://github.com/skalk/genode/commit/2d2d7f982555f551227ad5dcbf9df46705d7d...
My colleague Alexander Boettcher already investigated the problem in part, and might share his insights with you.
as far as I can tell, the invalidation is skipped at this line [0].
If one removes the conditional check, and ever do the invalidation call
- then the test succeeds (so, the thread faults on the remote CPU as
expected).
The line looks like a "optimization" attempt which breaks things. I have to point out that CONFIG_SUPPORT_PCID is unset in our kernel configuration. Nevertheless, on x86 SMP setups you have ever to notify remote CPUs to flush/invalidate the TLB, which seems to be avoided at [0].
Interestingly, on ARM [1], at least it seems, that you handle things unconditional in the unmapPage code handling.
I hope the information are helpful to fix the issue.
Cheers,
Alex.
[0] https://github.com/seL4/seL4/blob/9.0.1/src/arch/x86/kernel/vspace.c#L761 [1] https://github.com/seL4/seL4/blob/9.0.1/src/arch/arm/64/kernel/vspace.c#L140...
since there are no converse suggestions/ideas by anyone, I opened up a pull request which fixes (according to our TLB flush test) this seL4 kernel bug on x86 in SMP setups. The patch is used with 9.0.0, however cleanly applies to latest seL4 release (10.1.1).
I can confirm that this fixes the issue that was reported. This has now been merged in https://github.com/seL4/seL4/pull/107.
-
Alexander Boettcher -
Mcleod, Kent (Data61, Kensington NSW) -
Stefan Kalkowski