MIT: Neues Dateisystem mathematisch beweisbar ohne Datenverluste

Ein neues Dateisystem soll zukünftig dafür sorgen, dass Abstürze nicht mehr mit Datenverlusten verbunden sind. Die Entwickler setzen dafür allerdings nicht darauf, alle denkbaren Fehlerquellen zu bedenken und entsprechende Notfall-Maßnahmen ... mehr... Quellcode, Code, Programmierung, Programmiersprache Quellcode, Code, Programmiersprache, Php, Source Code Quellcode, Code, Programmiersprache, Php, Source Code Free for Commercial Use / Flickr

Diese Nachricht vollständig anzeigen.

Jetzt einen Kommentar schreiben
 
Sorry, aber das ergibt keinen Sinn. Ein Dateisystem hat nichts mit Datenverlust bei einem Absturz zu tun. Solange die Daten im Arbeitsspeicher sind, weil man gerade in einer Anwendung einen Text schreibt oder ein Bild bearbeitet und es noch nicht abgespeichert hat, und es zu einem Absturz kommt, sind die Daten weg. Egal was für ein Dateisystem auf der Festplatte ist. Kommt es während des Schreibens auf der Festplatte zum Absturz, sind die Daten auch so lange nicht vorhanden, bis sie vollständig geschrieben wurden. Was nicht da ist, ist nicht da. Ganz einfach. Das Dateisystem kann lediglich gegen Datenverlust durch Beschädigung abgesichert werden. Aber das genannte Szenario im Artikel hat keinen Zusammenhang mit dem Dateisystem.
 
@DerKritiker: Das sagt mir meine Logik auch, allerdings befürchte ich, mich mit so was auch bei Weitem nicht ansatzweise so gut auszukennen wie diese MIT-Jungs. Von daher gehe ich mal davon aus, dass die schon wissen, was sie tun. Der Knackpunkt an der Sache könnte eventuell sein, dass der Text, den wir hier zu lesen bekommen, den eigentlichen Kern der Sache nicht laienverständlich rüberbringt.
 
@DerKritiker: Doch es ergibt Sinn. Die aktuellen Lösungen gegen Datenverlust sind eher als "Kleckern" zu bezeichnen.

https://en.wikipedia.org/wiki/Journaling_file_system
 
@DerKritiker: Deswegen ist es wahrscheinlich auch etwas schwammig ausgedrückt. In meinen Augen kann es auch keinen Schutz gegen ein "halbes" Schreiben geben, außer dass man transaktionale Konzepte nutzt, bei denen eben beim Überschreiben der alte Zustand bei einem Absturz erhalten bleibt. Damit käme es de-facto aber trotzdem zu einem "Verlust" der Daten, die gerade geschrieben wurden. Es kommt nicht zur Korruption des Dateisystems (zumindest bezogen auf eine Datei), aber Daten, die im Moment des Absturzes geschrieben werden, sind weg und dagegen lässt sich auch nichts unternehmen. Zumindest nicht, wenn man RAM nicht gegen persistenten Speicher austauscht.
 
@DerKritiker: Es geht nicht um den Verlust der Daten im Arbeitsspeicher, sondern darum, dass keine unauflösbaren Inkonsistenzen auftreten, z.B. wenn während des Schreibens auf den Datenträger der Strom ausfällt oder gerade eine Datei verschoben wird, so darf nie ein Zwischenzustand entstehen bei dem nicht mehr entschieden werden kann ob es 2 Dateien sind oder die Datei auf Platz A oder B ist (oder gar nur teilweise an bestimmten Positionen).
 
@wischi: Jain: "Formally verified working file system could lead to computers guaranteed never to lose your data." und "At the ACM Symposium on Operating Systems Principles in October, MIT researchers will present the first file system that is mathematically guaranteed not to lose track of data during crashes." weckt zumindest bei mir die Erwartungshaltung, dass keinerlei Daten, also auch die nicht, die gerade geschrieben werden sollen, jemals durch einen Crash verloren gehen können.

Alles andere, was du schreibst, gibt es schon.
 
@Mitsch79: Es gibt schon mathematisch Bewiesene Journal-Dateisysteme? Schick mal einen Link.
 
@wischi: "Es geht [...] darum, dass keine unauflösbaren Inkonsistenzen auftreten, z.B. wenn während des Schreibens auf den Datenträger der Strom ausfällt oder gerade eine Datei verschoben wird, so darf nie ein Zwischenzustand entstehen bei dem nicht mehr entschieden werden kann ob es 2 Dateien sind oder die Datei auf Platz A oder B ist (oder gar nur teilweise an bestimmten Positionen)."

Genau das stellen NTFS, ReiserFS, Ext4 und Co. sicher.
Von mathematischer Beweisbarkeit hat niemand was gesagt. Auch du nicht. Allerdings ist die Stabilität von NTFS in einem produktiven, also realen Einsatzszenario zumindest empirisch bewiesen, was dem mathematischen Beweis überlegen ist. Ich setze NTFS seit ca. 1999 ein (NT4.0 SP4 bzw. Win2k und dann fortlaufend), was sicherlich mehrere Billionen erfolgreiche Transaktionen bedeutet. Und ich habe es noch _nie_ erlebt, dass irgendein Datenverlust oder Inkonsistenzen aufgetreten wären. Multipliziere das mit der Anzahl aller Personen die NTFS nutzten oder nutzen und denen es ähnlich geht und der E(Datenverlust oder Inkonsistenzen treten auf) = 0
 
@DerKritiker: Es hängt davon ab, was die Kollegen alles zu ihrem Modell des Dateisystems dazu zählen. Punkt eins wurde schon genannt, dass man Dateisystemoperationen als Transaktionen betrachtet und dementsprechend erst nach einem commit die neuen Daten aktuell werden.

Sollten die MITler auch davon ausgehen, dass Hardware ein Teil des Dateisystems sein kann, dann reicht eigentlich ein unabhängiger Transaktionspuffer/-controller aus. Das Betriebssystem gibt die Daten die geschrieben werden sollen in den Puffer, sobald es fertig ist, gibt es ein commit und die Daten werden persistiert. Dabei ist es mathematisch durchaus möglich, eventuell fehlerhafte Daten über entsprechende Paritätsinformationen zu korrigieren und dann zu schreiben. Bspw, wenn beim Schreiben in den Puffer ein Crash passiert ist. Genaugenommen könnte man den Puffer auch weglassen, wenn man die Daten so verteilt schreibt, dass die Informationen für das Berechnen immer so vorhanden sind, dass der Crashzeitpunkt egal ist. Wichtig dürfte hauptsächlich sein, dass die Schreibvorgänge autonom ablaufen können, also nicht auf die Steuerung durch das OS angewiesen sind.

Spannend bleibt, wie sie die Schreibvorgänge letztlich organisieren, damit bei einem Crash alles wiederhergestellt werden kann... Denn wenn ich 1Gbyte an Daten schreiben muss und das System crasht nach 100Kbyte, dann ist es schwer vorstellbar, dass das MIT-FS da etwas reißen kann. Und transaktionsbasierte FS gibt es ja schon... NTFS wäre eines, falls das jemand kennt ;)
 
@Mitsch79: Kann mir das auch nicht so recht vorstellen.

Dass eine Datei (Transaktion) nicht komplett geschrieben wurde, und damit im Bereich XY Datenmüll liegt kann ja NTFS bereits durch das Journal erkennen.

Um bei deinem Beispiel zu bleiben: Wenn ich 1 Gbyte Daten speichern will, MUSS ich 1 Gbyte Daten unterbrechungslos auf die Platte bringen - sonst sind die Daten "futsch".

Wo da nun genau der Unterschied zu aktueller Technologie liegen soll erschließt sich mir nicht.
 
@dognose: Mir eben auch nicht so recht, weshalb ich sehr gespannt bin wie das nun umgesetzt wurde.

Denn sollten die MIT-ler einen quasi genialen Weg gefunden haben, unabhängig von der Datenmenge irgendwie die "Wiederherstellungsinformationen" und die Daten so auf den Datenträger zu schreiben, dass egal wann, ein Absturz keinen Effekt hat, dann stellt sich die Frage, warum man nicht überhaupt nur die "Wiederherstellungsinformationen" schreibt und einfach die Daten errechnet ^^

Je mehr ich darüber nachdenke komme ich zu der Feststellung, dass sie eigentlich nichts neues per se entwickelt haben, sondern nur einen Weg, ein Dateisystem formell so zu beschreiben, dass sie theoretisch beweisen können, dass es niemals zu Dateninkonsistenzen kommen kann. Aber Datenverluste sind bei einem Crash während des Schreibvorganges nach wie vor der Fall, genauso wie Daten durch das Altern oder den Ausfall eines Datenträgers verloren gehen können.

Sprich, sie können innerhalb ihres Modells nun lediglich das beweisen, was andere von ihren Dateisystemen mehr oder weniger behaupten.

Da sie aber die Hardware und deren Beziehung ebenfalls formell beschreiben, ist hier zwangsläufig eine Abstraktion in dem Modell erreicht, die reale Hardware auch nur idealisiert abbilden kann. Jedes Modell idealisiert die Wirklichkeit nur, egal wie detailliert es ist.
 
@Mitsch79: "Schreibe nur die Wiederherstellungsinformation": Dann hätten Sie die Ultimative Kompressionslösung entwickelt :-)

Ich denke auch, dass es hierbei nur um die "Beweisbarkeit" geht. Und ob meine Festplatte nun praktisch keine Daten verliert - oder sowohl praktisch als auch theoretisch beweisbar ist mir eigentlich Egal.

Also Gelinde gesagt das pendantische Bedürfnis einiger Mathematiker etwas funktionierendes auch mathematisch Beweisen zu wollen.
 
@DerKritiker: Solang mir keiner Geld auf mein Konto überwiesen hat, is auch keins drauf. Egal welche Bank ich dafür nutze.
 
Es ist (vergleichsweise) einfach Software zu schreiben dessen Funktionalität Mathematisch bewiesen ist jedoch werden verwendete Axiome (wie z.B. die Hardware) für den Beweis nicht näher betrachtet, doch genau diese Annahmen müssten auch in den Beweis eingebaut werden, was in der Praxis nicht möglich ist. Es ist also wieder eine Meldung von der wir ab heute nicht mehr viel hören werden.
 
@wischi: Es ist einfach? Also wenn ich nun mathematisch beweisen müsste, dass ein ein einfaches Programm, in jedem Detail korrekt arbeitet, dann bin ich schon etwas beschäftigt. Möglich ja, aber in meinen Augen, definitiv nicht einfach. Und wenn ich dann komplexe Programme, dann will ich gar nicht dran denken
 
@Fallen][Angel: Es ist relativ einfach, du musst nur geeignete Programmiersprachen nutzen. Programme geschrieben mit funktionalen Programmiersprachen wie Haskell lassen sich gut formal beweisen.
 
@Fallen][Angel: Das vergleichsweise steht im Kommentar nicht zum Spaß. Und ja im Vergleich zum mathematischen Beweisen von Hardware (was notwendig wäre, weil ja alles andere darauf aufbaut) ist nicht möglich ohne einen Laplaceschen Dämon. Die Beweisen nur die Software mathematisch was in der Realität nichts bringt wenn die Axiome auf denen die Beweise aufbauen in der Realität keine Fakten sind!
 
@wischi: Das wir davon nichts mehr hören, sehe ich anders. Was sicherere, abstraktere und konsequentere Programmiersprachen und die Abkapselung von Software angeht, geht es ja schon seit Jahren voran (dankenswerterweise). Das wird das Thema beweisbarer Korrektheit langfristig immer interessanter machen, selbst wenn es vorerst unter dem Vorbehalt von Chipfehlern steht.

Aber auch auf dem Bereich der Validierung von Chipdesigns wird es vorangehen, ist ja auch ein mathematisches Forschungsthema. Zum Umgang mit den Gefahren von physikalischen Fehlerquellen in ursprünglich korrekten Chips, hätte ich jetzt zwar noch keine konkrete Idee, da finden sich vielleicht prohabilistische Ansätze zur Früherkennung von Fehlern oder zur Robustheit gegenüber Fehlern.

Uns bleibt auch schlicht nichts anderes übrig. Je mehr Bereiche komplexe automatische Entscheidung benötigen (Smartgrids für dezentrale Energieversorgung, die Versorgung entstehender Megacitys, immer weiter automatisierte Massenfertigung, automatisierter Verkehr, womöglich medizinische Anwendungen auf mikroskopischem Level, etc., womöglich nachlassende Möglichkeiten für Redundanz in bestimmten Bereichen aufgrund knapper werdender Ressourcen) und je komplexer die Programme werden (z.B. auch durch Notwendigkeit von Parallelisierung, die ihren eigenen Haufen an Problemen mitbringt), welche diese Funktion ermöglichen, desto stärker wird der Bedarf werden die Fehleranfälligkeit zu senken, sonst werden bestimmte Anwendungen gar nicht machbar sein.
 
Ohne die angedeuteten Konzepte verstanden zu haben:

Klassischer Konflikt Mathematik vs Real Life.

Ich bezweifle, dass sich in komplexen Systemen alle Komponenten reproduzierbar um die mathematischen Algorithmen scheren werden.
 
Was der Artikel angibt ist unmöglich. Wenn ich im Datentransit die Energiezufuhr kappe wird alles was bis dahin nicht auf nichtflüchtigen Speichern liegt im Nether verschwinden.

Das Einzige was ich mir vorstellen kann was dieses Dateisystem tut: das entsprechende Fragment welches auf der Platte ankam, ist nach dem nächsten hochfahren nicht "korrupt" sondern noch lesbar.
 
Da bin ich mal gespannt! Das klingt spannend, vielleicht werden solche Dateisysteme den Datendurchsatz erhöhen können. Durch Mathematik lassen sich einige Operationen bestimmt sparen, wobei dann Smartphones weniger Strom verbrauchen.

Warten wir es ab ;-)
Kommentar abgeben Netiquette beachten!

Video-Empfehlungen