1. 任务分类 #
原始的seL4中只有线程的概念，根据特权级可分为：
- 用户态的线程：执行用户态任务，由内核直接调度，不具有并发能力。
- 内核态的线程：执行内核态任务（如系统调用、异常等）。 ReL4在seL4的基础上，扩充了任务的种类。在用户台与内核态分别引入协程的概念，以增强系统的并发性。
- 用户态的协程：执行用户态的异步任务，由用户态的异步运行时调度，具有并发能力。
- 内核态的协程：执行内核态的异步任务（这里主要指异步系统调用），由内核态的异步运行时调度。
2. 任务调度 #
由于引入了协程，需要额外的运行时来对其进行调度。这里将分别讨论用户态调度与内核态调度。
2.1 用户态调度 #
我们在用户态引入协程调度器，从用户态的角度来看，它是基于优先级的轮询调度器。他在内部维护了一个优先级队列，协程按照优先级从高到低排列，相同优先级协程根据添加时间顺序排列。用户态线程将异步运行时初始化完成之后将执行整个事件循环，不断从任务队列中取出任务并执行。
2.2 内核态调度 #
我们在内核态实现了类似用户态的协程调度器，但与用户态不同的是，内核态本身还有一个线程调度器，内核态也无法始终执行整个事件循环。因此我们对内核态协程的调度时机进行了额外的设计。 内核态本身的线程调度器是根据线程的优先级来进行调度，因此我们内核的协程调度时机不能违背了所在线程的优先级调度规则。因此我们为每一个CPU核心引入执行优先级的概念，主要分为三类：
- idle core：空闲CPU核心，执行优先级最低。
- User thread core：正在执行用户态线程的CPU核心，执行优先级等于对应的线程优先级。
- Kernel thread core：正在处理中断或异常的core，执行优先级最高。 内核态的协程优先级被设置为提交异步系统调用的线程的优先级，当协程优先级高于某一个CPU core的执行优先级时，协程调度器将抢占该core并执行事件循环。
3. 任务抢占 #
ReL4的任务抢占主要分为两类：外部中断抢占与优先级抢占：
- 外部中断抢占：当外部中断到来时，如果CPU处于内核态的非抢占点时，将不可被抢占，当处于可抢占点时会被抢占并处理中断。如果CPU处于用户态，用户态任务将被抢占，并处理对应的中断信号。
- 优先级抢占：
- 用户态协程与内核协程：协程之间的优先级抢占是在同一个协程调度器内部。
- 用户态线程：用户态线程之间的优先级抢占是由时钟中断触发并由线程调度器内部的线程进行抢占。
- 内核线程：内核不支持优先级抢占，仅在可抢占点允许被外部中断抢占。
Interface #
- seL4_TCB_Suspend/seL4_TCB_Resume ：暂停/重启线程
- seL4_TCB_SetAffinity: 设置线程亲和性
- seL4_TCB_SetPriority：设置线程优先级
- reL4_coroutine_spawn_with_prio: 创建新的优先级协程
- reL4_coroutine_wake：唤醒协程
- reL4_coroutine_run_until_complete：调度协程
- reL4_wake_syscall_handler：唤醒内核协程