On Thu, Feb 26, 2009 at 7:10 PM, <[email protected]> wrote: >>Because BitC is focused on systems programming, and we therefore need >>to deal concretely with things like hardware registers, cache line >>sizes, and things of that sort. Matters of data layout in systems >>programs are prescriptive. The formal inconveniences that you identify >>are real, but they cannot be solved at the cost of failing to satisfy >>pragmatics requirements. > > certainly. The question is where these pragmatic requirements are to be > satisfied - I'm wondering if the language is the right place. I'm > wondering if the output phase is more appropriate.
The answer is that this is a language matter. The reason is that arithmetic over unbounded precision is natural number arithmetic, where arithmetic over bounded precision types is arithmetic over a ring algebra. The two really are different types because of their different semantics. Even for the restricted usages of operating systems, there is no known verifier today that can discharge bounds obligations with sufficient automation, and even if there were we have no means to specify the requirements on such a verifier. This ruled the approach out. This decision was frozen in early 2006, and it is not up for discussion in BitC at this point. We can discuss it for purposes of understanding and documentation, or for purposes of thinking about a hypothetical future language, but at the moment my attention needs to be on getting a BitC release out. BitC doesn't need to be perfect. It needs to be useful. >>We also want to be within 1% to 1.5% of the performance of >>aggressively hand-optimized C (and privately I'ld like to *beat* that >>performance). That definitely cannot be done if we build any >>significant overhead in at the level of integer arithmetic. > > surely Since the bounds checks cannot be automatically discharged even in the restricted case, you can see the specifying range-bounded arithmetic in terms of natural number semantics would require runtime checks. These would carry significant overhead -- well outside our acceptable limits. >>BitC does provide an unbounded integer arithmetic capability, and for >>many applications that is the right thing to use. It isn't good enough >>to write operating systems. > > didn't know unbounded int was provided, but for you 2nd point, agreed At the moment it's in a library that is only halfway implemented. We probably need to bless this one into the language so that we can do literals for it. >>Range constraints incur a discharge obligation. > > I presume that 'discharge obligation' mathspeak for 'you gotta prove it > stays fenced in' Yes,. >>In the general case, >>this is an unsolved problem in the literature. > > In general I'm sure it is. But we're not facing generalities but trying > to prove restricted things. Kernel stuff is going to be restricted. It > has to be to be provable. Experience shows that this proof cannot be automatically discharged even within a kernel. If not, then it's an insufficient basis for making representation decisions. The language specification is not in a position to dictate what properties *must* be discharged; the state of the art for provers isn't far enough along, and on this issue it's unlikely that it ever will be. > (I saw something about dependent types which relate to this; read the > wiki pages but not much more. Whatever these exactly are, will they > cover all possibilites needed? I'll have to read more) BitC isn't doing dependent types and will not do so in this round. Dependent types is a discussion for future extensions/enhancements. > So, it seems to me to make sense that the language deals with integers > generally (it's got to be easier on the specification & prover!) but > if it can determine, or can be fed, proof that a range will not be > exceeded then it makes sense the back end spits out the int16 - or > whatever the smallest/fastest sized word fits - instead of code to > manage an unbounded integer. But that choice is an optimisation. It's > an optimisation that has to be made for acceptable performance, but it > seems that optimisation hints about machine words should not be > specifiable in the language. No, dammit. I apologize. You aren't the problem here, but the level at which many PL people and formal methodists seem constitutionally incapable of grokking this issue has been very frustrating. For systems code, representation is bloody well NOT just an optimization. It is a prescriptive requirement. > To put it another way, machine word size specifications should come out > of the back, not be fed in at the front. I understand your view. Since your view is not achievable in practical terms, and since it is not likely to be within our lifetimes, this is not a viable design point for a practically useful language today. Jan: you're asking good questions, and my frustrations on this point are in no way due to you. You've merely had the misfortune to step on a sore point. One point to consider: the general view of what is "semantic" in the PL world usually excludes time bounds. While it is true that we do not know today how to specify time bounds precisely, that does not absolve us from writing programs that have to honor these bounds. The advantage of moving to more abstract and mathematical semantics is that we can reason more cleanly. The disadvantage is that we can no longer write time- or space-constrained programs. It seems to me self evident that this puts the lie to the view that representation and optimization are non-semantic issues. While I recognize that I'm about to use a different sense of the term "meaning", there are real applications where people are killed when we get this stuff wrong, and that's about as required and as meaningful as anything I can imagine. If our notions of formal semantics in allegedly general-purpose programming languages aren't rich enough to address this type of real-world meaning, then it is our notions of formal semantics that must yield (or improve). shap _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
