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