Golang for Mission Critical Projects

[Ji Park]

Hello, I've been hearing a lot of good things about Golang for a while and tried playing around with it and so far I'm loving it!

I was just wondering, does anyone know if Golang can be a good fit for machines/systems resulting in failure can lead to catastrophe or death?

I'd appreciate any response, thanks.

[Ian Lance Taylor]

On Wed, Jan 28, 2015 at 11:49 AM, Ji Park <jhp...@gmail.com> wrote:
>
> Hello, I've been hearing a lot of good things about Golang for a while and
> tried playing around with it and so far I'm loving it!
>
> I was just wondering, does anyone know if Golang can be a good fit for
> machines/systems resulting in failure can lead to catastrophe or death?

Speaking strictly for myself, I would hope that as much as possible
machines that can lead to catastrophe or death would not use
computers. And if they must use computers, I would hope that there
would be multiple levels of defense against very bad results, so that
there have to be multiple bugs at several levels before anything very
bad happens.

With regard to Go in particular, I'm not aware of anybody who has
tried to vet the code for this level of care. But then, I'm not aware
of anybody having vetted the average C++ compiler either. So the
question is: what is your alternative?

Ian

[andrewc...@gmail.com]

You could have redundancy with 2 different implementations completed by different parties following a reviewed spec, then
also run the same code with both gccgo and gc and have the 4 versions "vote" on correct system ouput values.

Go does not have any sort of equivalent to http://compcert.inria.fr/ or other formal verification tools I am aware of.

[Silvan Jegen]

On Wednesday, January 28, 2015 at 9:36:06 PM UTC+1, Ian Lance Taylor wrote:

On Wed, Jan 28, 2015 at 11:49 AM, Ji Park <jhp...@gmail.com> wrote:
>
> Hello, I've been hearing a lot of good things about Golang for a while and
> tried playing around with it and so far I'm loving it!
>
> I was just wondering, does anyone know if Golang can be a good fit for
> machines/systems resulting in failure can lead to catastrophe or death?

Speaking strictly for myself, I would hope that as much as possible
machines that can lead to catastrophe or death would not use
computers.  And if they must use computers, I would hope that there
would be multiple levels of defense against very bad results, so that
there have to be multiple bugs at several levels before anything very
bad happens.

I am sure that you are not alone in this opinion because I wholeheartedly agree :P

 

With regard to Go in particular, I'm not aware of anybody who has
tried to vet the code for this level of care.  But then, I'm not aware
of anybody having vetted the average C++ compiler either.  So the
question is: what is your alternative?

 

As long as your code cannot pass formal verification (which may not even be possible with a language that does allow for (uncontained?) side effects, but I am not an expert) I don't think anyone can be sure that a system is reliable enough to be trusted. Even when using formal verification you have to put trust into your formal verification process, programs and runtime...

Reducing the complexity of your programs and implementing several layers of checks/failover systems seems like the best approach if you can't do without software in your mission critical systems.

You can imagine that I am not a big fan of the "Internet of Things" but that could just be me...

Given these caveats I don't think Go would be better or worse for such systems than other programming tools that allow for side effects.

Cheers,

Silvan

[Kostarev Ilya]

`Haskell` having richer type system provide more compiler guarantees, so widely used in finance.

`Ada` compilers are  more strictly vetted in accordance with standard formal specification, so widely used by military.

-- 
Kostarev Ilya

On 28 Jan 2015 at 23:35:54, Ian Lance Taylor (ia...@golang.org) wrote:

On Wed, Jan 28, 2015 at 11:49 AM, Ji Park <jhp...@gmail.com> wrote:
>
> Hello, I've been hearing a lot of good things about Golang for a while and
> tried playing around with it and so far I'm loving it!
>
> I was just wondering, does anyone know if Golang can be a good fit for
> machines/systems resulting in failure can lead to catastrophe or death?

[Ian]

I'd check state regulations (it's an arduous task, to be sure!) Some of them, for inexplicable technical but somewhat obviously political/lobbying reasons, a quite specific about languages and the technology that can be used. I forget which one, but I remember being told that at least one state bars Visual Basic in medical equipment, for instance. I don't know if it's still there, but Java had a license provision that barred its use in nuclear power systems. I know it took awhile for iPad's to be approved for use in airliner cockpits, simply because there were legitimate questions about the device's reliability versus paper maps! 

If I were to look at Go for such a system, I'd examine the concurrency code *very* carefully - Go is not a real-time systems language. The things that make concurrency so easy and wonderful make it less than desirable for a system such as you ask about! (I'd also think about the garbage collection code; I've not seen it, but it might be worth thinking about those infamous GC-pauses. Would they upset any real-time code that was running or needed to run?) It depends on what you're trying to do; if failure to run a Go routine exactly on time, for instance, would result in some poor soul prematurely meeting his or her maker, then you need to think very carefully about your language choice, system architecture and design. On the other hand, as long as something happens, as it were, within particular time boundaries and you can figure out, and, for your lawyer's continued sunny disposition, mathematically prove that you satisfy those conditions, Go *might* be the perfect language for your application! 

In short, your question is actually a too vague to be reasonably and properly answered. 

[Niklas Schnelle]

One language that is from the ground up explicitly designed for mission critical use is Ada. It has an extremely strong type system

that has ways to specify things like integer between 10 and 16 or float with at least x precise digits. Also it comes with nice concurrency

support that ravels even that of Go, especially with things like explicit rendezvous. One problem though is that the the GCC implementation and

it's commercially supported GNAT derivative are somewhat less stable and going for the military grade implementations is expensive. Still, 

this is definitely the programming languages with the highest language level safety features.

While I agree with Ian that computers in life critical systems should be well thought out they are definitely a reality and in many situations we simply can't

built systems without computers be it spacecraft, ABS systems in cars or even self driving vehicles. That said with proper fail safe design,

good review processes etc. I'd much rather trust a computer with my life than the average human. Especially with self driving cars the hard reality is

that we will definitely see computers killing humans, either through things like computer vision just not being good enough or even through real bugs,
still the number of people killed in car accidents will drop significantly simply because even with all their faults computers don't get tired and will

make far fewer deadly mistakes than human drivers, so I guess we will just have to deal with it.

[anl...@gmail.com]

until self driving flying cars (over seas etc)
imagine a time glitch hitting at once
ba dum tss

[Ian]

On Thursday, January 29, 2015 at 11:45:08 AM UTC-5, Niklas Schnelle wrote:

 

While I agree with Ian that computers in life critical systems should be well thought out they are definitely a reality and in many situations we simply can't built systems without computers be it spacecraft, ABS systems in cars or even self driving vehicles. ...

Not exactly on topic, but... As an avid and long-standing motorcyclist, I'd say we've had driverless cars for quite some time!

[j...@nella.org]

I think the final decision will be legal/financial and not technical.

But when you go to talk with the regulators to get your choice of language pre approved (and later when you do your audit for your license), you can and should point out that pure Go dramatically reduces the risk of pointer errors that you have in C Abe C++. You can also point of that the GC pause time is strictly bounded for bounded memory use. So if you have failsafes in place ensuring your max mem is 100megs, then you can probably show that the the max GC time is (eg) 5 ms. Finally, our experience with godrone.io is that in soft realtime systems, Go can be a good fit because you can calculate the upper bound on missed deadlines. (Soft realtime = missed deadlines, up to a point, do not result in catastrophic failure.) Our target quadricopter has a cycle of 200 hz. Missing two cycles (10 ms) due to GC would not cause a crash.

Jeff

[Paul]

This is all very interesting and I have to say some of the answers have an eyebrow raising effect on me. If ADA was the last language to be designed with inherent safety and security in mind, then where would that put us? 

<tongue-in-cheek on>

I'm reminded of Elon Musk's warning about creating a Skynet super-intelligent entity by accident sometime in the next 5-10 years. Kind of a humorous notion that is, until you see Henry Markrams work on the 'Blue Brain' project. 'Blue Brain' is modeled with Neuron which is written in C++ and Fortran. And I'm not trying to say that we are going to be better off if it all gets rewritten in Go. 

</tongue-in-cheek off>

[Uriel Fanelli]

I fully agree with that, but sometimes EAL certifications are requested.

Sometimes the customer is requiring it.

A producer of dishwashers was forced to recall 200,000,000 dishwashers because of a bug. 

The bug created in total 9 waterflood in the planet. 9 on 200.000.000 means you need something like EAL5+.

So, imagine now the IoT is coming, and each and every big producer starts to ask you to fail less than

9 times on 200 millions.

Also, when doing ASIC/SoC you are going to be formally verified by the silicon foundry.

So, in my humble opinion, a tool for doing formal verificaiton is a must for golang. This is because:

1. You can audit your software before of getting reported, saving project times.
2. You can audit 3rd party libraries before of using them, or deciding to write your own ones.

don't take me wrong, I don't say testing is not good. I say tests are missing the capability to write formal policies,

which are needed for EAL certification.

I think a little improvement from google could make the testing library able to manage formal policies, and this at the beginning of IoT era,

could be a winner.

Just my two cents, of course.

Uriel

[Benjamin Measures]

On Saturday, 23 May 2015 14:59:04 UTC+1, Uriel Fanelli wrote:

So, imagine now the IoT is coming, and each and every big producer starts to ask you to fail less than

9 times on 200 millions.

On economics, the IoT will lead to /less/ testing not more, with the incentive that internet updates avoids the need (and thus the cost) for expensive recalls.

[Uriel Fanelli]

I don't agree. Insurance companies are giving a damn of what you do AFTER a car crash happened because of faulty software: they want

to know how much times it will fail in average.

Currently in automotive they are asking less than 1 fault per 10^9 hours. 

I can't see why insurance companies should take more risks just because you can update a dishwasher after it has flooded your apartment. In big part of Europe

 it is mandatory to have house insurance and building insurance. And insurance companies won't pay until all the electrical appliances aren't certified. And not

"the future releases" . What you have now.

It is even in doubt if insurance companies will accept something like "internet upgrade": we aren't speaking about phones, we talk about cars and electric appliances.

By example with "industrial internet" and "M2M" they didn't changed a bit of their position, and companies are going to ask certifications and formal verification.

I can't see why they should take liabilities on themselves: they are not charities.

[Henrik Johansson]

That is funny, what good are insurance companies then?

--
You received this message because you are subscribed to the Google Groups "golang-nuts" group.
To unsubscribe from this group and stop receiving emails from it, send an email to golang-nuts...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Uriel Fanelli]

They do business. And they are not going to cover software which is mostly , sorry to say, bullshit.

I know, after 30 years of software which comes "AS IS" , "with no accountability", 

as the normal EULA says,  people expecting it works can look strange.

But, when you buy a car, you don't want the cas says "we have a problem, windows is checking for a solution"....

This was acceptable when OS and software were doing mostly nothing impacting. If you want IoT, you need to

face the fact you expect objects at your home to work. to be safe. To be stable.

If you want to sell "home IoT", your software will need to work as good as the old appliances with no IoT. 

When I power up my light, it simply works. It works since 15 years, the same, 100% of time, 100% good.

And I did no update. Seamless.

Either your IoT light will work the same, or the insurance will prevent me to use it, and I will think the insurance is right.

Why should an insurance company introduce the concept of "bug" i devices which have, right now, 0 bugs at all?

[andrewc...@gmail.com]

On Tuesday, May 26, 2015 at 8:21:45 AM UTC+12, Uriel Fanelli wrote:

They do business. And they are not going to cover software which is mostly , sorry to say, bullshit.

Much embedded software is very low quality already, it will probably get worse with more people rushing in.
 

I know, after 30 years of software which comes "AS IS" , "with no accountability", 

as the normal EULA says,  people expecting it works can look strange.

 

We already have software in most of our home appliances.  I don't know why you think it is any different.

But, when you buy a car, you don't want the cas says "we have a problem, windows is checking for a solution"....

I think many car companies already do updates over the air.

This was acceptable when OS and software were doing mostly nothing impacting. If you want IoT, you need to

face the fact you expect objects at your home to work. to be safe. To be stable.

If you want to sell "home IoT", your software will need to work as good as the old appliances with no IoT. 

When I power up my light, it simply works. It works since 15 years, the same, 100% of time, 100% good.

And I did no update. Seamless.

Hopefully people can write code good enough to run a light bulb without formal verification.
 

 

Either your IoT light will work the same, or the insurance will prevent me to use it, and I will think the insurance is right.

Why should an insurance company introduce the concept of "bug" i devices which have, right now, 0 bugs at all?

This is clearly wrong, all products have defects, even current ones, this is what recalls are about.


The level of certification should match the level of safety required. Go does not currently cover the highest level of safety requirements.

[Uriel Fanelli]

On Tuesday, May 26, 2015 at 8:06:53 AM UTC+2, andrewc...@gmail.com wrote:

On Tuesday, May 26, 2015 at 8:21:45 AM UTC+12, Uriel Fanelli wrote:

They do business. And they are not going to cover software which is mostly , sorry to say, bullshit.

Much embedded software is very low quality already, it will probably get worse with more people rushing in.

Embedded software you are talking about  is used in devices which are not under insurance, not doing any liability and
not able to start fires, flooding or damage third parties. They can only hang the device, not more.

 

 

I know, after 30 years of software which comes "AS IS" , "with no accountability", 

as the normal EULA says,  people expecting it works can look strange.

 

We already have software in most of our home appliances.  I don't know why you think it is any different.

No, you don't. And this is the point. You still power up lights with old, legacy  switches, your dishwasher is mostly
a ROM with some electronics. You can call it "software" if you like,  but you know what we are talking about is something different.

 

But, when you buy a car, you don't want the cas says "we have a problem, windows is checking for a solution"....

I think many car companies already do updates over the air.

ONly for multimedia systems, which are not crucial for the car. From 2017 all new car in Europe MUST have e-call embedded,
and it is crucial for insurance. Car companies are actually asking for EAL5 .This is because insurance companies are relying on that.
 I can tell because this is my daily job: they DO require EAL5.

 

When I power up my light, it simply works. It works since 15 years, the same, 100% of time, 100% good.

And I did no update. Seamless.

Hopefully people can write code good enough to run a light bulb without formal verification.

I don't think so.
Firmware for industry is pretty able to do it, but it has different costs, different kind of developement cycle, mostly is developed in some kind of assembler,
and so on.

And none of them is connected to the internet.

If you want to connect your bulb to the internet, then you need to implement a tcp stack. Do it if you like, and tell me the brand . So I won't buy one.
 

 

 

Either your IoT light will work the same, or the insurance will prevent me to use it, and I will think the insurance is right.

Why should an insurance company introduce the concept of "bug" i devices which have, right now, 0 bugs at all?

This is clearly wrong, all products have defects, even current ones, this is what recalls are about.

No. I never needed an antivirus for my dishwasher. I never needed to reboot it to "refresh" some black magic lost in millions of row of code.
I am powering my bulb clicking some switch in the wall, which is not failing since years, never did an upgrade, neved needed some antivirus,
never needed any os upgrade, neved needed any configuration, neved needed any kind of support. And since it is TÜV-certified, it will fail
some times after some tenth of millions of click, in the average.

When any operating system will be reliable as the light switch I have in the wall, I think I will be dead since a couple of centuries.

And now, try to convince my insurance that I have to change it with something which fails, like windows , each 2600 hours in the average.
(microsoft only grants this amount, then they say "do a cluster for HA". ) .



 

The level of certification should match the level of safety required. Go does not currently cover the highest level of safety requirements.

But IoT will soon ask for it. Well, maybe not, since most of producers are now looking for silicon : SoC, ASIC, and so on. So probably we will have
a switch connected to the internet,

http://www.asix.com.tw/products.php?op=pItemdetail&PItemID=90;72;103

So you will have your bulb connected to the internet, 100% of verification (SoC are 100% formal verified).

But this is not a "good news" for developers.

[Michael Schaller]

FYI: There is MISRA C and C++ by the Motor Industry Software Reliability Association. MISRA is a set of guidelines to facilitate code safety, portability and reliability in the context of critical embedded systems.

If you take MISRA as a basis you might be able to come up with good Go guidelines...

On Tuesday, May 26, 2015 at 8:06:53 AM UTC+2, andrewc...@gmail.com wrote:

[Niklas Schnelle]

I would think that very few if any guidelines that make sense for safety critical C/C++ make sense in Go. Garbage Collection, automatic stack allocation and an extremely strong type system make Go vastly different

when it comes to dangerous coding practices. For Go the most useful guidelines would probably be something along:

- Don't use CGO so we steer clear of classic C/C++ problems and avoid one of the most intricate Go internals

- Do real code reviews, maybe even print out the code and read it away from the distractions of a computer

- Don't use anything from the unsafe package ever.

- Do proper estimation of heap size and plan for plenty of margins as Go allocations can only fail by killing the program -> make the program getting killed results in a safe situation

Also Go isn't safe for hard real time systems mainly because of garbage collection and hard to analyse goroutine timing behavior.

That said while Go isn't fit for hard real-time there are plenty of soft real time systems where I would be more comfortable with a Go implementation than any other language except maybe Ada.
I would say that Go is very well suited for:

- Smart door locks and other safety critical software that depends on encryption and/or communication, like ioT Hubs

- Safety critical planning or financial applications

- Data safety applications, data bases, backup solutions, cloud management and general backend software that can't guarantee hard real time anyway because it uses unpredictable packet networking (the Internet)

[Uriel Fanelli]

I confirm.
I was refering to the FRAMA-C  implementation of MISRA we use.

Please notice, using MISRA with FRAMA-C, or with whatever checker you want, is "semiformal verification plus something",
which means ~EAL5+

I don't know how hard is to port such a system: testing in go is not done using policies.

[Uriel Fanelli]

I won't say that.

If you think how you do formal verifications  , you are going to do something like that:

// true.i 
int main(void) 
{
 /*@ assert \true; */ 
return 0; 
}

so this will work because it returns true
But, when you do like:

// false.i 

int main(void) { 
int x = 0; 
/*@ assert x+1 == 0; */ 
return 0; 
}

what you get using the analyzer is:

Assertion failed at line 7.
The failing predicate is: (x+1 == 0).

so this means you are writing pseudo-comments which some parser is going to verify with the remaining part of the code.

I don't think it would be such harder to implement in go, being honest.

[Daniel Barrett]

Comments and code have a tendency to get out of sync. Do we have a tool to read these comment assertions and execute them? How do we verify this tool works correctly in all cases? In addition how do you cope with errors written by programmers in this new comment based language?

--

[Benjamin Measures]

On Tuesday, 26 May 2015 15:13:03 UTC+1, Uriel Fanelli wrote:

If you think how you do formal verifications  , you are going to do something like that:

You keep using that term- I do not think it means what you think it means.

It took ~20 person years to complete a formal verification of 7,500 lines of seL4 microkernel against a formal specification [1].

Nevertheless, I am reminded of Donald Knuth's famous words, "Beware of bugs in the above code; I have only proved it correct, not tried it". Indeed, a formal specification may not actually capture every requirement, due to oversight or lack of formal clarity such as "not able to start fires, flooding or damage third parties".

[1] http://ssrg.nicta.com.au/projects/TS/l4.verified/numbers.pml

[RickyS]

Embedded and Real-time systems programmers tend to avoid anything that smacks of Garbage Collection, as even a single pause can be fatal for many systems.  They tend to just use C and assembler.  For many systems that I've programmed, I found I needed to avoid even old-fashioned malloc/free during any critical process.  

In my opinion, Go is excellent for applications that run under an operating system.  That appears to be the sweet spot for Go.

However, we live in an era of self-driving cars, robo-surgeons, drones, et cetera, and low-level tools like C and assembler don't provide the productivity required.

[Uriel Fanelli]

On 05/27/2015 04:41 AM, Benjamin Measures wrote:

On Tuesday, 26 May 2015 15:13:03 UTC+1, Uriel Fanelli wrote:

If you think how you do formal verifications  , you are going to do something like that:

You keep using that term- I do not think it means what you think it means.

Indeed, I should have used "semiformal".

[Uriel Fanelli]

>
> Nevertheless, I am reminded of Donald Knuth's famous words, "Beware of
> bugs in the above code; I have only proved it correct, not tried it".
> Indeed, a formal specification may not actually capture every
> requirement, due to oversight or lack of formal clarity such as "not
> able to start fires, flooding or damage third parties".

Maybe, but I was not talking of rewriting every line of code in lambda
notation and use Hoare logics .
Still, if you want to do it, there are many automatic proof assistant
now, which can speed the job.

In any case, after a semiformal verification, the quality of software is
much, much, much higher.

And yes, undert the point of view of insurances, this matters.

But, again, at the end, living means to face reality, so let's see what
will happen....

[Alex D. Guerrieri]

There is something similar in Go: testable examples

You can use comments in *_example files to check a metodo output on stdout, and go test will execute and test also these assertions.

[Uriel Fanelli]

I was not aware of this functionality, so thank you.

So go is ready for semiformal verification...

[Eric Johnson]

Seems like there's lots of possibilities in Go for static validation. Rather than try to write additional assertions, use analysis of the code to determine issues.

For example, a routine that allocates an array based on a passed integer parameter should disallow values less than zero. That constraint can then be checked against all the sources of values to the function.

Or, for example, a file opened that isn't closed before a routine exits (not called via defer, for example).

In Java, you can use a tool like FindBugs to accomplish this analysis. I've been thinking Go could benefit from such a tool.

[demetri...@gmail.com]

DO NOT USE GO WHEN HUMAN LIFE IS IN DANGER.

Hire someone who has many years of experience with life-critical systems. Then do EXACTLY what that person says.

[Paul Borman]

On Tue, Jul 14, 2015 at 5:45 AM, <demetri...@gmail.com> wrote:

DO NOT USE GO WHEN HUMAN LIFE IS IN DANGER.

Hire someone who has many years of experience with life-critical systems.  Then do EXACTLY what that person says.

I don't think you need the qualifier on Go.  It is a statement about nearly all software "DO NOT USE THIS SOFTWARE IN LIFE CRITICAL APPLICATIONS."  How many programmers want the device that is keeping them alive to depend on software they wrote (aside from Tony Stark).  I don't think Go is of any greater threat than any other language.  The threat is the person doing the work.  The suggestion of involving someone with years of successful experience is a good one (I think you can do s/life critical/cryptography/g as well).

    -Paul

[Jesper Louis Andersen]

On Wed, May 27, 2015 at 4:41 AM, Benjamin Measures <saint....@gmail.com> wrote:

It took ~20 person years to complete a formal verification of 7,500 lines of seL4 microkernel against a formal specification [1].

Luckily, formality is a continuum between 0 and 1. Around 0, you have exploratory testing and unit testing. At 1 you have what the seL4 formal proof did. While expensive, the first approaches on new ground always take longer than expected, and things will probably speed up once you begin understanding what it takes to do formal proofs of stuff.

But you can also go in between. Model checking sits pretty close to 1. As does QuickChecking. The effort is vastly shorter, especially if you have experience. My own QuickCheck experience is that you can do it roughly as fast as a good covering unit test, but yielding far more subtle bugs found. It does take some modeling experience to make it fast, however.

The nice thing about model checking is that you don't have to carry out the proof. You just push a button, let the 10k machine cluster do its work and wait for the result. If there is a bug, you will get a minimal counterexample. If it says "ok", you can decide if you want to add the effort of a formal proof of correctness. It is a pretty effective method as well: the window between mechanized formalizations and a completed model check is surprisingly small in practice.

--

J.

[demetri...@gmail.com]

I was referring specifically to the Go run-time system, which every Go program uses. C, C++, and Ada have (I believe) much smaller run-times, which are much easier to certify for critical applications.

[Henry Adi Sumarto]

I think it is more of a design issue than a language issue, although the language choice does matter to a certain degree.

Hire someone who is experienced in developing such products, and let that person works in whatever language he is comfortable with. This is important because he / she needs to know the performance characteristics of the chosen language well in order to come up with a proper design.

[demetri...@gmail.com]

Agree completely.