Re: Languages don't matter. A mathematical refutation

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

On 15-04-09 17:35 , Dmitry A. Kazakov wrote:
> On Thu, 09 Apr 2015 15:14:59 +0200, G.B. wrote:
>
>> Now, WRT storage management, assume a bounded container.
>> The implementation may pre-allocate the maximum number of
>> objects.(*) Given that, why should it not be possible at all,
>> in no case, to guarantee a known complexity of storage
>> management? A bounded vector, say, could specify its
>> storage management needs, on condition that ... Much like
>> a hash table package would state that
>>
>>     "As long as the number of slots is as least N/M,
>>      finding an object will take no more than f(M, N, g(Hash))."
>
> Which is elementary incomputable, as it contains the future tense and thus
> cannot be a part of any contract.

It is quite possible to extend the semantics of a programming language 
with a predefined global (or task-specific) variable "elapsed execution 
time", and the above contract can be stated as a constraint on the 
difference between the pre- and post-values of this variable.

In fact, Ada.Execution_Time provides such variables. The Time_Remaining 
function could be used to express the above constraint.

>> Like everything that actually handles program data, GC does
>> influence the program's behavior, e.g. by taking time.
>
> That is not the program behavior. The behavior is only things related to
> the program logic = functional things.

This is niggling about words, but for real-time systems the execution 
time of computations is certainly an important property of the program, 
whether it is called "behaviour" or not.

That it is a platform-dependent property does not make it less important 
- only harder to manage. Formal analysis tools such as SPARK already 
take into account other platform-dependent properties such as the range 
of the predefined Integer type. The formal analysis tools called 
Worst-Case Execution-Time (WCET) Analyzers try to prove exactly this 
kind of contracts, sometimes using very detailed models of the platforms.

Of course garbage collection (GC) complicates WCET analysis a lot, at 
least if it is done synchronously, interrupting the normal computation 
at unpredictable times. A "background" GC would be more manageable, 
perhaps running on a dedicated core or in a low-priority task. (It is 
then necessary to prove, by some analysis, that the garbage-collection 
rate is sufficiently higher than the garbage-creation rate that a memory 
allocation never fails. That would be similar to analyses already being 
done, such as schedulability analyses and analyses to show that buffers 
never overflow.)

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .