MIT's New File System Won't Lose Data During Crashes 168
jan_jes sends news that MIT researchers will soon present a file system they say is mathematically guaranteed not to lose data during a crash. While building it, they wrote and rewrote the file system over and over, finding that the majority of their development time was spent defining the system components and the relationships between them. "With all these logics and proofs, there are so many ways to write them down, and each one of them has subtle implications down the line that we didn’t really understand." The file system is slow compared to other modern examples, but the researchers say their formal verification can also work with faster designs. Associate professor Nickolai Zeldovich said, "Making sure that the file system can recover from a crash at any point is tricky because there are so many different places that you could crash. You literally have to consider every instruction or every disk operation and think, ‘Well, what if I crash now? What now? What now?’ And so empirically, people have found lots of bugs in file systems that have to do with crash recovery, and they keep finding them, even in very well tested file systems, because it’s just so hard to do.”
But is it useful? (Score:5, Interesting)
slow compared to other modern examples, but the researchers say their formal verification can also work with faster designs
If we can accept 'slow', it's not that difficult to build an always consistent filesystem. While they can formally verify a faster design should one exist, there remains the question of whether it's possible to be formally proven to be resilient to data loss while taking some of the utterly required performance shortcuts for acceptable performance. I suspect the answer is that some essential performance 'shortcuts' will fail that verification.
Re: (Score:2)
If we can accept 'slow', it's not that difficult to build an always consistent filesystem.
citation required
Re:But is it useful? (Score:5, Funny)
A sufficiently slow writing filesystem is indistinguishable from a read-only filesystem. Read-only filesystems are consistent. Therefore, a slow enough writing filesystem is consistent.
For more serious analysis of crash-resistant write sequences, look elsewhere in this discussion.
Re: (Score:2)
what does this phrase even mean? why does speed or slowness matter? you can play the video of a disk disaster at any speed you want
Real-time (Score:2)
what does this phrase even mean? why does speed or slowness matter?
Speed means the ability to finish reading and writing all data associated with a job before the job's soft real-time deadline has expired.
Re: (Score:1)
before the job's soft real-time deadline has expired.
what does this have to do with anything?
Re: (Score:2)
If reading or writing files in a particular file system is slow enough that it makes applications painful to use, the file system won't pass into widespread use.
Re: (Score:2)
And yet the FAT16 file system was popular for a very long time.
Re: (Score:2)
If we can accept 'slow', it's not that difficult to build an always consistent filesystem.
citation required
Sheesh, do we have to do the Googling for you [wikipedia.org]?
Re: (Score:2)
Write a block to the storage device.
Apply all necessary flush and synchronization commands, and a few unnecessary ones.
Power off the storage device.
Power the device back on.
Read back the block to ensure it was actually written.
Repeat as necessary until block is confirmed as having been written.
Continue with block number two...
Well it won't lose data... (Score:2)
... until they find a logical flaw in their proofs or the bugs in mechanical verifier(s) that helped them prove the driver correct.
Re: (Score:1, Interesting)
Or – more likely – until they find a flaw in their assumptions, like a lower-level software stack that swears "yes, this data has been committed to storage" slightly before that's actually true.
Re: (Score:2)
That is pretty unlikely, but the whole thing is a worthless stunt anyways. The problem is that they have to use some hardware model and that will have errors. Hence the assurances they claim are purely theoretical, and in practice their thing may well be less reliable than a well-tested file system with data-journal, like ext3.
Proving Coq itself (Score:1)
formal proof using Coq
How do you prove Coq is correct, that it doesn't have a Ken Thompson bug (see "Reflections on Trusting Trust") causing a false positive on proof of Coq's own correctness? Is there an independently written implementation of Coq's proof language suitable for David A. Wheeler's "diverse double-compiling" method? And how do you prove that the hardware on which Coq is run doesn't have a flaw that affects Coq's correctness?
Re:Proving Coq itself (Score:5, Interesting)
Re: (Score:2)
How do you prove Coq is correct
You use the formal proof assistant Pusi to prove it correct. So what you do is feed Coq into Pusi, and then nine months later the proof drops out.
Formally verified system fails (Score:3, Funny)
MIT's new "crash-proof file system" crashed today amid accusations of bugs in the formal proof verification software used to formally verify it.
MIT are now working on a formal verification of the formal verification system, in order to avoid similar formal-verification-related problems in the future.
Re: (Score:2)
MIT's new "crash-proof file system" crashed today amid accusations of bugs in the formal proof verification software used to formally verify it.
So the whole thing was a bit of a Coq-up?
Linux File Systems (Score:5, Interesting)
I find some of the current file systems to be adequately reliable. Even their performance is acceptable. But, the Linux systems are lacking.
Is there a reliable Linux file system such as EXT4 that has an easy to use copy on write(CoW) feature to allow instant recovery of any file changed at any time?
rm ./test ./
restore --last test
dd if=/dev/random of=./test bs=1M count=10 ./
restore --datetime test
Novell Netware FS did all this and more in 1995 FFS! Fifteen years later and Linux doesn't seem to be able to do this. NTFS doesn't seem to be able to do this either. Yet Novell is dead?
Re: (Score:2, Informative)
Well, ex-Googler Kent Overstreet recently announced a COW filesystem on lkml:
https://lkml.org/lkml/2015/8/21/22
Not ready for production I would say, but looks interesting.
Re:Linux File Systems (Score:5, Interesting)
I still think Netware's filesystem permission model was better than anything out there now, at least for filesharing.
The feature I miss the most is allowing traversal through a directory hierarchy a user has no explicit permissions for to get to a folder they do have permissions for. I find the workarounds for this in other filesystems to be extremely ugly.
I think NDS was better in a lot of ways than AD, although it would have been nice if there had been something better than bindery mode for eliminating the need for users to know their fully qualified NDS name.
I also kind of wish TCP/IP had used the network:mac numbering scheme that IPX used. The rest of IPX/SPX I don't need, but there'd be no talk of address exhaustion of IPv4 if that scheme had been adopted, little need for DHCP address assignment and the addressing scheme would scale to the larger broadcast domains enabled by modern switching (avoiding the need to renumber legacy segments completely when they exhausted a /24 space and expansion via mask reduction wasn't possible due to linear numbering on adjacent segments).
chmod 751 some_directory (Score:5, Informative)
The feature I miss the most is allowing traversal through a directory hierarchy a user has no explicit permissions for to get to a folder they do have permissions for. I find the workarounds for this in other filesystems to be extremely ugly.
In POSIX, that's represented in a directory's mode bits with octal digit 1 (4: list files, 2: create or delete files, 1: traverse). What do you find ugly about mode 751 (owner create or delete, owner and group list, world traverse)?
I also kind of wish TCP/IP had used the network:mac numbering scheme that IPX used.
It does now. An IPv6 address is divided into a 48- or 56-bit network, a 16- or 8-bit subnet, and a 64-bit machine identifier commonly derived from the MAC.
Re: (Score:2)
Well, for example, I can think of a situation for: create, NOT delete, NOT modifiy, NOT read. If there is a shared area where people are putting resumes, or other submissions. You don't want htem to affect or compete with one already there. Nor read the others.
I can see a log file you can append-only to.
There's a lot of interesting cases if the permissions are cut fine enough.
Re:Linux File Systems (Score:4, Interesting)
Bah, forget NetWare, VINES and StreetTalk did everything you ask for and then some way before NDS was even a thought.
VINES' ACL's were beautifully granular ...
Re: (Score:2)
Bah, forget this newfangled crap, Multics was doing this half a century ago [multicians.org] (which includes use of RAID tape drives, checkpointing, ACLs, and other recent innovations).
Re: (Score:3)
It's a kludge, though, in NTFS, in Netware it just worked.
IPX/SPX as a layer 3 protocol isn't what I wanted, I wanted TCPv4 with a network prefix and the MAC as the node address. Clients could derive their address automatically from network traffic by picking up the network address from the wire and they already knew their MAC address.
Although to be honest, IPX/SPX even as a secondary protocol wasn't that bad to support in a mixed environment. We had no issues with TCP, IPX *and* CrappleTalk on 512k frame
Re: (Score:2)
How is it a kludge? You have the option in NTFS of having that everyone:traverse permission propogating through the directory heirarchy, but it isnt required. It sounds like Netware just assumes that traversal rights are implicit, where there may be scenarios where it is not desired.
Re: (Score:2)
I wanted TCPv4 with a network prefix and the MAC as the node address. Clients could derive their address automatically from network traffic by picking up the network address from the wire and they already knew their MAC address.
You mean more or less exactly what IPv6 does (in many cases)?
Re: (Score:3)
It still is: https://dl.netiq.com/Download?... [netiq.com]
I build multi-million user IAM systems on it for a living.
Re:Linux File Systems (Score:4, Interesting)
I find some of the current file systems to be adequately reliable. Even their performance is acceptable. But, the Linux systems are lacking.
Is there a reliable Linux file system such as EXT4 that has an easy to use copy on write(CoW) feature to allow instant recovery of any file changed at any time?
NILFS2 [kernel.org] provides continuous point in time snapshots, which can be selectively mounted and data recovered. Not quite as instant recovery as your use case examples, but it's only a few commands/wrapper scripts away.
Re: (Score:2)
nilfs2 does.
Re: (Score:2)
You are looking for NILFS2.
Of course you use more disk because you nothing gets deleted...
Re: (Score:2)
I think your Novell system needs a new clock battery or something...
Re: (Score:3)
Re: (Score:2)
BTRFS stores snapshots in the volume, ZFS stores them in the pool. If y
Re: (Score:2)
Re: Linux File Systems (Score:2)
what is the command to snapshot two zvols atomically?
Re: (Score:2)
It's a matter of distance (Score:3)
Journaled File System? (Score:2)
i thought Journaled file systems already possessed this feature.
Re: (Score:2)
i thought Journaled file systems already possessed this feature.
just like air bags and seat belts have eliminated all deaths on the road
Re: (Score:2)
You need to ensure that blocks are written to the media in the correct order. Or at least that everying before a synchronization point was completely written to the media. But even that is not always true because devices will lie and claim to have flushed data when they have not. So you also need to ensure that your underlying block based device is operating correctly, and that can be tricky when it's a third party device.
Is it really THAT hard? (Score:5, Interesting)
Write zero to a flag.
Write data to temporary area.
Calculate checksum and keep with temporary area.
When write is complete, signal application.
Copy data from temporary area when convenient.
Check checksum from temporary to permanent is the same.
Mark flag when finished.
If you crash before you write the zero, you don't have anything to write anyway.
If you crash mid-write, you've not signalled the application that you've done anything anyway. And you can checksum to see if you crashed JUST BEFORE the end, or half-way through.
If you crash mid-copy, your next restart should spot the temporary area being full with a zero-flag (meaning you haven't properly written it yet). Resume from the copy stage. Checksum will double-check this for you.
If you crash post-copy, pre-flagging, you end up doing the copy twice, big deal.
If you crash post-flagging, your filesystem is consistent.
I'm sure that things like error-handling are much more complex (what if you have space for the initial copy but not the full copy? What if the device goes read-only mid-way through?) but in terms of consistency is it really all that hard?
The problem is that somewhere, somehow, applications are waiting for you to confirm the write, and you can either delay (which slows everything down), or lie (which breaks consistency). Past that, it doesn't really matter. And if you get cut-off before you can confirm the write, data will be lost EVEN ON A PERFECT FILESYSTEM. You might be filesystem-consistent, but it won't reflect everything that was written.
Journalling doesn't need to be mathematically-proven, just logically thought through. But fast journalling filesystems are damn hard, as these guys have found out.
Re:Is it really THAT hard? (Score:5, Insightful)
> When write is complete, signal application.
How do you know the write was complete? Most storage hardware lies about completing the write. The ZFS folks found this out the hard way: their filesystem was supposed to survive arbitrary power failures, and on a limited set of hardware that was true. In reality, most drives/controllers say they've committed the write to disk when it's still in their cache.
Any filesystem that claims to survive crashes needs to take into account that any write confirmation could be a lie, and that any data it has written in the past may still be in a volatile cache.
Re: (Score:3)
You can't expect software to paper over BUSTED HARDWARE. If a disk drive flat out lies about status, expose the goddam manufacturer and sue him out of existence. If you think anyone can paper over the scenario you just outlined, then what about this - what about a disk drive that NEVER WRITES ANYTHING but lies and says everything is going hunky dory? Pretty damn sure there's nothing you can do in that scenario.
I've heard that story about the "drives that lie about about write-to-physical-media-complete" man
Re: (Score:2)
Then the MIT paper ignores reality, and is therefore useless.
You can prove your system is technically correct all you want, but if it doesn't work in the real world (where most hardware lies about write commits), then it's going to work in theory and fail in practice.
If it was easy wouldn't it already be done? (Score:3)
Why am I hearing Jeremy Clarkson asking "how hard can it be?" just before utterly screwing something up?
Perhaps there is just a tad more difficulty to it than you are considering?
Re: (Score:2)
I can never tell if Clarkson is a smart person pretending to be stupid, or a stupid person pretending to be smart. Because a stupid person could never pretend to be that stupid.
He is smart but plays dumb (Score:2)
I can never tell if Clarkson is a smart person pretending to be stupid, or a stupid person pretending to be smart.
I've heard from numerous movie directors that people who play dumb characters actually have to be quite smart. Clarkson isn't stupid (generally) and remember that Top Gear is/was a scripted show and people watch it primarily because it is funny. I think I remember Conan OBrian saying that a lot of comedy is throwing out your dignity and hoping you'll get it back.
Re: (Score:2)
I think you're basically right. I read about an even simpler system. They wanted to prove if a robotic surgical arm, controlled by a multi-axis joystick, would always no matter what move only when the surgeon commanded it.
So basically, you read the joystick position sensor for an axis. You multiply by a coefficient, usually less than 1. You send that number to the arm controller. Arm controller tries to move to that position.
Smooth, linear, no discontinuities...you technically only need to check about
Re: (Score:2)
What on earth makes you think that any algorithm, proof or technique can account for hardware failure of any kind? That's what RAID, etc. are for and are still far from a guarantee.
Plus, kind of the point of a checksum is to ensure the integrity (to a certain probability) of data. If either the checksum or data change, they will no longer match up - short of a billions-to-one random chance that you can't do anything about anyway. Incorporate the flag into the data that you checksum and that's covered.
You
Not exactly new or news... (Score:3)
Re: (Score:2)
But what about disk failure?
this is like expecting your seat belt to keep you safe during the apocalypse
Re: (Score:2)
Re: (Score:2)
"MIT's New File System Won't Lose Data During Crashes" can be read as "MIT's New File System Won't be at fault for lost data once committed during any interruption of writes"
ZFS does the same thing, minus the proofs. If you do a sync write and ZFS says it completed, then that data is not going to be lost due to any fault of ZFS. But what if someone threw all of your harddrives into lava? Again, not the fault of ZFS. Same idea.
Rule of thumb, if your FS needs FSCK,
Re: (Score:2)
I'm wondering if their proof requires the disk to actually write the data in the same order as the filesystem sends write commands to the disk. This is not necessarily true for disks that support command queuing, and certainly not true for SSDs.
RTFA:
"You literally have to consider every instruction or every disk operation"
Re: (Score:2)
Tough environments (Score:2)
Re: (Score:2)
the stars will implode and the universe will come to an end, how would any filesystem survive that?
Re: (Score:2)
Re: (Score:2)
Missile hit?
Re: (Score:2)
You joke, but I've seen IOPS drop in a RAID array because somebody was talking loudly next to the server. It was kind of fun to shout at the server and watch the disk activity drop. For testing purposes, of course.
Re: (Score:2)
Pretty much that. Ours were RAID arrays on Linux, and we induced it without being quite as close as he was, but pretty much the same deal. This was more than ten years ago, so maybe modern disks would handle it better, but it looks like a few years later that guy in your video was still seeing the same behaviour.
Re: (Score:2)
Re: (Score:2)
My wife once worked on a system that was in the next room from the skate sharpener. She'd never seen flames coming out of a hard disk before.
Re: (Score:2)
I remember one time about 10 years ago we got a handful of new HP servers in and were going through the burn-in process. Quite literally, apparently, as one of them had a RAID controller who's capacitors exploded quite violently setting off fire alarms and making us run for fire extinguishers when when we fired it up. (pun intended..).
Re: (Score:2)
Re:Tough environments (Score:4, Interesting)
I personally encountered a drive array driver cause an entire array to get overwritten by garbage. I was quite glad that I had tape backups of the computers and the shared array, so a recovery was fairly easy (especially with IBM sysback.)
Filesystems are one piece of a puzzle, but an important one. If that array decided to just write some garbage in a few sectors, almost no filesystem would notice that, allowing propagating of corrupted data to backups. The only two that might notice it would be a background ZFS task doing a scrub and noticing a 64 bit checksum is off, or ReFS doing something similar. Without RAID-Z2, the damage can't be repaired... but it can be found and relevant people notified.
Re: (Score:2)
Re: (Score:2)
I've seen RAID groups fail sort of violently (granted in some tough environments) where one disk crashed and so did the others next two it. Three out of five disks in a RAID 5 gone. Only option was backup. How would any filesystem survive that?
It is not the responsibility of the file system to maintain data integrity in the face of catastrophic failure of the underlying storage hardware.
Re: (Score:2)
Two General's Problem (Score:1)
I think any file system could be imagined as a simple case of a database system. You "commit" a file change and you must be sure that the change is written to disk before proceeding.
So, any database system has a well know logical limitation named "Two General's Problem"
https://en.wikipedia.org/wiki/Two_Generals%27_Problem
The implication of this is that in a database system you cannot guarantee a fully automated recovery; always there is a remaining possibility that some changes should be roll
Re: (Score:2)
You can never be sure that a write is committed to disk, because most hardware lies about that.
Re: (Score:2)
I suppose you can find authoritative references for that claim, complete with manufacturer names and drive model numbers?
Code not available, will it ever be? (Score:3)
MIT researchers live in ivory towers (Score:5, Insightful)
Beware of bugs in the above code; I have only proved it correct, not tried it. -- Donald Knuth
If the hard drive firmware is not proven, this FS won't be any better than ZFS and others.
Writing safe file systems is the easy part (even trivial using synchronous writes, when you consider their design is "slow").
The impossible part is dealing with firmwares that are known to lie (including pretending than a write is synchronous): how could you not lose data if the drive didn't ever write the data to the platters in the first place ?
Re: (Score:2)
Not impossible. Tell it to write to disk, wait for it to say it has. Then cut power to the drive, wait 30 seconds, reestablish power, then ask for the data back. If it isn't the same, repeat until it is. It'll be slow, and likely kill your drives, but you can be reasonably sure the drive did indeed write the data.
This is standard for mission-critical S/W (Score:2)
The idea of evaluating each step of the program for "what happens if this fails" is standard software engineering technique for mission-critical software. (That't not to say it's always actually done, just that it is the standard.) This method is hardly revolutionary (or even evolutionary.)
Re: (Score:2)
slashdot has truly degenerated into a cesspool when you consider that this drivel is one of the more insightful posts
Re: (Score:2)
The standard doesn't have a name; it's not some useless crap in an ISO catalog, it's just a way truly mission-critical software is built.
I know that NASA has used it for the flight-control computers for the manned space-flight program, and IBM uses it for some of the more vital parts of their mainframe operating systems.
I didn't say it was applicable to everything, just that as a software-engineering technique, it's not at all new.
What's their point? (Score:2)
Any journalling FS should provide a consistent state, checksumming FS like BTRFS or ZFS even provable.
So they won't lose data, which is written and in a consistent state, and unwritten data cannot be saved by definition.
Yeah, right. (Score:5, Interesting)
It reminds me of a story from the late 80s (?) at a tech conference. The makers of a real-time OS with real-time snapshots would periodically pull the plug on their systems, plug it back in and it would resume exactly what it was doing, to the delight and amazement of all the techies in the assistance. In the much larger and much more expensive booth in front of them was a richer vendor. The techies started coaxing them to do the same. After much hand wringing, they did, and after a very long rebuild time the system came back as a mess. Conclusion: the 1st vendor went out of business, the 2nd one is still very big.
Key Logic's KeyKOS (Score:2)
I've just spent the past few minutes trying to (re)find this story. Is it the KeyKOS recovery speed [eros-os.org] story from 1990?
Re: (Score:2)
Re: (Score:2)
That is often true.
x86 vs the 68k, MS-DOS vs Amiga, MS-DOS vs GEMTOS. and so on.
marketing often beats better tech.
Formal proofs of software are useless (Score:2)
Hi, MIT guys, formal proofs of filesystems are useless because you cannot incorporate physical systems into formal proofs. Real filesystems exist on real hardware.
I guarantee that your file system will fail if I start ripping cables out. A suitably strong EMP will take it out. In fact, I bet I could nuke your filesystem if I used my ham radio transceiver too close to the device. Other things that would destroy your filesystem include floods, earthquakes, and a lightning strike.
I began writing this by statin
Hardware Reliability (Score:2)
As others have pointed out, the formal verification does make the software provably reliable, but does nothing to protect against hardware issues. Just as a datapoint, the Stratus VOS operating system has been checksumming at the block driver level since the OS was written in 1980. It has detected failures on every generation of hardware it has been used with since. Some of the failures we have seen: Undetected transient media errors (the error correction/checking isn't perfect); Flaky I/O busses; bugs
Re: (Score:2)
I don't believe this one bit.
That's why we have checksums.
Re: (Score:1)
That's why we have checksums.
checksums will only detect a single bit error, you've got to do better than that
Re: (Score:2)
checksums will only detect a single bit error
Nope.
Re: Yeah rigth (Score:2)
Re: (Score:2)
That's why we have checksums.
There is no guarantee checksums will detect failure there is only a probability.
Re: (Score:2)
There is no guarantee that a Slashdot reader will detect a joke; there is only a probability.
Did anyone get it?
Re: (Score:2)
Re:Define "crash". (Score:4, Insightful)
Re: (Score:3)
As the Linux FS developers found some time ago, many modern disks also blatantly lie about having flushed data to disk. With software, you can then only do heuristic things to reduce the impact, not more. This "magic" MIT FS cannot do any better, and hence is entirely superfluous.
Re:Define "crash". (Score:4, Insightful)
Many consumer devices generally conform to an unwritten standard, not a written one. That unwritten standard is "do whatever is needed to make it work on Windows". This means that mandatory commands might not be fully tested, or sometimes not even implemented. And because these are consumer devices, the manufacturers generally aren't concerned about rare end-user problems, since whoever bought the flash thumb drive on sale isn't going to complain, and the margins are way too small to waste time on reliability. All that matters is getting it to work for most people most of the time.
Re: (Score:2)
I completely agree.
Re: (Score:2)
That's a snag I've found in the past. So much hardware is consumer grade so that the datasheets are rubbish. You think that your write has succeeded but it's still got data stuck in the cache, and the "flush, dammit" command is actually a no-op. So a never-fails file system I used in the past was getting corrupted, and the developers of it were baffled because they never saw a failure like that before.
So let's say your super reliable file system is mathematically proven, but the axioms are false, what the
Re: (Score:2)
Beware of bugs in the above code; I have only proved it correct, not tried it.
-- Donald Knuth.
This new filesystem sounds like another case of this...