Is there a realistic scenario where the mask passed to doRemoteMaskOp is the current core?

seL4 kernel
1

It seems like the “current core IS set in the mask” situation in doRemoteMaskOp can’t really be created with the 12.1.0-release kernel without any modifications (i.e., fault injection). Is it an l4v-related safety measure or is there actually a realistic condition that leads to this situation?

Also, the comment in the code seems to suggest such a precondition, but I have hard time making sense of it.

    /* this may happen, e.g. the caller tries to map a pagetable in
    * newly created PD which has not been run yet. Guard against them! */
    if (mask != 0) {