We are writing some code for the seL4_libs where a recursive function makes the most sense. I know that part of the code is not verified, but it got me curious as to whether the seL4 proofs could handle recursive functions.
It can, yes.
The more abstract proof levels in Isabelle/HOL make natural use of recursion all the time (lists etc), and the C level also supports recursion. There is even an in-kernel function that is nominally recursive that makes use of that; the maximum recursion depth in that case is only 3, but it looks as recursive to the verification environment as a “real” recursive function.
I’m coming back to this thread to confirm the maximum depth of recursion currently within the seL4 microkernel. I haven’t found a recursion of depth 3 mentioned by Gerwin.
The obvious one is the recursive deletion of a container (CNode/TCB), which I believe has a maximum recursive depth of 1:
cteDelete → finaliseSlot → reduceZombie → cteDelete → finaliseSlot → reduceZombie → cteSwapForDelete (breaks recursion)
Also mentioned in the Blackham_SCRH_11 paper,
“The formal proof guarantees termination, proving that the functions do not call themselves more than once.”
meaning the recursive depth does not exceed 1.
So where is the recursion with a depth of 3?
It is perfectly possible that the depth in C is just 1 – some of the functions are consolidated in the spec into one larger function, so the depth there is larger (e.g. reduceZombie is just a case of cteDelete in the spec – that is probably all there is, because that gets you to 3).
1 Like