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,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.157.3.208 with SMTP id f74mr3053860otf.1.1463796048282; Fri, 20 May 2016 19:00:48 -0700 (PDT) X-Received: by 10.140.101.170 with SMTP id u39mr207856qge.11.1463796048165; Fri, 20 May 2016 19:00:48 -0700 (PDT) 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.glorb.com!sq19no6810415igc.0!news-out.google.com!c13ni116673qge.1!nntp.google.com!88no5423593qga.1!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Fri, 20 May 2016 19:00:47 -0700 (PDT) In-Reply-To: Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=2601:191:8202:8510:5985:2c17:9409:aa9c; posting-account=fdRd8woAAADTIlxCu9FgvDrUK4wPzvy3 NNTP-Posting-Host: 2601:191:8202:8510:5985:2c17:9409:aa9c References: <5147eaaf-ca03-4288-8036-4f52c3364950@googlegroups.com> <2dc1c4a4-ec94-4cdf-95fc-c81f851c6845@googlegroups.com> <68713bb9-e92e-469a-834e-9e7b82009e48@googlegroups.com> <28f71c38-d6f5-4bde-9127-db32d3b018d8@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <3ad5a448-3e3a-4908-b87b-ee13a8c3c0ae@googlegroups.com> Subject: Re: Proof of array initialization in SPARK 2014 From: rieachus@comcast.net Injection-Date: Sat, 21 May 2016 02:00:48 +0000 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Xref: news.eternal-september.org comp.lang.ada:30442 Date: 2016-05-20T19:00:47-07:00 List-Id: On Thursday, May 19, 2016 at 2:12:49 PM UTC-4, Simon Wright wrote: > Dmitrij Novikov writes: >=20 > >> It may seem that I worry more about speed than correctness, but in > >> hard real time (like radar) when you are bit twiddling registers > >> inside interrupts, you want code that eliminates non-stack memory > >> references. > > > > Are CPUs fast enough for hard real time applications or is it > > necessary to use FPGAs or ASICs? >=20 > Normally hard real time systems are also fast real time systems, but > they need not be; the differentiation is that a hard real time system > *must* meet all its deadlines, according to Wikipedia[1]. Correct, I prefer the definition that results that don't arrive before the = deadline are wrong. It amounts to the same thing. As for using commercial = CPU chips, you very much don't want to work in virtual memory mode. Caches= if implemented nicely can be used in real-time systems, but they make meas= uring times very difficult. If you can meet your deadlines with the caches= disabled, and enabling the caches speeds everything up, you are good to go= . There are also some processors designed for the HRT business that have a= page of addressable static RAM instead of a cache. Extra work to figure o= ut what goes in the fast SRAM, but much easier to prove deadlines are met. = (It's nice when you can put all of the real-time operational code and data= in SRAM, and use DRAM for initialization and low-priority processes.) =20 > Myself, I would have thought it possible for only some of the deadlines > to be hard, while others could slip (but then, maybe they wouldn't count > as *dead*lines). It is fairly common for say an aircraft flight controller to have a number = of different deadlines, with preemption used to serve the earliest deadline= first. There will also be a priority level for tasks without explicit dea= dlines. It sounds simple, but for real systems you spend way more time pro= ving you can meet the deadlines than actually writing code. The issues involved in assigning priorities also get pretty messy during th= e requirements stage. Everyone thinks their data is important but, do they= really need it in 1 ms? How about 20 ms? Also let's say that the radar c= an track N hostile missiles or aircraft. However, dealing with that data m= akes the controls laggy, or pushes software for the ejection seat down. Yo= u may be better off limiting the system to N-1 or even N-2 bogies. (Hmmm, = to help you understand this: All aspect, zero-zero ejection seats are nice= . But they need a go-no go from the flight software so that the pilot does= n't get ejected into the ground. There may be an delay, and then the seat = ejects anyway, or more likely the flight software tells the seat in advance= when not to activate. Either way, very little extra processing, but very = time critical.)