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/2d2d7f982555f551227ad5dcbf9df46705d7da50 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 _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
