3 ms·
obviously computers are not totally infallible, solar rays can flip memory bits from 1 to 0 or vice versa -- but those failure modes are not expressed by the so
by preseinger 3y ago
obviously computers are not totally infallible, solar rays can flip memory bits from 1 to 0 or vice versa -- but those failure modes are not expressed by the source code of the running program, they're triggered at a layer of abstraction well below the compiled and running software
say the probability of a solar ray bit flip is (say) 0.01%, then consider the following function
fn x -> int {
if (randf32() < 0.0001) { panic("boom") }
return 123
}
x will panic with the same probability that a solar ray will flip a memory bit
is this acceptable? can i assume that calling x will never panic, in practice?
- xigoi 3y ago> can i assume that calling x will never panic, in practice? If you used the actual probability, which is several orders of magnitude lower, then yes.
- preseinger 3y agoi'm not sure what to say to this -- my question was rhetorical your position is incompatible with deterministic program execution -- it's unsound (shrug)
- Dylan16807 3y agoIt reads as rhetorical. But it was also a bit of a strawman. Sometimes dismantling a rhetorical question makes sense to do. The answer to your rhetorical question was an obvious no, but it also wasn't relevant to my argument because you used such a high probability. Deterministic program execution is an assumption we make even though it's not 100% true. Soundness, when it comes to computer programs, isn't real.
- preseinger 3y agothe specific probability was irrelevant
- xigoi 3y agoThe specific probability is relevant. 2^-256 is practically impossible, 10^-4 is not.
- preseinger 3y agogiven fn x -> int if (randf32() < P) { panic } return x x is buggy for all values of P except P=0 if you want to assume P=0 when P<n then OK but you have to prove that's safe in your use case, it's not something that can be assumed as true in general, no matter how small P gets
- Dylan16807 3y agoAll software is buggy on real hardware. You said in another comment "i can control what my application uses as IDs" but no not really. You can control what it does the vast vast majority of the time, but it will sometimes go wrong. The user doesn't care if it's a logic error that would also happen on impossibly perfect hardware or if it's a logic error caused by trusting your hardware. There's an implicit "hope not to hit the ultra rare bad luck" on each line of code. And when the probabilities are low enough it's hard to even say which version is safer sometimes.
- preseinger 3y ago> All software is buggy on real hardware. definitely not "buggy" is a logical property of the program as expressed, not a physical property of the program as executed a solar ray flipping a memory bit on the hardware executing an otherwise correct program does not make that program buggy > There's an implicit "hope not to hit the ultra rare bad luck" on each line of code. there definitely is not, at least in the context of the program as expressed such a case of "bad luck" would violate the assumptions of the language model, and/or execution model, and/or hardware model, and/or etc., of the running program, in a way that would be likely undetectable and definitely un-fixable it would be an invariant violation of the hardware/os/language model -- but a bug is a logic error it is so important that programmers understand this distinction fn f1(x int) -> int { return x } fn f2(x int) -> int { if x==2 { panic } else { return x } } fn f3(x int) -> int { if rand() < 1e-10 { panic } else { return x } } f1 is correct, f2 is buggy, and f3 is buggy -- no matter if 1e-10 is 1e-10 or 1e-20 or 1e-30
- Dylan16807 3y ago> but those failure modes are not expressed by the source code of the running program, they're triggered at a layer of abstraction well below the compiled and running software Does that make a difference? There's no way to use source code without applying the real world to it. > is this acceptable? can i assume that calling x will never panic, in practice? If the probability is that high, then even if x was just { return 123 } you shouldn't assume it will work. If you replace that code with if (secure_rand_u128() == 0) { panic("boom") }, then it would be safe to assume it won't panic.
- preseinger 3y ago> If the probability is that high, then even if x was just { return 123 } you shouldn't assume it will work. if x -> { return 123 } then callers can 100% assume it will work what is the alternative? how could callers de-risk the case when a solar ray flips a bit to make x not return 123? they can't, because they don't have access to an execution model outside of the semantics of the language, and those language semantics literally guarantee x will return 123 this is literally basic computer science material > if you replace that code with if (secure_rand_u128() == 0) { panic("boom") }, then it would be safe to assume it won't panic. secure_rand_u128 returns, presumably, a random unsigned 128 bit integer unsigned 128 bit integers can be any value between 0 and 340282366920938463463374607431768211455 -- and one of those possible return values is 0 if i call secure_rand_u128, then it absolutely can return 0, and code which assumes that it will never return 0 is, factually, buggy if you want to make the assumption that secure_rand_u128 will never return 0, then you have to justify that assumption in the context of your specific use case -- it absolutely cannot be assumed in the general case without qualifications -- P(x|x>0) != P(0)