15 Nov
2018
15 Nov
'18
1:20 p.m.
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/2d2d7f982555f551227ad5dcbf9df46705d7…
My colleague Alexander Boettcher already investigated the problem in
part, and might share his insights with you.
Best regards
Stefan
--
Stefan Kalkowski
Genode labs
https://github.com.skalk | https://genode.org
15 Nov
15 Nov
2:39 p.m.
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/2d2d7f982555f551227ad5dcbf9df46705d7…
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#L14…
--
Alexander Boettcher
Genode Labs
https://www.genode-labs.com - https://www.genode.org
Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth
18 Dec
18 Dec
9:27 p.m.
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:
--
Alexander Boettcher
Genode Labs
https://www.genode-labs.com - https://www.genode.org
Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth
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/2d2d7f982555f551227ad5dcbf9df46705d7…
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#L14…
15 Nov
15 Nov
2:29 a.m.
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.
958
days inactive
1323
days old
3 comments
3 participants
participants (3)
-
Alexander Boettcher -
Mcleod, Kent (Data61, Kensington NSW) -
Stefan Kalkowski