Re: Reiserfs 4

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

 




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




[Index of Archives]     [Linux File System Development]     [Linux BTRFS]     [Linux NFS]     [Linux Filesystems]     [Ext4 Filesystem]     [Kernel Newbies]     [Share Photos]     [Security]     [Netfilter]     [Bugtraq]     [Yosemite Forum]     [MIPS Linux]     [ARM Linux]     [Linux Security]     [Linux RAID]     [Samba]     [Device Mapper]     [Linux Resources]

  Powered by Linux