Re: Bob's 'Self-aggrandizing ignorant' Count: Was: What databases have taught me
From: Bob Badour <bbadour_at_pei.sympatico.ca>
Date: Fri, 30 Jun 2006 22:11:35 GMT
Message-ID: <rkhpg.4299$pu3.101199_at_ursa-nb00s0.nbnet.nb.ca>
>
> I see no particular theoretical difficulty. A type system could be
> designed
> that would handle the above. What is necessary is that the type system
> have an accurate measure of the ceiling of every kind of node in the
> abstract
> syntax of the language, parameterized on the child nodes.
>
> Such a language could not be Turing complete, or perhaps could have a
> non-Turing complete subset. For example, one might allow a top level
> event loop that itself took infinite CPU cycles (in that it never
> terminates)
> but each iteration through the loop was guaranteed to complete within
> some
> upper bound of time. One could statically analyze any resource this
> way:
> heap space, stack space, file handles, CPU time, etc.
>
> The type system would be more than usually bound to a particular
> machine
> architecture, but this detail could perhaps be abstracted out. So we
> could
> prove that this program executes in less than 30 s. on a pentium, but
> that same proof would not be valid for a 486.
Date: Fri, 30 Jun 2006 22:11:35 GMT
Message-ID: <rkhpg.4299$pu3.101199_at_ursa-nb00s0.nbnet.nb.ca>
Marshall wrote:
>>Absolutely. I have friends who have done real-time programming where the >>work had to be completed in assembler and where one had to prove the >>maximum number of CPU cycles consumed in the worst-case situation did >>not exceed some threshold. >> [Quoted] >>These observations naturally lead one to two important questions: >> >>1) Can one create a pair of languages where the proofs written in one >>language establish the correct outcome and where some other language [Quoted] >>instructs the compiler on how to implement to get the best possible >>performance? >> [Quoted] >>2) Could one create a compiler to translate proofs as above in 1) into >>assembler code with an automated proof that the maximum number of CPU >>cycles consumed in the worst-case situation would not exceed some threshold? >> [Quoted] >>These then lead into a third question: Can one combine the above >>features in a single product?
>
> I see no particular theoretical difficulty. A type system could be
> designed
> that would handle the above. What is necessary is that the type system
> have an accurate measure of the ceiling of every kind of node in the
> abstract
> syntax of the language, parameterized on the child nodes.
>
> Such a language could not be Turing complete, or perhaps could have a
> non-Turing complete subset. For example, one might allow a top level
> event loop that itself took infinite CPU cycles (in that it never
> terminates)
> but each iteration through the loop was guaranteed to complete within
> some
> upper bound of time. One could statically analyze any resource this
> way:
> heap space, stack space, file handles, CPU time, etc.
>
> The type system would be more than usually bound to a particular
> machine
> architecture, but this detail could perhaps be abstracted out. So we
> could
> prove that this program executes in less than 30 s. on a pentium, but
> that same proof would not be valid for a 486.
In general, it wouldn't need to be valid on multiple CPU's. The most critical stuff related to interrupt handlers, if I recall correctly. Received on Sat Jul 01 2006 - 00:11:35 CEST