scheduler syscall requirements

Hi.

I am interested in scheduling for L4 so I had a look
at the source of Scheduler syscall in Pistachio and wondered
how the scheduler and its scheduled thread
necessarily should be in the same address space.

pistachio/kernel/src/api/v4/schedule.cc

609     // are we in the same address space as the scheduler of the thread?
610     tcb_t * sched_tcb =
get_current_space()->get_tcb(dest_tcb->get_scheduler());
611     if (sched_tcb->get_global_id() != dest_tcb->get_scheduler() ||
612          sched_tcb->get_space() != get_current_space())
613     {
614          get_current_tcb ()->set_error_code (ENO_PRIVILEGE);
615          return_schedule(0, 0);
616     }

For me it restricts the opportunities for scheduling
policy and the manageability for program systems on
top of L4.

Also nothing is mentioned about these requirements
in "L4 kernel reference manual".

Is there any reasonable explanation for this?

BTW, there is no checking that Scheduler syscall invoked
by thread registered as scheduler for destination thread, and
proposed priority less than current thread's. It seems easy to fix,
so maybe it provided deviation?
Thanks.
Al.