パスワードを忘れた? アカウント作成
12487448 story
ソフトウェア

MITが「システムクラッシュしてもデータ損失が発生しないことを数学的に証明した」というファイルシステムを開発 30

ストーリー by hylom
証明がキモらしい 部門より
あるAnonymous Coward 曰く、

データの損失がほぼ起きないファイルシステムを開発したとMITが発表している(MITNewsSlashdot)。

一般的なファイルシステムではデータを書き込んでいる際にコンピュータがクラッシュした場合、そのデータは正常に書き込まれない。データ保護のためのジャーナリング機構を持つファイルシステムもあるが、これはあくまでファイルシステム全体の破損を防ぐことを目的としており、個々のファイルについては正常に書き込めない場合もある。

このファイルシステムについての詳細は明らかにされていないが、「クラッシュの際にデータを失わないことが数学的に保証された初のファイルシステム」だという。詳しくは10月のACM Symposiumでで公開される予定で、コードを含んだファイルシステムの立証環境を提供するとしている。

この議論は賞味期限が切れたので、アーカイブ化されています。 新たにコメントを付けることはできません。
  • 俺も開発した (スコア:4, おもしろおかしい)

    by Anonymous Coward on 2015年08月28日 16時27分 (#2872198)

    ただし書き込みはできない

  • OS/アプリがクラッシュするって事は、書き込み途中のデータも壊れてるor部分的にしか書けてない可能性が高い訳で、そんなデータを元にシステムとか修復すると、再起不要になる様な気がする。
    まずは、「OS/アプリが不完全な書き込みを信用しない」ってシステムが前提に無いと無用に思える。

    --
    -- Buy It When You Found It --
    • by Anonymous Coward

      それを活かすシステムがなければ、を前提にするなら何だって無用でしょうよ。
      それとも、実用実装を同時開発しない限り基礎技術の研究開発も無駄だと言う極論者なんだろうか。

      何なんだろね、この、まずは否定することから始める人って。

    • by Anonymous Coward

      今時のファイルシステムは、HDDへの転送が不完全だったりするデータは破棄する仕様ですよ。
      問題は、HDDの書き込み完了を確認するすべが必ずしもない事と、まさに物理的に書き込みしている最中での電源断などの時に完全か不完全かの判定が確実に可能なシステムなのかと。
      その辺は数学的な話ではないと思うので、今回は対象外でしょう。
      そんな感じで考えればジャーナリングとかsoftupdateのも該当しそうなんだけども。
      で、ちょっとリンク先覗いたところだとFFSとか書いてあって、softupdateに代わるなにかなのか、それともキャッシュとか遅延書き込みとかも含めて堅牢性を高める話なのか、って思ったけど時間ないので読んでない。

      • by Anonymous Coward

        ファイルに書き込む最後の1ビットが、ファイル無効から有効に切り替える1ビットで、これを書き換えるまでにストレージが止まったら、当然そんなファイルは存在しない事にされるし、ファイル無効から有効に切り替える1ビット書き換え中のクラッシュは、読み出した時のハードウェアの閾値で自動的にファイルの有効無効が決まるって話では?

        • by Anonymous Coward

          ブロックデバイスとは1ビット単位で書き込めないからそういう名前なんだよ。

          • by Anonymous Coward
            キャラクタデバイスも1ビット単位では書き込めないと思う…
  • by s-wakaba (47029) on 2015年08月28日 19時23分 (#2872282)

    ファイルシステムがクラッシュしてもデータ損失が発生しない証明を見つけたが、それを書くにはそのファイルシステムの空き容量が狭すぎる。

    • by Anonymous Coward

      『証明』って単語で誰もが思いつくけどイマイチ投稿ボタンまでは行かないネタの定番ですね!

  • by Anonymous Coward on 2015年08月28日 17時42分 (#2872234)

    これはファイルシステムみたいなlow levelのコード全体の形式的証明に成功したって
    話であって、現実的にデータ損失が発生しないって話じゃないでしょ。

    たとえば現実のハードディスク中のfirmwareは、今回の形式的証明で担保されてない
    わけで、この間のストーリー http://hardware.srad.jp/story/15/08/26/0642232/ [hardware.srad.jp] に
    あったような、firmware に原因がある silent data corruption には対処できない筈。

    • by Anonymous Coward

      「形式的」って数学用語なわけだが「実質的」の対義語みたいに見えてしまっていまいちな訳だと思う。

  • by Anonymous Coward on 2015年08月28日 20時35分 (#2872362)

    むかしむかしアカシックレコードに..

  • by Anonymous Coward on 2015年08月28日 20時41分 (#2872370)

    「データ損失が発生しないことを数学的に証明した」のに、
    データの損失がほぼ起きないファイルシステムを作っただと?

    • by nemui4 (20313) on 2015年08月28日 21時04分 (#2872385) 日記

      ホットスペアの玉数越えて壊れたら48hくらいでアウトになるのとかあるし、ハードも頑張らないとアカンねやろね。

      親コメント
    • by Anonymous Coward

      これ単に、OSクラッシュでデータ損失しないことを証明しただけじゃね?
      ハード故障でも損失しないことを証明することは、そりゃ無理でしょう。

      RAIDにしたところで、HDDが飛んだあとも交換せずに使い続ければいずれデータは飛ぶ。

      • by Anonymous Coward

        公理「決して故障しない理想的なハードが存在する」の下での証明?

        • by Anonymous Coward

          「存在する」では故障するハードにあたったときアウトだから、公理「ハードウェアは決して故障しない」では?

  • by Anonymous Coward on 2015年08月29日 0時29分 (#2872526)

    BSDがSoft updates実装したときに「そもそもハードウェアが命令どおりの手順を守らないことがあるから意味無くね」云々
    って話を聞いた気がするけどそういう場合でも大丈夫なのかね

  • by Anonymous Coward on 2015年08月29日 10時21分 (#2872664)

    書き込みはいつも新しいブロックに、古くなったブロックはトリムで後から回収。

  • by Anonymous Coward on 2015年08月29日 10時28分 (#2872669)

    ファイルシステムをCoqで書いたんだとさ

typodupeerror

ソースを見ろ -- ある4桁UID

読み込み中...