On Tue, Dec 9, 2008 at 1:49 AM, Eric Rannaud <[EMAIL PROTECTED]> wrote:
> Isn't BitC going to allow unsafe array accesses for performance critical > code? Array accesses do not require bounds checks. Vector accesses do. Optimizers can generally remove the vector bound checks in inner loops in any case, so no, we will not allow unsafe accesses to vectors. In loops, the bounds check can generally be hoisted out of the loop. It will eventually be possible to state and discharge properties that ensure that the bounds are honored. The compiler will be free to exploit such knowledge. > Is it really realistic, performance-wise, to only support array > accesses with bound checking? There is no quantitative evidence that the overhead of such checks matters in real programs. Obviously, there are various situations where an out-of-bound cannot > happen (one may even have written a proof for it); also, there are many > situations where a runtime exception is no more useful than a > segmentation fault. So if I cannot do anything useful with the > exception, there is little point in performing the corresponding runtime > checks (division-by-zero and null-dereferencing are always caught, > out-of-bounds may not). If one has written a proof for it, one should be able to state and discharge the property using the (eventual) BitC property language. The optimizer is then free to rely on that information. For example, in a kernel, what are you going to do with a > division-by-zero exception? Modern processors will generate a fault for > you anyway, and you can catch it and print a call trace to a console. In a kernel, it is appropriate to do whole-program verification to ensure that this cannot happen. As BitC aims to have similar performance to C, I was thinking so-called > "unsafe" operations would be supported (I actually assumed it would be > the default, instead aiming at static correctness). Will it be the case? Quite the reverse. The whole point of BitC is to have a *safe* systems language. If we didn't care about the programs being correct, we would be using C. shap
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
