Fwd: Reiserfs 4

Fwd: Reiserfs 4

[Bhikkhu Mettavihari]

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

Re: Fwd: Reiserfs 4

[doiggl]

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

Re: Reiserfs 4

[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.


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

Re: Reiserfs 4

[†]

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

Re: Reiserfs 4

[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 

Re: Reiserfs 4

[Christian Stroetmann]

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

Re: Reiserfs 4

[Daniel Horne]

> 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

Re: Reiserfs 4

[†]

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

Re: Reiserfs 4

[Daniel Horne]

> 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 

Re: Reiserfs 4

[Daniel Horne]

> 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 

Re: Reiserfs 4

[Christian Stroetmann]

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