February 09
On Tuesday, 9 February 2021 at 14:14:42 UTC, Bastiaan Veelo wrote:
> This makes me wonder what certifying the tool practically brings to the table, apart from doors that can be entered with a certificate only. If certification of the tool does not improve the safety of the product and does not make it easier to test the safety of the product, I have the feeling that the certificate only improves perceived safety.

I quess the point is that at least the knowledge of the bugs the compiler has does not get old. If you always use the newest version of GCC for instance, there is the possibility that code changes due to new features or refactoring have caused new bugs since the bug manifestation site was last tested.

Still, one would think it'd be more efficient to certify a version of an open-source compiler from a public interest fund, and anyone could then use that version for free.
February 09
On Tuesday, 9 February 2021 at 15:10:55 UTC, Dominikus Dittes Scherkl wrote:
> I know, here are a lot of people that have very little trust in thoughts that someone else put into something, but it's their choice: use something certified or spent a lot of time to prove it yourself.
> If you proof it yourself anyway, a certificate maybe really useless for you.

I don't see how a certificate relieves you of the responsibility to consider the safety and quality of your tools yourself.

You use a certified compiler. The certified compiler produces a bug. As a result, a product that you released doesn't work. Does that mean that it isn't your problem? No, of course it doesn't! It's still 100% on you to fix it. With that said, I don't understand what you are paying for. Are you paying for the vendor to think about security? But why would you want to use a tool from a vendor who doesn't think about security to begin with? One way or another, the buck stops with you, not the vendor.

It's not that if you consider the safety and security of your tools yourself, the certificate is useless for you. It's that you have to consider the safety and security of your tools *whether or not* they're certified.
February 09
On Tuesday, 9 February 2021 at 15:37:42 UTC, FeepingCreature wrote:
> On Tuesday, 9 February 2021 at 15:10:55 UTC, Dominikus Dittes Scherkl wrote:
>> I know, here are a lot of people that have very little trust in thoughts that someone else put into something, but it's their choice: use something certified or spent a lot of time to prove it yourself.
>> If you proof it yourself anyway, a certificate maybe really useless for you.
>
> I don't see how a certificate relieves you of the responsibility to consider the safety and quality of your tools yourself.
>
> You use a certified compiler. The certified compiler produces a bug. As a result, a product that you released doesn't work. Does that mean that it isn't your problem? No, of course it doesn't! It's still 100% on you to fix it. With that said, I don't understand what you are paying for. Are you paying for the vendor to think about security? But why would you want to use a tool from a vendor who doesn't think about security to begin with? One way or another, the buck stops with you, not the vendor.

Probably if somebody attempts to sue you for negligence, you will be in a better position to defend yourself if you can show that you used a certified compiler than if you used something like GCC or Clang. So what you are paying for is for the vendor to assume some (though not all) of the risk of blame if your product has a defect. In other words, the certificate is an insurance policy.
February 09
On Tuesday, 9 February 2021 at 15:37:42 UTC, FeepingCreature wrote:
> On Tuesday, 9 February 2021 at 15:10:55 UTC, Dominikus Dittes Scherkl wrote:
>> I know, here are a lot of people that have very little trust in thoughts that someone else put into something, but it's their choice: use something certified or spent a lot of time to prove it yourself.
>> If you proof it yourself anyway, a certificate maybe really useless for you.
>
> I don't see how a certificate relieves you of the responsibility to consider the safety and quality of your tools yourself.
>
> You use a certified compiler. The certified compiler produces a bug. As a result, a product that you released doesn't work. Does that mean that it isn't your problem? No, of course it doesn't! It's still 100% on you to fix it. With that said, I don't understand what you are paying for. Are you paying for the vendor to think about security? But why would you want to use a tool from a vendor who doesn't think about security to begin with? One way or another, the buck stops with you, not the vendor.
>

I think there is a slight misconception in this thread that the certification is for the end product only when it is focused a lot on the processes that result in it. That also means that the vendor providing a certified product is under certain obligations. One of them is enabling the user of the tool to use it properly (e.g. a safety manual), another one is an obligation to manage defects. AFAIK this involves a process for notifying customers of critical bugs.

Nitpick: safety != security. Safety in this context means that the resulting product does not experience silent or undetected malfunctions. Security is resilience towards dedicated attacks on a system. These are different things, even though they overlap to some degree.

The reality is that a lot of ISO 61508 compliant environments are safe (i.e. the factory *will* shut down safely if things break), but terribly insecure (a hacker can take over and mess with tons of parameters).

> It's not that if you consider the safety and security of your tools yourself, the certificate is useless for you. It's that you have to consider the safety and security of your tools *whether or not* they're certified.

This. You need to invest considerable time and effort to establish processes and toolchains that are compliant. A tool certificate is no good if the processes around it are not compliant. There are many ways in which you can be non-compliant with a compliant toolchain. The impact of a certificate on your own processes is simply that tool qualification has already happened elsewhere.
February 09
On Tuesday, 9 February 2021 at 14:54:35 UTC, IGotD- wrote:
> On Tuesday, 9 February 2021 at 13:35:36 UTC, Gregor Mückl wrote:
>>
>> There is a fair amount of hate in this post that I can't agree with.
>
> Then you have a crewed up idea what hate means. Hate does not mean that you disagree with someone.
>

Please allow me to retract the part mentioning hate. That may have gone too far. I'm sorry if I offended you.

>> I've worked with certified compilers, too. It was mainly one of the major products in the field. The package was a mixed bag. The custom IDE is lacking and the proprietary build tools are not very good, but the actual compiler for our target platform turned out to be very good. We threw it at a pretty big preexisting codebase and it worked (we had a few places where we were relying on subtle UB - that's on us). Compared to GCC, the generated code would consistently be smaller and thus faster, even when I compared unoptimized builds to GCC with optimizations (curiously, speed optimized GCC output was smaller than size optimized output!).
>
> The main reason some company uses a certain "certified" compiler is because the customer demands it. There in between anything is possible with any kind of back room deal. Just like doctors get money under the table in order to promote a certain drug, which we know is commonplace.
>

This is not representative of all industries everywhere. My own personal experience showed  me that there are places where this is taken seriously for good reasons. It seems that you and I have made very different experiences during our careers. Nothing wrong with that, I guess.

> The compiler I have worked with had a number of bugs and then I tried GCC and of course it ran perfectly with better code generation. The answer is of course obvious GCC is used by the hundreds of thousands and many contributing to the compiler. This compared to a small company creating some "certified" compiler. I'm all of commercial SW but I cannot deny that the huge backing of the GCC compilers is hard to beat. If I would decide which compiler to use I would of course go with GCC and skip the certified compiler, however it is the customers that dictates what to use.

In my experience, the quality of GCC code generation varies a lot depending on the target platform. It's an extremely good compiler for desktop/server class CPUs, but in my experience, it doesn't target small embedded platforms very well. This low end seems to be too niche to attract many developers to GCC or LLVM.
February 09
On Tuesday, 9 February 2021 at 13:42:51 UTC, Max Haughton wrote:
> On Tuesday, 9 February 2021 at 13:35:36 UTC, Gregor Mückl wrote:
>> On Tuesday, 9 February 2021 at 10:10:05 UTC, IGotD- wrote:
>>> [...]
>>
>> [...]
>
> What architecture was this running on? I say that because small is often not fast on a big machine - and the reason why fast gave smaller code is probably because of the weird non-determinism you get in big compilers as more stuff is inlined giving way to more information for the optimizer to use locally.

The specific project that allowed me to make that comparison had an ultra low power Cortex-M4. That's an in-order design with 3 pipeline stages and no optimizations for branching. So it's primitive enough that raw instruction count translates directly into performance.
February 09
On Tuesday, 9 February 2021 at 17:25:17 UTC, Gregor Mückl wrote:
> On Tuesday, 9 February 2021 at 13:42:51 UTC, Max Haughton wrote:
>> On Tuesday, 9 February 2021 at 13:35:36 UTC, Gregor Mückl wrote:
>>> [...]
>>
>> What architecture was this running on? I say that because small is often not fast on a big machine - and the reason why fast gave smaller code is probably because of the weird non-determinism you get in big compilers as more stuff is inlined giving way to more information for the optimizer to use locally.
>
> The specific project that allowed me to make that comparison had an ultra low power Cortex-M4. That's an in-order design with 3 pipeline stages and no optimizations for branching. So it's primitive enough that raw instruction count translates directly into performance.

I'm slightly surprised GCC generated larger code, but I can see it happening for something of that size.
February 09
On Tuesday, 9 February 2021 at 16:58:35 UTC, Gregor Mückl wrote:
> On Tuesday, 9 February 2021 at 15:37:42 UTC, FeepingCreature wrote:
>> On Tuesday, 9 February 2021 at 15:10:55 UTC, Dominikus Dittes Scherkl wrote:
>>> I know, here are a lot of people that have very little trust in thoughts that someone else put into something, but it's their choice: use something certified or spent a lot of time to prove it yourself.
>>> If you proof it yourself anyway, a certificate maybe really useless for you.
>>
>> I don't see how a certificate relieves you of the responsibility to consider the safety and quality of your tools yourself.
>>
>> You use a certified compiler. The certified compiler produces a bug. As a result, a product that you released doesn't work. Does that mean that it isn't your problem? No, of course it doesn't! It's still 100% on you to fix it. With that said, I don't understand what you are paying for. Are you paying for the vendor to think about security? But why would you want to use a tool from a vendor who doesn't think about security to begin with? One way or another, the buck stops with you, not the vendor.
>>
>
> I think there is a slight misconception in this thread that the certification is for the end product only when it is focused a lot on the processes that result in it. That also means that the vendor providing a certified product is under certain obligations. One of them is enabling the user of the tool to use it properly (e.g. a safety manual), another one is an obligation to manage defects. AFAIK this involves a process for notifying customers of critical bugs.
>
> Nitpick: safety != security. Safety in this context means that the resulting product does not experience silent or undetected malfunctions. Security is resilience towards dedicated attacks on a system. These are different things, even though they overlap to some degree.
>
> The reality is that a lot of ISO 61508 compliant environments are safe (i.e. the factory *will* shut down safely if things break), but terribly insecure (a hacker can take over and mess with tons of parameters).
>
>> It's not that if you consider the safety and security of your tools yourself, the certificate is useless for you. It's that you have to consider the safety and security of your tools *whether or not* they're certified.
>
> This. You need to invest considerable time and effort to establish processes and toolchains that are compliant. A tool certificate is no good if the processes around it are not compliant. There are many ways in which you can be non-compliant with a compliant toolchain. The impact of a certificate on your own processes is simply that tool qualification has already happened elsewhere.

Correct. Safety and security are not really related. And even under the word safety there are different kinds of safety. For example the definition of a safe state is very different in different environments. For example in the nuclear sector some doors must *open* on failure while in some other sector they must *close*.

Also in the mobile sector (I've worked as a control systems developer for harvester heads) the definition of a safe state can be both to freeze all valves etc, but also to release all energy of the system depending on various factors (PLD cat3 iirc in that case).

So it's a complex topic that's for sure 😁

Today I work as a systems architect on a radio remote control company and safety is (unsurprisingly) important ofc.

I'm not really sure we need a certified compiler (although we currently have one for certain products). We have a dialog w most certification "institutions" and tbh some times I'd say we know better then they do what is really safe (depends ofc). There are also other techniques like black channel/box etc etc but that's another topic.

I'm writing on the phone atm, I can elaborate on what our requirements would be later. But one reason I looked into D in the first place was actually @safe and the things Walter talked about.

I have hope for D being useful for us.


February 09
On Tuesday, 9 February 2021 at 19:59:02 UTC, Imperatorn wrote:
> On Tuesday, 9 February 2021 at 16:58:35 UTC, Gregor Mückl wrote:
>> [...]
>
> Correct. Safety and security are not really related. And even under the word safety there are different kinds of safety. For example the definition of a safe state is very different in different environments. For example in the nuclear sector some doors must *open* on failure while in some other sector they must *close*.
>
> [...]

I would like to write a bounded model checker for D although I make no guarantees because it's one more mad idea for the list of many mad ideas I have.
February 10
> I would like to write a bounded model checker for D although I make no guarantees because it's one more mad idea for the list of many mad ideas I have.

I have been considering the feasibility of implementing a model checker in D, but a symbolic one, mainly because of the convenience of having straightforward control over the GC. I've built some tiny bits (an extremely basic implementation of decision diagrams and a parser for Büchi automata used in LTL model checking).

It's a long project but IMHO it would be useful, if nothing else as a benchmarking tool with respect to other model checkers written in different languages (Java, C++) or different implementation choices (gc, nogc).

1 2 3 4 5