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