[HN Gopher] SquirrelFS: Using the Rust compiler to check file-sy...
       ___________________________________________________________________
        
       SquirrelFS: Using the Rust compiler to check file-system crash
       consistency
        
       Author : belter
       Score  : 55 points
       Date   : 2024-06-23 14:02 UTC (8 hours ago)
        
 (HTM) web link (arxiv.org)
 (TXT) w3m dump (arxiv.org)
        
       | metadat wrote:
       | Does this have a practical use? It's definitely a novel
       | application of a property of Rust. It's also been my impression
       | filesystem consistency is largely a solved problem thanks to
       | write-ahead logs (WAL) and the like.
       | 
       | It's nice the authors included a link to the underlying source
       | code in the last paragraph:
       | 
       | https://github.com/utsaslab/squirrelfs
        
         | vlovich123 wrote:
         | There's a pretty big difference between leveraging the compiler
         | to do a formal proof of the codebase on your behalf vs runtime
         | tests to make sure your WAL is maintaining the invariants you
         | expect it to have.
        
         | IshKebab wrote:
         | Does what have a practical use? The actual filesystem, or using
         | the typestate pattern to prove the absence of bugs?
         | 
         | The latter is clearly a practical use - no bugs (or at least
         | vastly less likely bugs).
         | 
         | The former is maybe a no since it seems like the authors
         | couldn't achieve their results for "normal" filesystems because
         | they are asynchronous - only for "persistent memory" which is
         | synchronous. I dunno exactly who has persistent memory though.
         | I guess it's stuff like Intel's Optane (which was
         | discontinued)?
        
       | klysm wrote:
       | This is definitely part of the future for better storage systems.
       | Too much responsibility is currently in the hands of programmers
       | (like me) to not make any mistakes. The storage layer can be a
       | high consequence place to make a mistake!
        
       ___________________________________________________________________
       (page generated 2024-06-23 23:00 UTC)