8 ms·
The Power of 10: Rules for Developing Safety-Critical Code [pdf]
- MatthiasPortzel 3y agoBy disallowing recursion and requiring loops to have a fixed upper bound, you’ve defined a subset of C that is less than Turning complete.
- jcranmer 3y agoIf you're being that pedantic, C itself is not Turing-complete in the first place: pointers have finite size, which means that C can address only a bounded amount of memory, so it is a finite state machine (just with an extremely large number of states).
- tgv 3y agoI don't think it's about that. Technically, everything is finite. But placing limits on the loops and restricting memory allocation bounds the complexity. It probably limits everything to P-time.
- l33t233372 3y agoWhen everything is finite and memory is always limited, what are you meaningfully saying about the possible behaviors of software here?
- c_crank 3y agoBounding the complexity is desirable for a system that should never fail due to software errors.
- adrianN 3y agoYou can easily have bounded loops and superexponential runtime.
- deleted 3y ago[deleted]
- AnimalMuppet 3y agoYes. And by doing so (and by removing recursion), you are also making the Halting Problem decidable.
- hedora 3y agoRule 5 prohibits programs that average less than two undecidable branches per function.
- adrianN 3y agoHow many problems in safety critical systems need Turing completeness and how many are fine with something weaker eg primitive recursion? My intuition is that most things are fine without full Turing completeness (as far as you can even apply terms about computability to systems with complex IO behavior)
- marcosdumay 3y ago> How many problems in safety critical systems need Turing completeness Probably all, like the ones outside of critical systems. But if you concentrate the complex behavior in a single layer, you will probably get a very thin layer, that you can call an OS or something like that, verify it very well, and have almost all the code follow a non-complete idiom.
- adrianN 3y agoI have worked on a safety critical system and can't recall a part that needed Turing completeness.
- marcosdumay 3y agoWhat starts your safety critical code?
- adrianN 3y agoSome part of the hardware starts executing the code at some fixed address when the system is powered on. I don't know the details, I only do software.
- zokier 3y agoThat is a good thing, right? Turing completeness is rarely a desirable property
- AlotOfReading 3y agoThese are somewhat dated rules, and generally too restrictive for modern safety critical development. For one thing, unbounded loops are situationally fine. The key distinction is that the program has to make forward progress regardless, which is not always the same thing as escaping the loop. Pool allocators have also become very common, so the complete prohibition on "dynamic allocation" is a lot more flexible now. Many of the other rules broadly hold up though. You still want to avoid things like pointers because static analyzers are terrible at proving through them. This typically means LUTs are wrapped in the equivalent of an unsafe block though. Not ideal, and hopefully better tooling will eventually exist for these sorts of things.
- eschneider 3y agoThe problem with dynamic allocation (aside from the problem that it can fail) is that calls to malloc don't complete in a predicable time, so it's pretty much verboten in hard realtime apps. Pool allocators can (though not always are) written to return in a bounded time, so if it's created at startup, yeah, not really dynamic allocation.
- AlotOfReading 3y agoThey're not meaningfully different from the perspective of the programmer. You call a malloc-like function and get some memory back. The total dynamic memory use of the application is simply capped. You can do this even with libc malloc in a standards compliant way (e.g. Broadcom used to ship a malloc implemented as a series of pool allocators over statically initialized arenas), it's just uncommon.
- AnimalMuppet 3y agoIf you're the programmer who has to provably meet hard real time constraints, the difference matters quite a bit.
- deleted 3y ago[deleted]
- 3y ago
- deleted 3y ago[deleted]
- Farmadupe 3y agojust a few drive-by comments: First and most important, the title claims these are safety-critical rules, but the conclusion says that they are only being used on mission-critical projects. I get the feeling that there might have been some late-change copyediting done here, as the content is far too generalizing to be taken seriously in any specific safety critical context, and hopefully the author would have known that. * Agree that many safety-critical coding standards are a grab-bag of sometimes dubiously-valuable rules. * Agree with the implication that stylistic guidelines are almost totally worthless, and may distract reviews from their core task of finding functional errors. * The document states that manual review of large cases may be infeasible, but I have never worked on a project that didn't mandate it. Drudgery goes hand-in-hand with safety-critical, and mindnumbing close review is an accepted element of this. * Agree that less rules is good, but the author doesn't justify why 10 rules is the best. Unfortunately this is a field where correctness trumps easiness or simplicity, and any class of error with unacceptable risk to life/limb must be prevented. Thus any ruleset cannot justify itself simply because it is small. * In fact, there are many wordings in this document that are generally-unacceptable because they are admitting incompleteness in the general case (and therefore unsuitability for any safety-critical purpose), such as "Although such a small set of rules cannot be all-encompassing" or "In return, it should be possible to demonstrate more convincingly that critical software will work as intended" commentaries on specific rules: * rule 4: "No function should be longer than what can be printed on a single sheet of paper". In my experience, readability is not always improved by limiting function length. The main goal of safety-critical be correct (and hopefully be obviously so). Sometimes splitting up code is harmful to this. (also this is actually a stylistic rule of the kind rejected in the 2nd paragraph of the document.) * rule 5: In the safety-critical domain, defensive checks and "assertions" are usually considered at low-level-design. It's generally unacceptable for a coder to "just" insert defensive behaviours into the implementation, because all such behaviours must be analyzed for correctness. I don't disagree with the idea behind this rules, but a coding standard is the wrong place for it.
- nunuvit 3y ago> Agree that many safety-critical coding standards are a grab-bag of sometimes dubiously-valuable rules. What frustrates me is that most standards are self-aware of this and explicitly allow you to tailor them, but hardly anyone does that to a meaningful extent.
- fallingmeat 3y agoFun fact: the author of these rules (Gerard Holzmann) is also the inventor of the Spin model checker (spinroot.com)!
- LorenPechtel 3y agoI think they're being too restrictive on recursion. They're excluding it based on not being able to prove it will terminate--but you can do that with a time-to-die counter.
- oleganza 3y agoStack is a dynamic memory of sorts and some languages (Rust) heavily optimize towards keeping things on stack so that your data types could turn out to be quite big. It is hard to determine the max value for time-to-die counter if your stack footprint is hard to estimate due to nested structs/enums/unions/generics/optimizations.
- hedora 3y agoI wish there was a “this is tail recursive; if you cannot turn it into a loop, fail to compile” compiler annotation for C++/rust.
- Svetlitski 3y agoClang provides the "musttail" attribute for C and C++: https://clang.llvm.org/docs/AttributeReference.html#musttail https://clang.llvm.org/docs/AttributeReference.html#musttail
- Zamiel_Snawley 3y agoThere is something ironic about there being an obvious typo in the subtitle(domponents instead of components). Regardless, I think these are generally good guidelines, but I'd not call the rules. Sometimes you really need the C preprocessor. For example, for compile-time assertions in C99.
- isityouyesitsme 3y agoEver write against AUTOSAR? Vendors will implement full state machines in the preprocessor. Generated code will include the same header 2 or 3 times, because each time through, the state machine has changed and different code is exposed. I am not joking.
- Shawnj2 3y agoThey are the rules for JPL, where they are sending shit to other planets and have 1 incredibly expensive shot to get the software right on the first try. The software cannot have an unrecoverable error condition and the safety critical portions of the code like that used for landing the spacecraft need to work on the first shot no matter what goes wrong. Even other spacecraft don’t need to have as strict rules but this is a different playing field
- isityouyesitsme 3y agoPerhaps not everyone knows what AUTOSAR is. https://en.m.wikipedia.org/wiki/AUTOSAR https://en.m.wikipedia.org/wiki/AUTOSAR. Think: automotive brake controllers, that type of shit. It is safety critical. My point isn't that the rules apply universally, it's that something found to be a good practice in a safety critical industry is flagrantly discarded in another, without good reason. Literal state machines in the preprocessor. Metaprogramming in C. But because it is generated code, it is "ok."
- RealityVoid 3y agoThe automotive industry is weird like that. They started doing things a way, got stuck in a groove and now if you push back against it they look at you like you killed their dog. I should really find a different field, for my mental well being.
- hedora 3y agoI love rule 5. Each function should have on average, at least two assertions that cannot be checked statically, and the calling code must try to recover from the failure. So much for writing code that doesn’t suffer from the halting problem, or that has high branch coverage!
- lincpa 3y ago[dead]
- jpc0 3y agoMore modern take of this https://yurichev.com/mirrors/C/JPL_Coding_Standard_C.pdf https://yurichev.com/mirrors/C/JPL_Coding_Standard_C.pdf