Oracle FAQ Your Portal to the Oracle Knowledge Grid

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 <>
Date: Fri, 30 Jun 2006 22:11:35 GMT
Message-ID: <rkhpg.4299$>

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
>>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