[Marcus Voelp]
I understand there are substantial variations of L4 implementations, and I don't have a complete picture of which one uses which algorithm.
You are right, there are different implementations in the various kernels. To my knowledge none is currently using the algorithm I described in my diploma thesis.
Just thought I'd chip in to describe how the new mapping database in Pistachio works. Modificateion of access rights occur in a top-down order using a depth first traversal. Deletion of mappings or resetting access status bits occur in the opposite order (i.e., reversed depth first traversal) after the end of the mapping tree has been reached.
The problems you describe would not apply to any Pistachio implementation since locking (either of subtrees or whole mapping DB) would ensure that you'd have no concurrent conflicting operations.
eSk