Speaking of reiser4, unfortunately I would not expect it to be
recommendable as a
viable production-ready upgrade path for 3.6 in the near future. Sadly,
there's just
not enough resources backing up development at the moment. Feel free to
change that
though ;-)
I wonder if there would be any interest in a project to formally verify
Reiser4? I mean, who needs a lot of testing effort when you've got a machine
checked proof.
SeL4, for example, is a microkernel of ~84000 lines iirc, and had its major
correctness criterion proved through the isabelle/HOL theorem prover.
Reiser4 is on the same order of magnitude in terms of lines of code, so
could possibly be proven in roughly the same amount of effort. We could
probably restrict the scope of a verification project to the consistency of
the on-disk store to start with, and add in other correctness criteria (such
as deadlock avoidance) later.
I recall hans saying that he'd proven the leaf-first locking scheme of
reiser4 - Did he do this as an informal pen-and-paper proof, or is there a
proof script for a proof assistant lying around somewhere?
--
DH
--
To unsubscribe from this list: send the line "unsubscribe reiserfs-devel" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html
