* Fwd: Reiserfs 4 [not found] <CAMRsyOdq8mTCtxGH0h1m4pTOKZoGvk+N0aG4ADSFBx5qSHmUAw@mail.gmail.com> @ 2014-07-20 3:10 ` Bhikkhu Mettavihari 2014-07-20 9:30 ` doiggl 2014-07-20 15:42 ` dimas 0 siblings, 2 replies; 11+ messages in thread From: Bhikkhu Mettavihari @ 2014-07-20 3:10 UTC (permalink / raw) To: reiserfs-devel Greetings I am running about 30 ubuntu desktops and servers. I am a regular reiserfs 3.6 user These are production machines doing video editing Our entire production is on Linux Our entire backup in on Linux servers. The fs on the backup servers is though ext3 since the guy that did the server setup was not familiar with riser. When do you recommend me to upgrade to riser 4 I do not like to upgrade if there is not a stable system, then I would rather run with 3.6 with metta Mettavihari ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Fwd: Reiserfs 4 2014-07-20 3:10 ` Fwd: Reiserfs 4 Bhikkhu Mettavihari @ 2014-07-20 9:30 ` doiggl 2014-07-20 15:42 ` dimas 1 sibling, 0 replies; 11+ messages in thread From: doiggl @ 2014-07-20 9:30 UTC (permalink / raw) To: Bhikkhu Mettavihari; +Cc: reiserfs-devel On Sun, 20 Jul 2014 08:40:24 +0530, Bhikkhu Mettavihari <tv.lists@gmail.com> wrote: > Greetings > > I am running about 30 ubuntu desktops and servers. > I am a regular reiserfs 3.6 user > These are production machines doing video editing > Our entire production is on Linux > Our entire backup in on Linux servers. > The fs on the backup servers is though ext3 since the guy that did the > server setup was not familiar with riser. > > When do you recommend me to upgrade to riser 4 > > I do not like to upgrade if there is not a stable system, then I would > rather run with 3.6 > > with metta > Mettavihari > -- > To unsubscribe from this list: send the line "unsubscribe reiserfs-devel" > in > the body of a message to majordomo@vger.kernel.org > More majordomo info at http://vger.kernel.org/majordomo-info.html Hello, my opinion only. Since this production [1] stick with 3.6 series, ensure you have the latest revision of 3.6 series. --Glenn [1] "These are production machines doing video editing" other links: http://en.wikipedia.org/wiki/ReiserFS http://askubuntu.com/questions/99834/how-do-you-see-what-packages-are-available-for-update ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Reiserfs 4 2014-07-20 3:10 ` Fwd: Reiserfs 4 Bhikkhu Mettavihari 2014-07-20 9:30 ` doiggl @ 2014-07-20 15:42 ` dimas 2014-07-21 9:09 ` † 1 sibling, 1 reply; 11+ messages in thread From: dimas @ 2014-07-20 15:42 UTC (permalink / raw) To: reiserfs-devel if you mean backup storage, why do you need such a complicated journaled fs like ext3 or r4? for mostly static storage, modified once a day or even rarer, i'd suggest ext2 as a simplest way. 2014-201 08:40 Bhikkhu Mettavihari <tv.lists@gmail.com> wrote: > The fs on the backup servers is though ext3 since the guy that did the > server setup was not familiar with riser. > > When do you recommend me to upgrade to riser 4 ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Reiserfs 4 2014-07-20 15:42 ` dimas @ 2014-07-21 9:09 ` † 2014-07-21 20:26 ` Daniel Horne 0 siblings, 1 reply; 11+ messages in thread From: † @ 2014-07-21 9:09 UTC (permalink / raw) To: reiserfs-devel 20.07.2014 17:42, dimas пишет: > if you mean backup storage, why do you need such a complicated journaled fs > like ext3 or r4? for mostly static storage, modified once a day or even rarer, > i'd suggest ext2 as a simplest way. > That's the worst possible recommendation: if you don't want to use journal you can just switch it off on ext4. Using outdated ext2 code offers absolutely no advantages. 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 ;-) cheers, Max. -- To unsubscribe from this list: send the line "unsubscribe reiserfs-devel" in the body of a message to majordomo@vger.kernel.org More majordomo info at http://vger.kernel.org/majordomo-info.html ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Reiserfs 4 2014-07-21 9:09 ` † @ 2014-07-21 20:26 ` Daniel Horne 2014-07-22 12:11 ` Christian Stroetmann 0 siblings, 1 reply; 11+ messages in thread From: Daniel Horne @ 2014-07-21 20:26 UTC (permalink / raw) To: reiserfs-devel > 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 ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Reiserfs 4 2014-07-21 20:26 ` Daniel Horne @ 2014-07-22 12:11 ` Christian Stroetmann 2014-07-22 13:48 ` Daniel Horne 2014-07-22 13:54 ` † 0 siblings, 2 replies; 11+ messages in thread From: Christian Stroetmann @ 2014-07-22 12:11 UTC (permalink / raw) To: Linux Reiserfs Devel Am 21.07.2014 22:26, schrieb Daniel Horne: > >> 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 > -- I promised not to sent any messages to this maling-list anymore, but this is an exception because the work of my company and me is directly addressed in a way that might mislead members of this mailing-list and the broader public and also might have been an attack on our reputation. FYI, I would like to mention the following points, though only point 1. and point 2. might be of interest for R4 developers and followers: 1. The general concept about a formally verified R4 was already made in the November 2006 with the start of OntoLinux [1] (see its characteristics on the webpage Overview [2]). At that time, the OntoFS [3] was based on R4. 2. Actually, OntoLinux is also based on the L4 microkernel (see the first section of the webpage Components [4] and its section OntoL4 [5]). Hence, to use a formally verified L4 microkernel was suggested and planned with OntoLinux even before the National Information and Communications Technology Centre of Excellence Australia (NICTA) conducted the formal verification of its L4 variant with only "7,500 lines of C code" in the October of 2009 (its case has been investigated by us and documented on OntomaX [6]). There are other issues related with the L4 variant of NICTA that I do not want to discuss here. But the similarities between our works are no surprise. 3. HiLog is included in the OntoBot component [7] by XSB [8] that permits limited High-Order Logic (HOL) programming, though HOL is not needed at all due to the rewriting logic of Maude [9] included as well in the OntoBot. 4. The generic proof assistant Isabelle [10] with its instance Isabelle/HOL was added to the section Formal Verification of the webpage Links to Software [11] with the OntoLinux Website update of the 23th of August.2009 (see the related message on OntomaX [12]). 5. OntoFS is not based on R4 anymore since quite some time now, but on OntoBase [13]. Last but not least, I am sure that pen-and-paper was the method at that time, if a proof was done at all. Have fun with (Onto)logics Christian Stroetmann [1] OntoLinux www.ontolinux.com [2] OntoLinux - Overview www.ontolinux.com/technology/overview.htm [3] OntoLinux - OntoFS www.ontolinux.com/technology/ontofs.htm [4] OntoLinux - Components www.ontolinux.com/technology/components.htm [5] OntoLinux - Components - OntoL4 www.ontolinux.com/technology/components.htm#ontol4 [6] OntomaX - News - 2009 - August www.ontomax.com/newsarchive/2009/august.htm21.August.2009 [7] OntoLinux - Components - OntoBot www.ontolinux.com/technology/components.htm#ontobot [8] XSB xsb.sourceforge.net/ [9] Maude maude.cs.uiuc.edu/ [10] Isabelle www.cl.cam.ac.uk/research/hvg/Isabelle/ [11] Links to Software - Formal Verification www.ontolinux.com/community/software.htm#formalverification [12] OntomaX - News - 2009 - August www.ontomax.com/newsarchive/2009/august.htm#23.August.2009 [13] OntoLinux - OntoBase www.ontolinux.com/technology/ontobase/ontobase.htm ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Reiserfs 4 2014-07-22 12:11 ` Christian Stroetmann @ 2014-07-22 13:48 ` Daniel Horne 2014-07-22 15:17 ` Christian Stroetmann 2014-07-22 13:54 ` † 1 sibling, 1 reply; 11+ messages in thread From: Daniel Horne @ 2014-07-22 13:48 UTC (permalink / raw) To: Linux Reiserfs Devel > I promised not to sent any messages to this maling-list anymore, but this > is an exception because the work of my company and me is directly > addressed in a way that might mislead members of this mailing-list and the > broader public and also might have been an attack on our reputation. It wasn't intended as such - I'm new to the field of formal verification and wasn't aware of this work. Thanks for the information, though. I'll read through those links. -- DH ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Reiserfs 4 2014-07-22 13:48 ` Daniel Horne @ 2014-07-22 15:17 ` Christian Stroetmann 0 siblings, 0 replies; 11+ messages in thread From: Christian Stroetmann @ 2014-07-22 15:17 UTC (permalink / raw) To: Daniel Horne; +Cc: Linux Reiserfs Devel On the 22nd of July 2014 15:48, Daniel Horne wrote:: >> I promised not to sent any messages to this maling-list anymore, but >> this is an exception because the work of my company and me is >> directly addressed in a way that might mislead members of this >> mailing-list and the broader public and also might have been an >> attack on our reputation. > > It wasn't intended as such - I'm new to the field of formal > verification and wasn't aware of this work. > > Thanks for the information, though. I'll read through those links. > > -- > DH > I do apologize for any harsh statement. To the subject of formal verification: This is a highly complex task and if it makes sense to formally verify R4 has to be approached from several sides: 1. Is R4 in a state that it is matured enough? 2. File systems for general use are a little bit different than the L4 microkernel, so the complexity that has to be verified might be higher. 3. Is the environment verified as well, for example the operating system kernel of Linux? Actually, I do not know if it makes sense to do it, but if you attempt it, then I will have a look on your results. Best regards Christian Stroetmann ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Reiserfs 4 2014-07-22 12:11 ` Christian Stroetmann 2014-07-22 13:48 ` Daniel Horne @ 2014-07-22 13:54 ` † 2014-07-22 15:08 ` Daniel Horne 2014-07-22 15:08 ` Daniel Horne 1 sibling, 2 replies; 11+ messages in thread From: † @ 2014-07-22 13:54 UTC (permalink / raw) To: Linux Reiserfs Devel 22.07.2014 14:11, Christian Stroetmann пишет: > > > 1. The general concept about a formally verified R4 was already made in the > November 2006 with the start of OntoLinux [1] (see its characteristics on the > webpage Overview [2]). At that time, the OntoFS [3] was based on R4. Could you provide links to actual verification or source code? All I've managed to find there is some marketing junk from the company I've never heard about before. On a related note - I think formally verified R4 is great idea but you've got to be aware that as long as it's running on top of unverified Linux kernel we can only assure that some properties hold under the assumption that kernel actually does the right thing. Not sure how practically viable it is outside of general academic curiosity. cheers, Max. -- To unsubscribe from this list: send the line "unsubscribe reiserfs-devel" in the body of a message to majordomo@vger.kernel.org More majordomo info at http://vger.kernel.org/majordomo-info.html ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Reiserfs 4 2014-07-22 13:54 ` † @ 2014-07-22 15:08 ` Daniel Horne 2014-07-22 15:08 ` Daniel Horne 1 sibling, 0 replies; 11+ messages in thread From: Daniel Horne @ 2014-07-22 15:08 UTC (permalink / raw) To: Linux Reiserfs Devel > On a related note - I think formally verified R4 is great idea but you've > got to be > aware that as long as it's running on top of unverified Linux kernel we > can only > assure that some properties hold under the assumption that kernel actually > does the > right thing. Not sure how practically viable it is outside of general > academic curiosity. True enough. The SeL4 verification apparently took on the order of a few manyears, and we don't have that. I do think, however, there's likely to be value in incomplete efforts. I personally know that I've had bugs in my code that I've spent a couple of days trying to iron out, only to find that when I stop and write out hoare triples for each of the statements in the code I find the issue in about ten minutes. We can start with a highly abstract model and gradually introduce more details while establishing that each more detailed model doesn't invalidate proofs made on more general ones. Having a proven yet highly abstract model to informally compare the actual source to would make debugging quite a bit easier, I think, and we could gradually build on it to reduce the semantic "distance" between the model and the kernel code. -- DH ^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Reiserfs 4 2014-07-22 13:54 ` † 2014-07-22 15:08 ` Daniel Horne @ 2014-07-22 15:08 ` Daniel Horne 1 sibling, 0 replies; 11+ messages in thread From: Daniel Horne @ 2014-07-22 15:08 UTC (permalink / raw) To: Linux Reiserfs Devel > On a related note - I think formally verified R4 is great idea but you've > got to be > aware that as long as it's running on top of unverified Linux kernel we > can only > assure that some properties hold under the assumption that kernel actually > does the > right thing. Not sure how practically viable it is outside of general > academic curiosity. True enough. The SeL4 verification apparently took on the order of a few manyears, and we don't have that. I do think, however, there's likely to be value in incomplete efforts. I personally know that I've had bugs in my code that I've spent a couple of days trying to iron out, only to find that when I stop and write out hoare triples for each of the statements in the code I find the issue in about ten minutes. We can start with a highly abstract model and gradually introduce more details while establishing that each more detailed model doesn't invalidate proofs made on more general ones. Having a proven yet highly abstract model to informally compare the actual source to would make debugging quite a bit easier, I think, and we could gradually build on it to reduce the semantic "distance" between the model and the kernel code. -- DH ^ permalink raw reply [flat|nested] 11+ messages in thread
end of thread, other threads:[~2014-07-22 15:17 UTC | newest] Thread overview: 11+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- [not found] <CAMRsyOdq8mTCtxGH0h1m4pTOKZoGvk+N0aG4ADSFBx5qSHmUAw@mail.gmail.com> 2014-07-20 3:10 ` Fwd: Reiserfs 4 Bhikkhu Mettavihari 2014-07-20 9:30 ` doiggl 2014-07-20 15:42 ` dimas 2014-07-21 9:09 ` † 2014-07-21 20:26 ` Daniel Horne 2014-07-22 12:11 ` Christian Stroetmann 2014-07-22 13:48 ` Daniel Horne 2014-07-22 15:17 ` Christian Stroetmann 2014-07-22 13:54 ` † 2014-07-22 15:08 ` Daniel Horne 2014-07-22 15:08 ` Daniel Horne
This is an external index of several public inboxes, see mirroring instructions on how to clone and mirror all data and code used by this external index.