Hi Tim,
the easy ones first: experimental is not verified. We do plan to verify the real-time patches eventually, but that may be a larger project.
The verified version of seL4 is in the master branch and only ARM/kzm in that branch is currently verified. Verification is being kept up to date on an ongoing basis: any change to that code in master goes through formal verification before it is accepted on that branch. The proofs are part of the regression test, so we can see the proof outcome for every commit.
Our process for ongoing seL4 development (somewhat idealised) depends on where development and changes are coming from:
1) new experimental research ideas, exploration, proofs of concepts, prototypes, student projects etc: these usually go on their own branch and can develop however they want with whatever quality level is appropriate for the project. The default for them is not to be merged back into master. Some of them will make it on the experimental branch after review and testing and discussion with the core kernel team. The experimental branch loosely speaking is the collection of patches that the kernel team thinks should be going into master eventually if we had infinite resources. Some of the features on experimental will make it on to master and be formally verified after review and discussion with the verification team. This is mostly a question of prioritising what is most urgent/important traded off against how much work it is going to be to verify and who is around to do it. E.g. a small easy change might make it into master quickly, larger changes usually need planning, discussion, and resources.
2) new platform ports: these often can go directly on master if they are mature enough (after review and testing), and if they do not affect the verified platform (ARMv6/kzm). They will be merged into experimental.
3) code changes invisible to the verification, documentation, build system tweaks etc: these are similar to new platform ports. Changes in the asm and boot code are invisible to the verification, as are changes to other platforms (e.g. x86). The easiest way to tell is to build the fully preprocessed kernel_all.c_pp for ARMv6/kzm. If there diff is empty, verification won’t see the change. The change may still be correctness critical (asm or boot code), so review and testing requirements there will be fairly strict.
4) optimisations and smaller changes to verified code would usually be discussed with the verification team to see if they really are small and low effort. If the verification team agrees that they are and that someone has time to spend a day or so, the change would go on a small branch off master, be verified directly and merged in. Otherwise they are treated as in 1).
Cheers, Gerwin
On 5 Aug 2014, at 5:14 am, Tim Newsham tim.newsham+sel4@gmail.com wrote:
A question I had about how the sel4 project is run internally: What is your process of developing ongoing changes and how does verification fit into it? Do you maintain the proofs with kernel modifications on an ongoing basis? On a semi-regular basis?
Is the "experimental" branch verified? When time slices are no longer global, will those changes be verified? etc...
Tim
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.