Below tables list our target dates for various parts of seL4 and Data61-supported parts of its ecosystem.
Where status is deferred, this relates to previously published version of this roadmap; in such a case, the date given here is our present (as of December 2016) estimate when we will deliver the feature.
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.
All 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|
|deferred to||Q1’17||Multicore support for ARM||master|
|deferred to||Q2’17||Support for strict temporal partitioning (timing-channel protection)
Note: API changes!
|deferred to||Q2’17||64-bit support for ARM (full ARM v8)||master|
|deferred to||Q2’17||Multicore for 64-bit ARM and x64||master|
|deferred to||Q2’17||SMP-capable virtual-machine monitor (VMM)||master|
|delivered on||Q3’16||CAmkES support for seL4 real-time scheduling model||master|
|on schedule||Apr’17||ARM virtualisation support
(excluding system MMU)
|on schedule||Apr’17||x64 support
(excluding virtualisation support)
|on schedule||Q2’18||New scheduling model||master|
|delivered on||Q2’16||Generation of RPC glue-code and capDL proofs||master|