MITが「システムクラッシュしてもデータ損失が発生しないことを数学的に証明した」というファイルシステムを開発 30
ストーリー by hylom
証明がキモらしい 部門より
証明がキモらしい 部門より
あるAnonymous Coward 曰く、
データの損失がほぼ起きないファイルシステムを開発したとMITが発表している（MITNews、Slashdot）。
一般的なファイルシステムではデータを書き込んでいる際にコンピュータがクラッシュした場合、そのデータは正常に書き込まれない。データ保護のためのジャーナリング機構を持つファイルシステムもあるが、これはあくまでファイルシステム全体の破損を防ぐことを目的としており、個々のファイルについては正常に書き込めない場合もある。
このファイルシステムについての詳細は明らかにされていないが、「クラッシュの際にデータを失わないことが数学的に保証された初のファイルシステム」だという。詳しくは10月のACM Symposiumでで公開される予定で、コードを含んだファイルシステムの立証環境を提供するとしている。
俺も開発した (スコア:4, おもしろおかしい)
ただし書き込みはできない
Re:俺も開発した (スコア:4, 興味深い)
ただし書き込みは出来るが読み出しはできない。
# 40年以上前のネタではある [wikipedia.org]
Re:俺も開発した (スコア:2)
つ /dev/null
Re:俺も開発した (スコア:1)
ロムならぬウォムか。
Re: (スコア:0)
わいも。
読み書きともに可能。ただし、容量1bit。
Re: (スコア:0)
ソフトウェア的にはそうかもしれないが、ハードウェア的に負荷がかかってブロックが読めなくなったり、なんてことにはならないのかな。
幾らデータが読めた所で (スコア:2)
OS/アプリがクラッシュするって事は、書き込み途中のデータも壊れてるor部分的にしか書けてない可能性が高い訳で、そんなデータを元にシステムとか修復すると、再起不要になる様な気がする。
まずは、「OS/アプリが不完全な書き込みを信用しない」ってシステムが前提に無いと無用に思える。
-- Buy It When You Found It --
Re: (スコア:0)
それを活かすシステムがなければ、を前提にするなら何だって無用でしょうよ。
それとも、実用実装を同時開発しない限り基礎技術の研究開発も無駄だと言う極論者なんだろうか。
何なんだろね、この、まずは否定することから始める人って。
Re: (スコア:0)
今時のファイルシステムは、HDDへの転送が不完全だったりするデータは破棄する仕様ですよ。
問題は、HDDの書き込み完了を確認するすべが必ずしもない事と、まさに物理的に書き込みしている最中での電源断などの時に完全か不完全かの判定が確実に可能なシステムなのかと。
その辺は数学的な話ではないと思うので、今回は対象外でしょう。
そんな感じで考えればジャーナリングとかsoftupdateのも該当しそうなんだけども。
で、ちょっとリンク先覗いたところだとFFSとか書いてあって、softupdateに代わるなにかなのか、それともキャッシュとか遅延書き込みとかも含めて堅牢性を高める話なのか、って思ったけど時間ないので読んでない。
Re: (スコア:0)
ファイルに書き込む最後の1ビットが、ファイル無効から有効に切り替える1ビットで、これを書き換えるまでにストレージが止まったら、当然そんなファイルは存在しない事にされるし、ファイル無効から有効に切り替える1ビット書き換え中のクラッシュは、読み出した時のハードウェアの閾値で自動的にファイルの有効無効が決まるって話では？
Re: (スコア:0)
ブロックデバイスとは1ビット単位で書き込めないからそういう名前なんだよ。
Re: (スコア:0)
証明はできたんだけど (スコア:2)
ファイルシステムがクラッシュしてもデータ損失が発生しない証明を見つけたが、それを書くにはそのファイルシステムの空き容量が狭すぎる。
Re: (スコア:0)
『証明』って単語で誰もが思いつくけどイマイチ投稿ボタンまでは行かないネタの定番ですね！
形式的証明の話でしょ (スコア:0)
これはファイルシステムみたいなlow levelのコード全体の形式的証明に成功したって
話であって、現実的にデータ損失が発生しないって話じゃないでしょ。
たとえば現実のハードディスク中のfirmwareは、今回の形式的証明で担保されてない
わけで、この間のストーリー http://hardware.srad.jp/story/15/08/26/0642232/ [hardware.srad.jp] に
あったような、firmware に原因がある silent data corruption には対処できない筈。
Re: (スコア:0)
「形式的」って数学用語なわけだが「実質的」の対義語みたいに見えてしまっていまいちな訳だと思う。
Re:形式的証明の話でしょ (スコア:1)
適当な用語が望まれますね!
Re: (スコア:0)
「適当な」とか「勝手な」とか「任意の」と訳されるアレも何とかしてほしい。
失われた圧縮技術 (スコア:0)
むかしむかしアカシックレコードに..
何その嫌がらせ (スコア:0)
「データ損失が発生しないことを数学的に証明した」のに、
データの損失がほぼ起きないファイルシステムを作っただと？
Re:何その嫌がらせ (スコア:1)
ホットスペアの玉数越えて壊れたら48hくらいでアウトになるのとかあるし、ハードも頑張らないとアカンねやろね。
Re: (スコア:0)
これ単に、OSクラッシュでデータ損失しないことを証明しただけじゃね？
ハード故障でも損失しないことを証明することは、そりゃ無理でしょう。
RAIDにしたところで、HDDが飛んだあとも交換せずに使い続ければいずれデータは飛ぶ。
Re: (スコア:0)
公理「決して故障しない理想的なハードが存在する」の下での証明？
Re: (スコア:0)
「存在する」では故障するハードにあたったときアウトだから、公理「ハードウェアは決して故障しない」では?
以前 (スコア:0)
BSDがSoft updates実装したときに「そもそもハードウェアが命令どおりの手順を守らないことがあるから意味無くね」云々
って話を聞いた気がするけどそういう場合でも大丈夫なのかね
Re: (スコア:0)
okky先生?
Re: (スコア:0)
これ? [srad.jp]
FLASHと同じように使えばええんじゃね (スコア:0)
書き込みはいつも新しいブロックに、古くなったブロックはトリムで後から回収。
Re: (スコア:0)
こういうやつね「Linux用ログ構造化ファイルシステム」
http://lc.linux.or.jp/paper/lc2005/CP-04.pdf [linux.or.jp]
データベースなんかでも似たことをするれども[1]、数学的証明というのが萌えポイントなのでは?
[1] ログ先行書き込み (WAL)
https://www.postgresql.jp/document/8.0/html/wal.html [postgresql.jp]
証明 (スコア:0)
ファイルシステムをCoqで書いたんだとさ