Selv om datamaskiner kanskje ikke krasjer så ofte som tidligere, er det likevel fortsatt mange som opplever dette og de følgene det kan få for filsystemet. For dersom krasjen skjer samtidig som at det skrives data til lagringsenheten, kan filsystemets opptegnelser og data bli korrumpert.
Har man ingen fersk sikkerhetskopi, kan viktige data gå tapt. I tillegg kan systemet i verste fall slutte å fungere skikkelig.
Bruker mobilkameraet: Microsoft med 3D-skanning for alle
Journal
Det finnes en mange filsystemer med funksjonalitet og egenskaper som skal kunne redusere problemene med systemkrasj eller strømavbrudd. En av de vanligste teknikkene er å logge alle endringer i en journal i en separat del av filsystemet, før endringene skrives til det hovedfilsystemet.
Vanlige filsystemer som NTFS, ext3 og HFS+ støtter alle en slik tilnærming. Men de kan ikke garantere at feil ikke oppstår ved en krasj.
I går ble det kjent at en gruppe elektronikk- og informatikkforskere ved MIT skal ha utviklet et filsystem som er matematisk garantert til ikke tape data under en krasj. Dette skal aldri ha blitt gjort tidligere.
Norskledet prosjekt: Skal gjøre nettverksstøtte enklere for applikasjonsutviklere
Enhver situasjon
– Å sikre at filsystemet til enhver tid kan gjenopprettes etter en krasj, er vanskelig fordi det er så mange ulike steder hvor du kan krasje. Du må bokstavelig talt vurdere enhver instruksjon eller enhver diskoperasjon og tenke, «Hva om jeg krasjer nå? Eller nå? Eller nå?», sier en av forskerne, Nickolai Zeldovich, førsteamanuensis i informatikk ved MIT, i en pressemelding.
– Empirisk har folk funnet mange feil i filsystemer som har å gjøre med krasjgjenoppretting. Og de fortsetter å finne dem, selv i svært godt testede filsystemer, fordi dette er så vanskelig å få til.
Leste du denne? Slik blir Microsofts nye filsystem
FSCQ
Filsystemet som forskerne har utviklet, kalles for FSCQ. Det har en design hentet fra filsystemet til Unix-implementeringen xv6, et operativsystem skapt ved MIT for undervisningsformål.
Gjenopprettingsfunksjonen i FSCQ er basert på en komponent som kalles for FscqLog. All oppdatering av disken gjøres gjennom denne, som setter sammen alle skrivekommandoer til atomiske transaksjoner.
Dette gjør det mulig å bevise at alle endringene som et systemkall gjør med disken, har enten alle skjedd eller ingen skjedd, selv om systemkallet feiler på grunn av en krasj etter å ha gitt noen skrivekommandoer (log_write).
Medisisk bildeanalyse: Nå skal IBMs Watson få «syn»
Formell verifikasjon
Detaljer om FSCQ har for lengst blitt offentliggjort, blant annet i denne artikkelen. Det nye nå er altså at forskerne har kunnet bevise påliteligheten til filsystemet gjennom en metode som kalles for formell verifikasjon.
Dette innebærer at man matematisk beskriver de akseptable grensene for kjøringen av et dataprogram og deretter beviser at programmet aldri vil krysse disse grensene.
Ifølge MIT er dette en komplisert prosess, noe som gjør at den vanligvis bare brukes på en skjematisk høynivå-representasjon av programvarens funksjonalitet. Dette har blitt gjort med andre filsystemer. MIT-forskerne har derimot testet egenskapene til selve kildekoden til FSCQ.
Ny arkitektur: Genierklært unggutt utvikler superbrikke
Verktøy
For å gjøre dette, har forskerne tatt i bruk et verktøy som heter Coq Proof Assistant. Forskerne måtte selv beskrive de ulike komponentene i Coqs formelle språk, inkludert å definere hva en disk er og hva en bit er. Deretter har de formelt måttet beskrive forholdene mellom atferden til disse ulike komponentene under krasjforhold.
– Vi implementerte derfor filsystemet i det samme språket som vi skrev testene. Og testene sjekkes mot det faktiske filsystemet, ikke en eller annet skjønnmaleri på en tavle som ikke har noen formell tilknytning til koden, sier Adam Chlipala, en annen førsteamanuensis i informatikk som har deltatt i prosjektet.
En forskningsartikkel om denne nyeste milepælen vil bli presentert under konferansen The ACM Symposium on Operating Systems Principle som arrangeres i Monterey, California, i begynnelsen av oktober. Da vil artikkelen trolig bli gjort tilgjengelig på denne siden.
Mer fart og rekkevidde: Knuste effektgrensen for optisk fiber
Eksperimentelt
Trolig er det ingen som kommer til å ta i bruk FSCQ slik filsystemet funger i dag. Forskerne innrømmer at det er tregt etter dagens standarder. Men de mener at teknikkene som har blitt brukt i forbindelse med utprøvingen, også kan tas i bruk i forbindelse med mer sofistikerte løsninger i framtiden.
Samtidig er det ikke alle tilfeller av datatap som skyldes krasj eller avbrudd. For eksempel må tap av data som skyldes plutselige, fysiske feil ved selve lagringsenheten forhindres ved hjelp av andre metoder.
