(:warning: 2013) Toyota Unintended Acceleration and the Big Bowl of “Spaghetti” Code



  • @dse said:

    Embedded system, and no Rust yet.

    What about ADA?
    @antiquarian


  • BINNED

    The only language I have seen come close to be a worthy practical contender is Rust. The problem is, it will takes decades to know for sure. I will not use it in my current project because I do not want to be looked at as that guy.


  • BINNED

    @aliceif said:

    What about ADA?@antiquarian

    If you use Ada for your project, I have good news and bad news. The bad news is you run a significant risk of RSI, as Ada code tends to make COBOL seem terse. The good news is that you and others will be easily able to read the code once done.



  • @dse said:

    to harden against buffer overflow, you will need a more robust method, maybe run the application on 2 separate isolated units at once and back off if they disagree (randomize memory access and use cookies so buffer overflow will result in that event). It is risky to handle an exception without a full reset, the only correct way is to increase redundancy and refresh/resync everything every once in while.

    How much good will that do when every redundant copy gets the same data, has the same bug, hits the same edge case, and fails simultaneously?


  • BINNED

    I have never done that, it is an extreme measure, I remember someone explaining it to me about this paradigm in an electric plant. Supposedly randomization of memory layout, and adding cookies to stack should produce different outcomes.
    The thing is, the redundant system may never be used at all in its lifetime, which is the expected outcome. But even if a gamma radiation flips many bits to fool FEC, you want to have a robust system.


  • Java Dev

    Testing can only prove the presence of bugs, not their absence.


  • BINNED

    It is hard to prove the absence of anything. You can just decrease the likelihood of bugs by testing more and with a more diverse set of tools and methods.



  • I suspect you're missing the point. A test shows the absence or presence of one bug. Formal methods can prove the absence of whole classes of bugs.


  • BINNED

    I am not. Formal methods are not like mathematical proofs, if you look at some big ones you will know what I mean. They are huge, even bigger than original code! And that is when you do not bring in multiple threads, and processors and such. Those that are short, have lots of simplifications, and that is where the catch is.
    If you have the budget (mostly time, but also cash because full proofs are expensive and huge) go for it, otherwise do the best that you can. Static analysis, many compilers, many code reviewers, ... At the end if it is a nuclear plant, or an Apollo mission, run redundant systems to make it robust against gamma rays too.

    Formal proofs are just another test.



  • @anotherusername said:

    How much good will that do when every redundant copy gets the same data, has the same bug, hits the same edge case, and fails simultaneously?

    @dse said:

    Supposedly randomization of memory layout, and adding cookies to stack should produce different outcomes.

    The really serious systems go even one step further. They have pair of dissimilar boards (different architectures) running independently implemented copies of the same logic that cross-check each other, plus one or two more copies of the same pair for fail-over. And for the most critical part, two such systems that implement the same functionality using separate machinery.



  • @dse said:

    It is hard to prove the absence of anything.

    ...but much less hard to prove the absence of the possibility of something using formal rules.

    To give one simple example that should be familiar to everyone here, if I declare a private member in a class and then don't use it in the code for that class, any compiler worth its salt can tell you that it's impossible for this to ever be used anywhere, (assuming you don't have things that can break the rules, such as reflection that can reach into private members,) which thus effectively "proves the absence of" something: nothing is using this member. The compiler then reports it as a warning.


  • Discourse touched me in a no-no place

    @Mason_Wheeler said:

    The compiler then reports it as a warning.

    Or it just excludes the code in that case. That's more usually done for things like unreachable code inside functions, where compilers have much more total understanding of the real semantics of what's going on, but it can be done elsewhere too (JIT engines do this sort of thing, since they've access to the total definition of the program and not just of the compilation unit).


  • BINNED

    @Mason_Wheeler said:

    ...but much less hard to prove the absence of the possibility of something using formal rules.

    Not exactly:

    @Mason_Wheeler said:

    assuming you don't have things that can break the rules, such as reflection that can reach into private members,

    assuming single thread, assuming no compiler bugs, assuming no mistake in the formal proof, ... is not a practical assumption.

    @Mason_Wheeler said:

    thus effectively "proves the absence of" something: nothing is using this member.

    No it just gives us more guarantees under some assumptions, which is great. However, a real proof means you could bet your life on it.


  • Discourse touched me in a no-no place

    @dse said:

    assuming single thread, assuming no compiler bugs, assuming no mistake in the formal proof, ... is not a practical assumption.

    Still works better than testing! Testing can at best show that you've not got the errors you've thought of, and often not even that. Threaded code is notorious for being impractical to test thoroughly.

    Proof systems are usually coded so that they're so simple they're obviously not wrong (as opposed to the usual standard for software: not obviously wrong). You also usually don't use them for a full correctness proof, typically because you probably don't have a formal description of everything the system is supposed to do beyond the program being analysed, but some critical properties are much easier to demonstrate. Little things like finite-memory-use, no-buffer-overflows, always-live, that sort of thing. Yes, some of these are tricky in the general case, which is why you use conservative assumptions: if you can't prove the property within some reasonable bound of effort, you've got a problem (and undecidable cases are just as poisonous as definitely-wrong cases).

    Proof systems aren't panaceas, and are quite difficult to use well, but they help a lot.

    @dse said:

    They are huge, even bigger than original code!

    Oh, the horror! 😱


  • BINNED

    @dkf said:

    Testing can at best show that you've not got the errors you've thought of, and often not even that.

    Not fuzzing. Fuzz testers find errors with very low occurrence rate.

    @dkf said:

    Proof systems aren't panaceas, and are quite difficult to use well, but they help a lot.

    No argument here, of course they help a lot. I would love if I could get them for free, but I guess not ..

    @dkf said:

    Still works better than testing!

    What is the point of proving a system under some simplified assumptions when those assumptions (e.g. threads) are the major point of bugs anyways? Like you prove a coding algorithm is all fine, but the bug is from another part of the SSL stack not related to bounds check of the algorithm? Testing will find those bugs, because it hits them in reality.

    @dse said:

    They are huge, even bigger than original code!
    @dkf said:
    Oh, the horror!

    👦 Ok can you prove these 100 lines of code are correct?
    👴 sure, here we go these 1000 lines of mathematical proof will do, I hope I did not mess up the signs because my eyes do not see well.
    👦 signal to noise is decreased, I have to read 10 times more of math jargon


  • BINNED

    Have you used any of the software here:

    Astree looks interesting.

    Which one do you suggest?
    Proprietary or open source, do you have other suggestion?


  • Discourse touched me in a no-no place

    @dse said:

    Which one do you suggest?

    I've used FindBugs, but it's a tool for Java IIRC. Wrote my own (a long time ago) but the language we were analysing was a bit unusual, as it was aimed at hardware synthesis instead of software systems. Hardware languages are a bit different to working with C (e.g., you go for a formally-finite type system in anything you are ever going to synthesise, have no memory allocation at all — memory is something you describe — and you've vast amounts of parallelism) and that has a whole load of downstream implications.

    Aside from that, most of the approaches used in the field back when I was working in Formal Methods were actually based on being correct by construction, using provably correct methods to generate correct code from specifications. They were mostly aimed at safety critical applications like railway signalling. I've no personal experience with them, but my boss at the time was quite insistent that ad hoc after-the-fact proofs were a lot more difficult to work with.


Log in to reply