The first level time-sliced domain scheduler is a nice fit for some real-time applications, but the limitation of having each thread belong to only one domain complicates the system when a server cannot belong to multiple domains.  While it is clear that the seL4 information flow proof depends on this restriction , it is not clear how dire relaxing this restriction would be to the main proof.
For example, if the restriction was relaxed so that a thread could belong to up to MAX_DOMAINS_PER_THREAD domains, and the information flow proof was declared to only be valid for cases where this value was set to 1, what level of proof effort would be required to reestablish the functional correctness of this scheduling change?
Hoping that someone might have a quick, reasonable guess, since the verification effort of MCS seems to be touching on a similar area.
 Q. Kang, C. Yuan, X. Wei, Y. Gao and L. Wang, “A User-Level Approach for ARINC 653 Temporal Partitioning in seL4,” 2016 International Symposium on System and Software Reliability (ISSSR) , Shanghai, 2016, pp. 106-110, doi: 10.1109/ISSSR.2016.025.
 T. Murray et al ., “seL4: From General Purpose to a Proof of Information Flow Enforcement,” 2013 IEEE Symposium on Security and Privacy , Berkeley, CA, 2013, pp. 415-429, doi: 10.1109/SP.2013.35.