[HN Gopher] The Power of 10: Rules for Developing Safety-Critica...
___________________________________________________________________
The Power of 10: Rules for Developing Safety-Critical Code [pdf]
Author : CharlesW
Score : 51 points
Date : 2023-06-28 13:18 UTC (9 hours ago)
(HTM) web link (web.eecs.umich.edu)
(TXT) w3m dump (web.eecs.umich.edu)
| fallingmeat wrote:
| Fun fact: the author of these rules (Gerard Holzmann) is also the
| inventor of the Spin model checker (spinroot.com)!
| AlotOfReading wrote:
| These 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.
| dwohnitmok wrote:
| > 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.
|
| The article somewhat alludes to this, although they don't use
| the notion of progress that you use, which is extremely
| important.
|
| > This rule does not, of course, apply to iterations that are
| meant to be nonterminating--for example, in a process
| scheduler. In those special cases, the reverse rule is applied:
| It should be possible for a checking tool to prove statically
| that the iteration cannot terminate.
|
| As a further searchable term, people can look up "total
| functions." Total functions must either terminate (loop ends)
| or be productive (always make forward progress). That as many
| functions as possible should be total is a pretty good rule of
| thumb in any codebase.
| TeMPOraL wrote:
| >> _In those special cases, the reverse rule is applied: It
| should be possible for a checking tool to prove statically
| that the iteration cannot terminate._
|
| This part made me pause for a moment, but then it clicked,
| and I'm remembering the rare and unusual experience of facing
| a process that escaped a loop that was supposed to go on
| indefinitely. A software equivalent of transmission belt
| slipping off. Most frequently seen in video games, where it's
| mostly harmless - but imagining a scheduler in an embedded
| system quitting on me like this fills me with dread to
| irrational extent.
|
| > _As a further searchable term, people can look up "total
| functions." Total functions must either terminate (loop ends)
| or be productive (always make forward progress)._
|
| That's a new one to me. I'm not deep into more advanced
| flavors of functional programming, but I thought total
| functions are defined as terminating in finite time for all
| inputs. I suppose it depends on whether you consider infinite
| loop a successful termination in infinity or not, but
| personally I wouldn't, at least not when it's clear the
| function is plain running in circles (as opposed to
| asymptotically approaching a value).
| AlotOfReading wrote:
| Yep, it's a bit terrifying to contemplate. If you're ever
| unfortunate enough to do safety critical systems, you'll
| have to remember that you have to protect against this not
| only at the software level with formal methods, but also at
| the hardware level to ensure that e.g. a bit flip in the
| CPU registers or the instruction sequence as it travels
| from memory also doesn't violate your safety model.
| eschneider wrote:
| The 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 wrote:
| They'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.
| [deleted]
| JohnFen wrote:
| > You can do this even with libc malloc in a standards
| compliant way
|
| This is what I do in nontrivial embedded projects. It makes
| things easier and less error-prone to replace
| malloc()/free()/etc implementations directly with ones that
| behave as needed. And then you don't have the standard
| implementations sitting around waiting for a new dev to
| accidentally use them.
| AnimalMuppet wrote:
| If you're the programmer who has to provably meet hard real
| time constraints, the difference matters quite a bit.
| LorenPechtel wrote:
| I 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 wrote:
| Stack 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.
| MatthiasPortzel wrote:
| By disallowing recursion and requiring loops to have a fixed
| upper bound, you've defined a subset of C that is less than
| Turning complete.
| adrianN wrote:
| How 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 wrote:
| > 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.
| zokier wrote:
| That is a good thing, right? Turing completeness is rarely a
| desirable property
| jcranmer wrote:
| If 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 wrote:
| I 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.
| adrianN wrote:
| You can easily have bounded loops and superexponential
| runtime.
| tgv wrote:
| Without dynamic memory allocation? I think you'd need at
| least O(n) memory to store enough state to go
| exponential. But it's some time I did complexity theory;
| I could be wrong.
| l33t233372 wrote:
| When everything is finite and memory is always limited,
| what are you meaningfully saying about the possible
| behaviors of software here?
| c_crank wrote:
| Bounding the complexity is desirable for a system that
| should never fail due to software errors.
| [deleted]
| AnimalMuppet wrote:
| Yes. And by doing so (and by removing recursion), you are also
| making the Halting Problem decidable.
| [deleted]
| Farmadupe wrote:
| just 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 wrote:
| > 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.
| munch117 wrote:
| Do that and you are just creating targets for the next
| security auditor that you need any sort of certification or
| approval from.
|
| In the end you'll choose the path of least resistance, which
| is to slavishly obey every rule on the checklist. It's not
| that people don't want to tailor the rules. They try at
| first, and then it gets beaten out of them.
|
| Frustrating indeed.
| nunuvit wrote:
| It's doable sometimes when there's a tailoring framework.
| Here's a publicly available example [1]. Though I admit
| that it's usually easier to do in the US than in the
| European Union, so your experience may vary.
|
| [1]
| https://www.nasa.gov/seh/3-11_tailoring_and_customization
___________________________________________________________________
(page generated 2023-06-28 23:02 UTC)