3 ms·

> The rule about recursion is likely also to ensure a statically known bound on needed stack space It's definitely that. Static stack size analysis in the emb

by ajross 2y ago

> The rule about recursion is likely also to ensure a statically known bound on needed stack space It's definitely that. Static stack size analysis in the embedded world is a long-standing paradigm and recursion and function pointer indirection defeat that. If the point of rule was that NASA was arguing that recursive constructions are always harder to reason about than iterative ones, then obviously NASA is wrong.

AnimalMuppet 2y ago
If hard realtime and stack space are part of your constraints, then recursive constructions are in fact always harder to reason about.
- ajross 2y ago
  To clarify: it's not stack "space" that's at issue. It's the requirement that the lack of stack overflow at runtime be formally verified. If functions exist in a static call tree[1] you can do this with a little disassembly wizardry and a few hundred lines of python. If you allow them to call themselves recursively, or even to indirect through a function pointer, it becomes undecidable. [1] There are some other related rules like "no alloca()".
  - rcxdude 2y ago
    Function pointers are possible to deal with, with varying levels of automation. You can detect when pointers to functions are taken, and tie them to call sides with type information or some manual work (I have a static analysis tool which allows function pointers for callbacks by linking functions passed into one function to the list of possible destinations for a given callsite). Recursion is harder but it's still possible in principle to prove a bound in a lot of cases, given a proof framework. Not something I'd encourage, though.
shakna 2y ago
Just to quote the original rationale: > Rationale: Simpler control flow translates into stronger capabilities for verification and often results in improved code clarity. The banishment of recursion is perhaps the biggest surprise here. Without recursion, though, we are guaranteed to have an acyclic function call graph, which can be exploited by code analyzers, and can directly help to prove that all executions that should be bounded are in fact bounded. (Note that this rule does not require that all functions have a single point of return – although this often also simplifies control flow. There are enough cases, though, where an early error return is the simpler solution.) [0] [0] https://spinroot.com/gerard/pdf/P10.pdf https://spinroot.com/gerard/pdf/P10.pdf

by ajross 2y ago

AnimalMuppet 2y ago

If hard realtime and stack space are part of your constraints, then recursive constructions are in fact always harder to reason about.

ajross 2y ago
To clarify: it's not stack "space" that's at issue. It's the requirement that the lack of stack overflow at runtime be formally verified. If functions exist in a static call tree[1] you can do this with a little disassembly wizardry and a few hundred lines of python. If you allow them to call themselves recursively, or even to indirect through a function pointer, it becomes undecidable. [1] There are some other related rules like "no alloca()".
- rcxdude 2y ago
  Function pointers are possible to deal with, with varying levels of automation. You can detect when pointers to functions are taken, and tie them to call sides with type information or some manual work (I have a static analysis tool which allows function pointers for callbacks by linking functions passed into one function to the list of possible destinations for a given callsite). Recursion is harder but it's still possible in principle to prove a bound in a lot of cases, given a proof framework. Not something I'd encourage, though.

shakna 2y ago

Just to quote the original rationale: > Rationale: Simpler control flow translates into stronger capabilities for verification and often results in improved code clarity. The banishment of recursion is perhaps the biggest surprise here. Without recursion, though, we are guaranteed to have an acyclic function call graph, which can be exploited by code analyzers, and can directly help to prove that all executions that should be bounded are in fact bounded. (Note that this rule does not require that all functions have a single point of return – although this often also simplifies control flow. There are enough cases, though, where an early error return is the simpler solution.) [0] [0] https://spinroot.com/gerard/pdf/P10.pdf https://spinroot.com/gerard/pdf/P10.pdf