Wetenschappers van MIT hebben een computersysteem gebouwd met de ‘wiskundige garantie’ geen data te verliezen.

Het zou geen overbodige luxe zijn: een computer waarbij je niet vanalles verliest als hij crast. De nieuwe computer van MIT is niet zozeer immuun voor bugs en crashes als wel zo ontworpen dat geen data verloren kan gaan in het geval van systeemfalen.

Ideeën voor een crashbestendig systeem bestonden al langer en zijn in sommige gevallen ook theoretisch bewezen. MIT is er nu voor het eerst in geslaagd dergelijke wiskundige modellen te vertalen in effectieve codetaal, ofwel, in een computersysteem dat geen bestanden kwijtraakt. Het systeem is nog traag, maar zou de basis kunnen worden voor toekomstige computers.

Grenzen

Aan de basis ligt het principe formal verification. Simpel gesteld, betekent dit dat men de grenzen van een computerprogramma wiskundig definieert en vervolgens test of het programma in praktijk daadwerkelijk nooit buiten deze limieten treedt.

Met behulp van een tool, Coq genaamd, bouwden de onderzoekers een nieuw systeem van onderop. Letterlijk elk onderdeel moesten ze eigenhandig definiëren: wat is een schijf? Wat is een bit? Vervolgens werden de onderlinge relaties tussen alle elementen van het systeem bepaald. Pas toen deze theoretische structuur min of meer klaar was, kon de bouw van het systeem beginnen.

Sleutel

Met hun bestandssyteem waarbij limieten en relaties zo zijn gedefinieerd dat het in theorie onmogelijk moet zijn data ooit te verliezen, hopen de wetenschappers van MIT de sleutel in handen te hebben voor het computersysteem van de toekomst. In oktober zal MIT de details van het systeem verder bekendmaken.

Bronnen: MIT, Wired, Computerworld

Beeld: Christine Daniloff / MIT