the_oz has quit [Remote host closed the connection]
the_oz has joined #osdev
bauen1 has quit [Ping timeout: 260 seconds]
craigo has quit [Quit: Leaving]
xenos1984 has quit [Ping timeout: 272 seconds]
sidcha has joined #osdev
obrien has quit [Remote host closed the connection]
cloudowind has quit [Ping timeout: 252 seconds]
xenos1984 has joined #osdev
cloudowind has joined #osdev
zenmov has quit [Ping timeout: 260 seconds]
zenmov has joined #osdev
<SystemPrompt>
the future of safety will be formal verification,in 2200 when someone figures out how to make it work well and when computers are obsolete anyway. Rust will just be a special case of using only operations that can be automatically verified.
<heat>
haha i fixed the problem
<heat>
this was awful
<heat>
basically what seemed to be happening was: 1) someone grabs a filesystem block for metadata, marks it dirty 2) eventually frees it 3) block gets reused for the DB 4) the disk cache has its own copy of the block, the page cache for rpmdb.sqlite also does 5) these writes compete
<heat>
someone = the filesystem implementation, of course
<SystemPrompt>
that's what rust is - they just try to pre-declare a set of operations that are easy to verify
<heat>
yeah it's probably intensely hard to prove that something like grabbing refs to two or more indices is correct
<SystemPrompt>
as usual, a more restricted language increases what you can do WITH the language while reducing what you can do IN the language
<heat>
like, the given example is trivial, but for instance if you have two variables serving as indices, it gets mega hard to prove correctness there
<SystemPrompt>
if you had an extension of rust with full verifiability, you could give the compiler a proof that x!=y and then have refs to a[x] and a[y] at the same time
<SystemPrompt>
how hard is that proof? depends on your program design - don't make one where you're unable to prove it
<nortti>
isn't this what stuff with dependant types, like idris or so, have?
npc has joined #osdev
<zid>
add some barriers, huehuehue
<zid>
aka locks
<SystemPrompt>
if you can't prove it but you're pretty sure it's true, you could always write if(x==y) abort();
Matt|home has joined #osdev
<SystemPrompt>
this proves that on the next line, x!=y
<SystemPrompt>
it doesn't have to be high overhead. Some Java extensions have a feature like this for instanceof. Inside a block where if(x instanceof Y) you can call methods from Y.
<SystemPrompt>
it's a feature specific to if(x instanceof Y) and doesn't generalize to any other expression though
Celelibi has quit [Ping timeout: 264 seconds]
Celelibi has joined #osdev
foudfou has quit [Quit: Bye]
foudfou has joined #osdev
Gooberpatrol66 has quit [Ping timeout: 276 seconds]