Oracle FAQ Your Portal to the Oracle Knowledge Grid
HOME | ASK QUESTION | ADD INFO | SEARCH | E-MAIL US
 

Home -> Community -> Usenet -> comp.databases.theory -> Re: Bob's 'Self-aggrandizing ignorant' Count: Was: What databases have taught me

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@ursa-nb00s0.nbnet.nb.ca>


Marshall wrote:

> Bob Badour 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.
>>
>>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
>>instructs the compiler on how to implement to get the best possible
>>performance?
>>
>>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?
>>
>>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 Fri Jun 30 2006 - 17:11:35 CDT

Original text of this message

HOME | ASK QUESTION | ADD INFO | SEARCH | E-MAIL US