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!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: How to get Ada to =?utf-8?Q?=E2=80=9Ccross?= the =?utf-8?Q?ch?=
 =?utf-8?Q?asm=E2=80=9D=3F?=
Date: Fri, 20 Apr 2018 12:34:35 -0700
Organization: A noiseless patient Spider
Message-ID: <87zi1xu0xg.fsf@nightsong.com>
References: <1c73f159-eae4-4ae7-a348-03964b007197@googlegroups.com>
	<878t9nemrl.fsf@nightsong.com>
	<de23c005-4b50-4910-9327-6d4acdaa7270@googlegroups.com>
	<87h8o7lowg.fsf@nightsong.com>
	<c15bd651-b717-420e-a0d2-7ed27289cd28@googlegroups.com>
	<8736zqkwat.fsf@nightsong.com>
	<6839088c-f221-4650-a6ea-1841ae539486@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org;
 posting-host="c64f90128f27b36aa0215bf95afe8b2a";
	logging-data="20015"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1/pWwHCE5FcXvRm37k83VUE"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (gnu/linux)
Cancel-Lock: sha1:FbQaCXY5hmROv9+GIqq/7Q0NT64=
	sha1:ufL2VfeR3+91Y1Kx7MNwdF+l0XQ=
Xref: reader02.eternal-september.org comp.lang.ada:51648
Date: 2018-04-20T12:34:35-07:00
List-Id: <comp.lang.ada>

"Dan'l Miller" <optikos@verizon.net> writes:
> Embedded realtime systems are going to be going mainstream in data
> processing with FPGAs in the datacenter.

Hmm.  FPGAs in the datacenter are usually about doing specialized
computation efficiently: examples include things like machine learning
using the DSP blocks on the FPGA's, or (famously) bitcoin mining.
So I wouldn't count that as either realtime or embedded.

Embedded usually means the processor is there to perform some
specialized computation to control hardware.  So seeing FPGA's in the
data center used for general purpose computation is actually cool
because it means FPGA's have escaped from the embedded realm.  They are
instead computing something and sending the answer over the internet.

Similarly, realtime to me means the answer must be delivered within some
specific deadline, usually measured in microseconds, or else disaster
ensues.  If the answer is being delivered over the internet, they any
interruption in network connectivity means the deadline is missed.    

So I can't consider anything running in a data center to be realtime
enough to need formal verification.  If your network reliability is
99.99% (on average it is out less than 1 second a day, including for
reasons like power failures) you are doing great.  Therefore it is
sufficient if your software delivers answers with 99.999% reliability, a
level you can easily reach with traditional testing methods.  The
likelihood of software failure is then swamped by the likelihood of
network failure.

Note that the 0.0001% failure allowance above doesn't mean that the
program is allowed to ever deliver wrong answers.  It just means that
the possibility of a deadline miss (where the program takes longer than
you expected, or fails to give you an answer at all) can be tolerated if
the likelihood is low enough.  Formal assurance against wrong answers is
most easily done by methods that are in tension with realtime
guarantees.  So deciding what methods to use requires understanding what
the complete system has to do.