www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - D for safety critical applications

reply Imperatorn <johan_forsberg_86 hotmail.com> writes:
Talking with some colleges. They have some questions regarding D:

1. Is D ready for prime time á la safety critical applications?
(I guess they mean GDC on ARM for example)

2. Are there any plans to make a certified compiler?
Feb 08
next sibling parent reply Gregor =?UTF-8?B?TcO8Y2ts?= <gregormueckl gmx.de> writes:
On Monday, 8 February 2021 at 11:09:49 UTC, Imperatorn wrote:
 Talking with some colleges. They have some questions regarding 
 D:

 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)

 2. Are there any plans to make a certified compiler?
What kind of safety critical applications are we talking about? Which certifications are you targeting for your product(s)? I'm not currently aware of any certified compilers for D. It would be cool if one existed, though.
Feb 08
parent reply Imperatorn <johan_forsberg_86 hotmail.com> writes:
On Monday, 8 February 2021 at 11:19:44 UTC, Gregor Mückl wrote:
 On Monday, 8 February 2021 at 11:09:49 UTC, Imperatorn wrote:
 Talking with some colleges. They have some questions regarding 
 D:

 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)

 2. Are there any plans to make a certified compiler?
What kind of safety critical applications are we talking about? Which certifications are you targeting for your product(s)? I'm not currently aware of any certified compilers for D. It would be cool if one existed, though.
I'm in a bit of a hurry atm, but basically IEC 61508 and ISO 26262 (we have older systems for EN 50128 and EN 50657 but they are not actively developed): https://www.iar.com/iar-embedded-workbench/certified-tools-for-functional-safety/
Feb 08
parent reply Denis Feklushkin <feklushkin.denis gmail.com> writes:
On Monday, 8 February 2021 at 13:17:31 UTC, Imperatorn wrote:

 What kind of safety critical applications are we talking 
 about? Which certifications are you targeting for your 
 product(s)?

 I'm not currently aware of any certified compilers for D. It 
 would be cool if one existed, though.
I'm in a bit of a hurry atm, but basically IEC 61508 and ISO 26262 (we have older systems for EN 50128 and EN 50657 but they are not actively developed): https://www.iar.com/iar-embedded-workbench/certified-tools-for-functional-safety/
In brief, how does it work? If a bug will be found in the compiler, certifying authority (or its staff) will be fined?
Feb 08
parent Dominikus Dittes Scherkl <dominikus scherkl.de> writes:
On Monday, 8 February 2021 at 23:01:17 UTC, Denis Feklushkin 
wrote:
 On Monday, 8 February 2021 at 13:17:31 UTC, Imperatorn wrote:

 What kind of safety critical applications are we talking 
 about? Which certifications are you targeting for your 
 product(s)?

 I'm not currently aware of any certified compilers for D. It 
 would be cool if one existed, though.
I'm in a bit of a hurry atm, but basically IEC 61508 and ISO 26262 (we have older systems for EN 50128 and EN 50657 but they are not actively developed): https://www.iar.com/iar-embedded-workbench/certified-tools-for-functional-safety/
In brief, how does it work? If a bug will be found in the compiler, certifying authority (or its staff) will be fined?
The certification only increases the trust in a SW generated by the certified tool. Without this certificate a tool is simply not allowed to be used to build ISO compliant SW. But the SW still need to be fully tested and the tool provider is not responsible for any undetected bug in the resulting SW. Of course a tool bug need to be documented, if its vendor wants to keep its certification. It is not even a fix required, not to mention fines :-)
Feb 09
prev sibling next sibling parent reply Paulo Pinto <pjmlp progtools.org> writes:
On Monday, 8 February 2021 at 11:09:49 UTC, Imperatorn wrote:
 Talking with some colleges. They have some questions regarding 
 D:

 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)

 2. Are there any plans to make a certified compiler?
Besides C and C++, I am only aware of Java (PTC/Aicas) and Ada compilers as fully certified compilers. Rust has one company driving the roadmap for such kind of deployments, https://ferrous-systems.com/blog/sealed-rust-the-pitch/ Whereas Wilderness Labs is driving .NET IoT efforts, however without certification in place, https://www.wildernesslabs.co/ I am not aware of similar efforts regarding D.
Feb 08
parent reply Imperatorn <johan_forsberg_86 hotmail.com> writes:
On Monday, 8 February 2021 at 15:12:47 UTC, Paulo Pinto wrote:
 On Monday, 8 February 2021 at 11:09:49 UTC, Imperatorn wrote:
 Talking with some colleges. They have some questions regarding 
 D:

 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)

 2. Are there any plans to make a certified compiler?
Besides C and C++, I am only aware of Java (PTC/Aicas) and Ada compilers as fully certified compilers. Rust has one company driving the roadmap for such kind of deployments, https://ferrous-systems.com/blog/sealed-rust-the-pitch/ Whereas Wilderness Labs is driving .NET IoT efforts, however without certification in place, https://www.wildernesslabs.co/ I am not aware of similar efforts regarding D.
We might not need the compiler to be certified if we can do other tests (like using Klee etc). But was curious if it had been discussed before.
Feb 08
parent rikki cattermole <rikki cattermole.co.nz> writes:
On 09/02/2021 4:44 AM, Imperatorn wrote:
 We might not need the compiler to be certified if we can do other tests 
 (like using Klee etc). But was curious if it had been discussed before.
Walter has said, that we won't do certification without a reason. Once we have a reason such as your company we can determine what needs to be done, and do it. The next step is to talk to him I think.
Feb 08
prev sibling next sibling parent reply Walter Bright <newshound2 digitalmars.com> writes:
On 2/8/2021 3:09 AM, Imperatorn wrote:
 Talking with some colleges. They have some questions regarding D:
 
 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)
Sure. It's far better than C is. The biggest impact is simply having array overflow detection. There's a lot more, too, such as protections against uninitialized variables and pointers to expired stack frames.
 2. Are there any plans to make a certified compiler?
Not at the moment.
Feb 09
next sibling parent Imperatorn <johan_forsberg_86 hotmail.com> writes:
On Tuesday, 9 February 2021 at 09:39:50 UTC, Walter Bright wrote:
 On 2/8/2021 3:09 AM, Imperatorn wrote:
 Talking with some colleges. They have some questions regarding 
 D:
 
 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)
Sure. It's far better than C is. The biggest impact is simply having array overflow detection. There's a lot more, too, such as protections against uninitialized variables and pointers to expired stack frames.
 2. Are there any plans to make a certified compiler?
Not at the moment.
Splendid! I'll try to convince my colleagues to try it 🐢
Feb 09
prev sibling parent reply Lasheen <hazem.lasheen yandex.com> writes:
On Tuesday, 9 February 2021 at 09:39:50 UTC, Walter Bright wrote:
 On 2/8/2021 3:09 AM, Imperatorn wrote:
 Talking with some colleges. They have some questions regarding 
 D:
 
 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)
Sure. It's far better than C is. The biggest impact is simply having array overflow detection. There's a lot more, too, such as protections against uninitialized variables and pointers to expired stack frames.
 2. Are there any plans to make a certified compiler?
Not at the moment.
where i can find a detailed tutorial that can help me to understand how to use D in AI apps and specially when mission-critical system is needed.
Mar 16
next sibling parent rikki cattermole <rikki cattermole.co.nz> writes:
On 17/03/2021 4:30 PM, Lasheen wrote:
 where i can find a detailed tutorial that can help me to understand how 
 to use D
 in AI apps and specially when mission-critical system is needed.
There are no tutorials. You may find it is easier to ask the questions you have over on Discord. https://discord.gg/VRg3CeqD
Mar 16
prev sibling parent reply Dukc <ajieskola gmail.com> writes:
On Wednesday, 17 March 2021 at 03:30:17 UTC, Lasheen wrote:
 where i can find a detailed tutorial that can help me to 
 understand how to use D
 in AI apps and specially when mission-critical system is needed.
Not a tutorial, but Walter has written many articles that should hint towards the right mindset: https://digitalmars.com/articles/index.html Mission-critical systems are something I feel it is terribly difficult to find tutorials on. In any language, not just in D. One can learn by watching by following development of critical open-source projects - OpenSSL, Tor or different Unix kernels for example. But other than them, I feel critical systems design is an art that tends be locked in the proprietary world - correct me if I'm wrong.
Mar 17
parent Paulo Pinto <pjmlp progtools.org> writes:
On Wednesday, 17 March 2021 at 21:37:01 UTC, Dukc wrote:
 On Wednesday, 17 March 2021 at 03:30:17 UTC, Lasheen wrote:
 where i can find a detailed tutorial that can help me to 
 understand how to use D
 in AI apps and specially when mission-critical system is 
 needed.
Not a tutorial, but Walter has written many articles that should hint towards the right mindset: https://digitalmars.com/articles/index.html Mission-critical systems are something I feel it is terribly difficult to find tutorials on. In any language, not just in D. One can learn by watching by following development of critical open-source projects - OpenSSL, Tor or different Unix kernels for example. But other than them, I feel critical systems design is an art that tends be locked in the proprietary world - correct me if I'm wrong.
That knowledge is available if one searches for it. https://www.perforce.com/resources/qac/misra-c-cpp https://frama-c.com/ https://www.rapitasystems.com/downloads/validation-cots-ada-compiler-safety-critical-applications https://www.amazon.com/Real-Time-Critical-Systems-Prototype-Integration/dp/1984171992 https://dl.acm.org/doi/10.5555/111797.111813
Mar 18
prev sibling next sibling parent reply IGotD- <nise nise.com> writes:
On Monday, 8 February 2021 at 11:09:49 UTC, Imperatorn wrote:
 Talking with some colleges. They have some questions regarding 
 D:

 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)

 2. Are there any plans to make a certified compiler?
Just to put it into some perspective. I have worked with so called certified C/C++ compilers in the automotive industry. I remember encountered several bugs in those compilers as well they are usually far behind when adopting the new language standards. Compare this to GCC, when was the last time you encountered a bug in that compiler? I can't remember any. The certified compilers which are not better than GCC are usually proprietary and cost money for each user. Here we have a product that is essentially worse than GCC and cost money. What it is really about is a form of corruption. The only positive side is that if you find a bug you can put pressure on the company that provides the compiler but usually that takes several months.
Feb 09
next sibling parent reply Dominikus Dittes Scherkl <dominikus scherkl.de> writes:
On Tuesday, 9 February 2021 at 10:10:05 UTC, IGotD- wrote:
 Just to put it into some perspective. I have worked with so 
 called certified C/C++ compilers in the automotive industry. I 
 remember encountered several bugs in those compilers as well 
 they are usually far behind when adopting the new language 
 standards.
As I said, fixing bugs is NOT required for certification. It is only necessary to document them.
 The certified compilers which are not better than GCC are 
 usually proprietary and cost money for each user.
You can qualify a tool to be used in an ISO compliant build process on your own (in your company). We do this regularly for every little script we use. But to qualify something as complex as a compiler is a huge lot of work. This is why getting an official certificate (from e.g. TÜV) is so expensive that a vendor NEEDS to sell it and can't give it away for free.
 Here we have a product that is essentially worse than GCC and 
 cost money. What it is really about is a form of corruption.
Harsh words. If you don't want to pay for a compiler, qualify it yourself. You'll see it cost you at least the same amount of money (or time).
 Compare this to GCC, when was the last time you encountered a 
 bug in that compiler? I can't remember any.
But this is only because also there the bugs are quiet good documented in bugzilla and so can easily be avoided. Having this documentation will help you a lot in qualifying the compiler yourself.
Feb 09
parent reply Bastiaan Veelo <Bastiaan Veelo.net> writes:
On Tuesday, 9 February 2021 at 11:25:26 UTC, Dominikus Dittes 
Scherkl wrote:
 As I said, fixing bugs is NOT required for certification.
 It is only necessary to document them.
Out of curiosity, what happens next then? I assume the goal is to certify your application. In the process of certifying your application, wouldn't you have to prove that the application does not trigger any of the documented bugs in the certified tools? This could well be harder to do than fixing the bugs in the tools. -- Bastiaan.
Feb 09
parent reply Gregor =?UTF-8?B?TcO8Y2ts?= <gregormueckl gmx.de> writes:
On Tuesday, 9 February 2021 at 12:38:21 UTC, Bastiaan Veelo wrote:
 On Tuesday, 9 February 2021 at 11:25:26 UTC, Dominikus Dittes 
 Scherkl wrote:
 As I said, fixing bugs is NOT required for certification.
 It is only necessary to document them.
Out of curiosity, what happens next then? I assume the goal is to certify your application. In the process of certifying your application, wouldn't you have to prove that the application does not trigger any of the documented bugs in the certified tools? This could well be harder to do than fixing the bugs in the tools. -- Bastiaan.
I'm not aware that any certification requires explicit proof that you avoid those bugs. This is mostly covered indirectly by two things: you need to adhere to the safety manual for the tools you use and you need a pretty rigorous testing regime for your product. The mandated test coverage should be good enough to detect misbehaving code introduced by faulty tools.
Feb 09
parent reply Bastiaan Veelo <Bastiaan Veelo.net> writes:
On Tuesday, 9 February 2021 at 13:22:22 UTC, Gregor Mückl wrote:
 On Tuesday, 9 February 2021 at 12:38:21 UTC, Bastiaan Veelo 
 wrote:
 On Tuesday, 9 February 2021 at 11:25:26 UTC, Dominikus Dittes 
 Scherkl wrote:
 As I said, fixing bugs is NOT required for certification.
 It is only necessary to document them.
Out of curiosity, what happens next then? I assume the goal is to certify your application. In the process of certifying your application, wouldn't you have to prove that the application does not trigger any of the documented bugs in the certified tools? This could well be harder to do than fixing the bugs in the tools. -- Bastiaan.
I'm not aware that any certification requires explicit proof that you avoid those bugs. This is mostly covered indirectly by two things: you need to adhere to the safety manual for the tools you use and you need a pretty rigorous testing regime for your product. The mandated test coverage should be good enough to detect misbehaving code introduced by faulty tools.
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. Your other comment that the certified commercial compiler you used produced higher quality binaries is not necessarily due to the certification, but likely due to available funds. -- Bastiaan.
Feb 09
next sibling parent reply Dominikus Dittes Scherkl <dominikus scherkl.de> writes:
On Tuesday, 9 February 2021 at 14:14:42 UTC, Bastiaan Veelo wrote:
 On Tuesday, 9 February 2021 at 13:22:22 UTC, Gregor Mückl wrote:
 I'm not aware that any certification requires explicit proof 
 that you avoid those bugs.[...]
This makes me wonder what certifying the tool practically brings to the table, apart from doors that can be entered with a certificate only.
Nothing. It's a key to some doors. If you like to enter them, you have to have the key. It's the same as with every certificate. E.g. if you don't have a CE-certificate, you can't sell your product in the EU. If you don't have the ISO-certificate, can't sell your controller software to a major vendor.
 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.
No, the certificate ensures that someone put intense thoughts about safety into the tool and documented what usecases it is good for and what you need to avoid to create a safe product with it. Thoughts that you would have to do yourself if you use a tool without that certificate. 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.
Feb 09
parent reply FeepingCreature <feepingcreature gmail.com> writes:
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.
Feb 09
next sibling parent Paul Backus <snarwin gmail.com> writes:
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.
Feb 09
prev sibling parent reply Gregor =?UTF-8?B?TcO8Y2ts?= <gregormueckl gmx.de> writes:
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.
Feb 09
parent reply Imperatorn <johan_forsberg_86 hotmail.com> writes:
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.
Feb 09
parent reply Max Haughton <maxhaton gmail.com> writes:
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.
Feb 09
next sibling parent reply lagfra <me fragal.eu> writes:
On Tuesday, 9 February 2021 at 21:23:35 UTC, Max Haughton wrote:
 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 big 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).
Feb 09
next sibling parent Imperatorn <johan_forsberg_86 hotmail.com> writes:
On Tuesday, 9 February 2021 at 23:59:32 UTC, lagfra wrote:
 On Tuesday, 9 February 2021 at 21:23:35 UTC, Max Haughton wrote:
 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 big 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).
That sounds like a cool project
Feb 09
prev sibling parent reply welkam <wwwelkam gmail.com> writes:
A talk about model checker Alloy. Its an introductory talk to 
people with not prior knowledge
"Finding bugs without running or even looking at code" by Jay 
Parlar
https://www.youtube.com/watch?v=FvNRlE4E9QQ
Feb 10
next sibling parent Imperatorn <johan_forsberg_86 hotmail.com> writes:
On Wednesday, 10 February 2021 at 17:01:19 UTC, welkam wrote:
 A talk about model checker Alloy. Its an introductory talk to 
 people with not prior knowledge
 "Finding bugs without running or even looking at code" by Jay 
 Parlar
 https://www.youtube.com/watch?v=FvNRlE4E9QQ
Nice. I've used UPPAAL in the past with some success. https://en.wikipedia.org/wiki/Uppaal_Model_Checker
Feb 10
prev sibling parent lagfra <me fragal.eu> writes:
On Wednesday, 10 February 2021 at 17:01:19 UTC, welkam wrote:
 A talk about model checker Alloy. Its an introductory talk to 
 people with not prior knowledge
 "Finding bugs without running or even looking at code" by Jay 
 Parlar
 https://www.youtube.com/watch?v=FvNRlE4E9QQ
That's actually an interesting SAT-based mc, though I never had the occasion of trying it out. I like the fact that it is currenly under development, in my experience model checkers are "old" (most theoretical breaktroughs have been published in the 1980s and still struggle to get a proper implementation). Plus, research is mostly supported by universities, which implies that development pace is often quite slow. A model checker that has been widely adopted is NuSMV (https://nusmv.fbk.eu/), there's a very nice survey by K. Rozier from NASA Ames research center describing an example application of it https://www.researchgate.net/publication/222531608_Linear_Temporal_Logic_Symbolic_Model_Checking
Feb 11
prev sibling parent lagfra <me fragal.eu> writes:
 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 Bchi 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).
Feb 09
prev sibling parent Dukc <ajieskola gmail.com> writes:
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.
Feb 09
prev sibling next sibling parent reply Gregor =?UTF-8?B?TcO8Y2ts?= <gregormueckl gmx.de> writes:
On Tuesday, 9 February 2021 at 10:10:05 UTC, IGotD- wrote:
 On Monday, 8 February 2021 at 11:09:49 UTC, Imperatorn wrote:
 Talking with some colleges. They have some questions regarding 
 D:

 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)

 2. Are there any plans to make a certified compiler?
Just to put it into some perspective. I have worked with so called certified C/C++ compilers in the automotive industry. I remember encountered several bugs in those compilers as well they are usually far behind when adopting the new language standards. Compare this to GCC, when was the last time you encountered a bug in that compiler? I can't remember any. The certified compilers which are not better than GCC are usually proprietary and cost money for each user. Here we have a product that is essentially worse than GCC and cost money. What it is really about is a form of corruption. The only positive side is that if you find a bug you can put pressure on the company that provides the compiler but usually that takes several months.
There is a fair amount of hate in this post that I can't agree with. 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!).
Feb 09
next sibling parent reply Max Haughton <maxhaton gmail.com> writes:
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:
 [...]
There is a fair amount of hate in this post that I can't agree with. 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!).
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.
Feb 09
parent reply Gregor =?UTF-8?B?TcO8Y2ts?= <gregormueckl gmx.de> writes:
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.
Feb 09
parent Max Haughton <maxhaton gmail.com> writes:
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.
Feb 09
prev sibling parent reply IGotD- <nise nise.com> writes:
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.
 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. 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.
Feb 09
parent Gregor =?UTF-8?B?TcO8Y2ts?= <gregormueckl gmx.de> writes:
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.
Feb 09
prev sibling parent Elronnd <elronnd elronnd.net> writes:
On Tuesday, 9 February 2021 at 10:10:05 UTC, IGotD- wrote:
 On Monday, 8 February 2021 at 11:09:49 UTC, Imperatorn wrote:
 2. Are there any plans to make a certified compiler?
Just to put it into some perspective. I have worked with so called certified C/C++ compilers in the automotive industry. I remember encountered several bugs in those compilers as well they are usually far behind when adopting the new language standards. Compare this to GCC, when was the last time you encountered a bug in that compiler? I can't remember any.
You may mean different things by ‘certified’. In some contexts, the term refers to a formally verified compiler, like, cakeml or compcert, which has been mathematically proven not to have any compilation bugs. I would be inclined to trust such a compiler.
Mar 17
prev sibling next sibling parent Dukc <ajieskola gmail.com> writes:
On Monday, 8 February 2021 at 11:09:49 UTC, Imperatorn wrote:
 Talking with some colleges. They have some questions regarding 
 D:

 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)

 2. Are there any plans to make a certified compiler?
One would presumably certify some version of the D compiler, let's say 2.095.0, and would have to use that for years to come. Perhaps patch version updates would be okay (2.095.1), but no updating to 2.096.0 without re-certifying. My experience is that Dub projects tend to stop compiling after perhaps 5 or so versions on average. That means that if D libraries are used, one would have to start maintaining them themselves after some time. This isn't a showstopper, since such maintenance is not a major burden assuming the library is already stable and no new features are desired. But it means that if someone releases a D library 3 years after the certification, the new library probably can't be used without considerable porting effort. One would be fairly much stuck with what exists at certification time.
Feb 09
prev sibling parent reply Arun <aruncxy gmail.com> writes:
On Monday, 8 February 2021 at 11:09:49 UTC, Imperatorn wrote:
 Talking with some colleges. They have some questions regarding 
 D:

 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)

 2. Are there any plans to make a certified compiler?
If C is ready for safety critical applications, then DasBetterC is beyond ready. HN discussions on the related topic here: https://news.ycombinator.com/item?id=23005297
Feb 17
parent Imperatorn <johan_forsberg_86 hotmail.com> writes:
On Wednesday, 17 February 2021 at 17:36:41 UTC, Arun wrote:
 On Monday, 8 February 2021 at 11:09:49 UTC, Imperatorn wrote:
 Talking with some colleges. They have some questions regarding 
 D:

 1. Is D ready for prime time á la safety critical applications?
 (I guess they mean GDC on ARM for example)

 2. Are there any plans to make a certified compiler?
If C is ready for safety critical applications, then DasBetterC is beyond ready. HN discussions on the related topic here: https://news.ycombinator.com/item?id=23005297
Nice, i guess they were more thinking of GDC, idk. I can ask again. everyone: Btw, where can I download gcc with D support and what version of D is it? I've heard rumors it will be updated "soon", is that correct? 🤔 Thanks!
Feb 19