On Tue, Dec 9, 2008 at 1:49 AM, Eric Rannaud <span dir="ltr"><<a href="mailto:eric.rannaud@gmail.com">eric.rannaud@gmail.com</a>></span> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Isn't BitC going to allow unsafe array accesses for performance critical<br>
code? </blockquote><div><br>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.<br>
<br>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.<br> <br></div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Is it really realistic, performance-wise, to only support array<br>
accesses with bound checking?</blockquote><div><br>There is no quantitative evidence that the overhead of such checks matters in real programs.<br><br></div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
Obviously, there are various situations where an out-of-bound cannot<br>
happen (one may even have written a proof for it); also, there are many<br>
situations where a runtime exception is no more useful than a<br>
segmentation fault. So if I cannot do anything useful with the<br>
exception, there is little point in performing the corresponding runtime<br>
checks (division-by-zero and null-dereferencing are always caught,<br>
out-of-bounds may not).</blockquote><div><br>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.<br>
<br></div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">For example, in a kernel, what are you going to do with a<br>
division-by-zero exception? Modern processors will generate a fault for<br>
you anyway, and you can catch it and print a call trace to a console.</blockquote><div><br>In a kernel, it is appropriate to do whole-program verification to ensure that this cannot happen.<br><br></div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
As BitC aims to have similar performance to C, I was thinking so-called<br>
"unsafe" operations would be supported (I actually assumed it would be<br>
the default, instead aiming at static correctness). Will it be the case?</blockquote><div><br>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.<br>
<br>shap<br></div></div>