Below tables list our plans for various parts of seL4 and Data61-supported parts of its ecosystem.
Where we indicate that the feature will appear in master, it might possibly appear in a branch earlier. Features in branches will be merged into mainline at a later time, timing of this is determined by the verification schedule. The reason is our commitment to ensuring that at any time, mainline code for our verified platforms is actually verified. This means that a feature can only be pushed into mainline if it doesn't break the verified platform proofs. In some cases this is no problem, e.g. as long as we haven't completed verification of x86, then changes that only affect x86 can go into mainline (as long as the verifiers agree that they will not inhibit future verification). This is the main reason why the real-time scheduling features will remain in a branch for some time – they are relatively invasive and break many existing proofs.
Some features are in branches because they are of an experimental nature, and are released to the community to allow people to experiment with them, we will do the same. This means that such experimental branches may undergo significant changes on their way into mainline, if they ever make it there.
Features that are in progress are currently being worked on, features that are planned have not yet had work started on them.
Any dates are indicative and subject to change!
In many cases, we could possibly deliver earlier if we had enough people to do the work. If our recruiting is more successful than expected, we might be able to go faster. If you want to help accelerate this roadmap, help us to find the right developers!
|delivered in||Q2’16||ARMv8 support (32-bit only)||master|
|delivered in||Q2'16||ARM virtualisation support complete||master|
New scheduling model (supporting mixed-criticality real-time scheduling)
Note: API changes!
|delivered in||Q3'16||64-bit support for x86 (x64 support)||master|
|delivered in||Q4'16||full virtualisation support for x86 (32-bit)||master|
|delivered in||Q4’16||Multicore support for x86||master|
|delivered in||Q4’16||Multicore support for x64||master|
|delivered in||Q2’17||Multicore support for ARM||master|
|delivered in||Q2’17||64-bit support for ARM (full ARM v8)||master|
|delivered in||Q2’18||RISC-V prototype support||master|
|in progress||64-bit ARM virtualisation support||branch|
|in progress||Support for strict temporal partitioning (timing-channel protection)
Note: API changes!
|planned||Multicore for 64-bit ARM and x64||master|
|planned||SMP-capable virtual-machine monitor (VMM)||master|
|delivered in||Q3’16||CAmkES support for seL4 real-time scheduling model||master|
|delivered in||Apr’17||ARM virtualisation support
(excluding system MMU)
|on schedule||Q2’18||New scheduling model||master|
|in progress||soon||x64 support
(excluding virtualisation support)
|delivered on||Q2’16||Generation of RPC glue-code and capDL proofs||master|