From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!news.swapon.de!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail From: Niklas Holsti Newsgroups: comp.lang.ada Subject: Re: Languages don't matter. A mathematical refutation Date: Thu, 09 Apr 2015 21:40:06 +0300 Organization: Tidorum Ltd Message-ID: References: <87oan56rpn.fsf@jester.gateway.sonic.net> <877fts7fvm.fsf@jester.gateway.sonic.net> <87twwv66pk.fsf@jester.gateway.sonic.net> <32ecaopodr1g.1xqh7ssdpa2ud.dlg@40tude.net> <87pp7j62ta.fsf@jester.gateway.sonic.net> <87pp7hb2xo.fsf@jester.gateway.sonic.net> <5rxvgyes5xg8.1mqq86gacbsb1.dlg@40tude.net> <87lhi5ayuv.fsf@jester.gateway.sonic.net> <87oan0aote.fsf@jester.gateway.sonic.net> <878ue3ff6y.fsf@jester.gateway.sonic.net> Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 7bit X-Trace: individual.net quqTU8DHlZq9gJmDu+PlKg4qXWe3sfeHuHxFbX5oHx6L8JcCAR Cancel-Lock: sha1:m9aYmluTcE3o1ZexQpgZaYbqi5o= User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:31.0) Gecko/20100101 Thunderbird/31.6.0 In-Reply-To: Xref: news.eternal-september.org comp.lang.ada:25496 Date: 2015-04-09T21:40:06+03:00 List-Id: 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 . @ .