4 ms·

F’: Flight Software and Embedded Systems Framework

189 points by zeristor 6y ago

zeristor 6y ago
How long before Rust will be mature enough for the task?
- foobar33333 6y ago
  Probably once people have decades of experience with it and know every single trap or quirk perfectly. Rust almost certainly could do the job now but stakes are so high no one would take that risk when its proven that C can do it and with enough auditing and conservatism, it can be done pretty safely.
  - bri3d 6y ago
    I don't think the barrier is _people_ knowing the traps, as people are always fallible and any system relying on them knowing the "traps and quirks" is fundamentally pointless. I do think the barrier is, rather, _tools_ knowing the traps. Most systems in this class, FPrime included, rely extensively on code generation and model-to-code auditing, which, while usually not formally proven (unfortunately), is battle-tested. Now, these sorts of systems should actually be _easier_, in the long-term, to build in Rust, since the type system can enable a class of proof which simply was not historically possible, but for the time being, the tooling doesn't exist yet.
  - cat199 6y ago
    > Probably once people have decades of experience with it and know every single trap or quirk perfectly. people were writing mission-critical C++ when C++ was new / only a few years old; with this in mind, rust is probably good to go with sufficient application/system testing that said, since C++ & associated tooling exists, there is more of an opportunity cost since, in the context of today, there are more alternatives that could be considered
    - carlmr 6y ago
      I think this is spot on. The tooling is there for C++, but human mistakes are much more prevalent, and the discipline to apply the tooling is not a given. There should be an industry push for certified Rust tooling, it would save the aerospace and auto industry billions. Or you could use the unsexy but also very good ADA 2012, which is already certified.
      - pjmlp 6y ago
        This is one of the reasons why NVidia went with Ada/SPARK for their security critical firmware project.
        sterlind 6y ago
        iirc, SPARK has proof capabilities that outstrip the memory-safety guarantees of Rust. basically design by contract, where you can check loop invariants and statically verify complex preconditions and postconditions. I suppose the workflow would be to flesh out and check the abstract design in something like Coq or (maybe) TLAPS, generate a refinement into the SPARK code contracts, then implement the functions. Since the toolchains are verified there shouldn't be much surface area for bugs left.
        pjmlp 6y ago
        Yep, here some very good books about it, specially relevant given the main subject. "Building High Integrity Applications with SPARK" https://www.amazon.com/Building-High-Integrity-Applications-SPARK/dp/1107656842 https://www.amazon.com/Building-High-Integrity-Applications-... "Building Parallel, Embedded, and Real-Time Applications with Ada" https://www.amazon.com/Building-Parallel-Embedded-Real-Time-Applications/dp/0521197163 https://www.amazon.com/Building-Parallel-Embedded-Real-Time-... "Embedded Software Development for Safety-Critical Systems" https://www.amazon.com/Embedded-Software-Development-Safety-Critical-Systems/dp/0367338858 https://www.amazon.com/Embedded-Software-Development-Safety-...
  - gregors 6y ago
    Here's a pretty interesting read regarding Lisp at JPL. http://www.flownet.com/gat/jpl-lisp.html http://www.flownet.com/gat/jpl-lisp.html I think the "safety" of "familiarity" vs pushing the envelope of what we can do technically are different things. We used to build brand new computers and operating systems from scratch specifically for these types of things. The risks are indeed high for managerial staff. I worked at a large quasi-government place. "you won't ever get fired for using Microsoft, Oracle, etc" was a tagline we heard often in non-critical systems, so I imagine there would need to be some major technical reason to switch. Now drones on the other hand... https://en.wikipedia.org/wiki/Iran%E2%80%93U.S._RQ-170_incident https://en.wikipedia.org/wiki/Iran%E2%80%93U.S._RQ-170_incid...
- bobthebuilders 6y ago
  Never. Rust will never be good enough to replace C.
  - kamranjon 6y ago
    this is c++
- mhh__ 6y ago
  Keep in mind that for this kind of project you want static analysis and formal verification (model checking for example) rather than just day-to-day safety features. I.e. the Rust this, Rust that spam is a little naive to the task at hand, even though it would be a step up from C
  - pensono 6y ago
    Is C++ complex enough that it is difficult to model, and therefore hard to apply in formal methods?
    - rurban 6y ago
      The problem is not the language, the problem are unbounded loops. Like linked lists vs vectors. Termination is theoretically impossible to prove, but practically you can handle it. Parts of the STL were formally verified. cprover (with satabs and cbmc) can handle C, C++ or Java. F' uses autogenerated classes, which helps a lot avoiding mistakes.
      - gugagore 6y ago
        Because the problem is unsolvable, there is a wide variety of "you can handle it"-ness that a language can have...
  - OnlyOneCannolo 6y ago
    NASA even has their own sound static analyzer for memory safety. If you use something like that, and depending on the context, there isn't even necessarily a memory safety advantage to using Rust over C or C++. https://github.com/NASA-SW-VnV/ikos https://github.com/NASA-SW-VnV/ikos
  - gregors 6y ago
    It was my understanding that when formal methods were used, they were used on very small subsets of code and not used in general. I do wonder about TLA+ and would love to hear more about how they use such tools. I know I've seen an older document that specifically prohibited use of malloc that the risk was too great. Is that still the case?
- otabdeveloper4 6y ago
  Use-after-free is a) probably the least important class of bugs for this sort of thing b) adequately solved with the existing C++ language features anyways. So what would be the point of rewriting in Rust? (Assume the people writing it aready have the C++ knowledge and tooling ready.)
  - pjmlp 6y ago
    c) assuming they have ISO C++ minutiae level of language understanding, https://herbsutter.com/2020/02/17/move-simply/ https://herbsutter.com/2020/02/17/move-simply/
  - hctaw 6y ago
    What about iterator invalidation or multiple mutable aliasing in concurrent code
    - otabdeveloper4 6y ago
      Iterator invalidation is a kind of use-after-free. Mutating aliased objects is, of course, usually the desired outcome and not a bug. It becomes a bug when your program's concurrency logic is not thought through, and there are no easy solutions here.
Linked_Liszt 6y ago
It's cool that this framework is getting some attention. In our college senior design project, we built a small prototype using this framework during a trade study. We got a few small UI fixes pushed upstream to the main repo. Our team even got to meet up with the maintainers for a few days as they were showing off the framework. It was one of the most interesting and unique software projects I've worked on. The framework itself is portable allowing for code sharing across multiple missions and hardware setups. According to the devs, in the space industry, software is so mission specific and intertwined that it's rarely reused. FPrime's "modules" create hard barriers between sections of the program, something I have mixed feelings about. Finally the "module" system allows for a very easy to use concurrency model, which I think is one of the strengths of the framework. (Though, take these words with a grain of salt as I was and still am wildly underqualified in the domain of embedded systems)
numpad0 6y ago
So it’s ROS replacement that doesn’t suck?
- jvanderbot 6y ago
  Half true!
  - 0xFFC 6y ago
    Can you elaborate more on this?
    - nexthash 6y ago
      ROS stands for Robotic Operating System. It is a framework of different tools such as an abstraction layer, libraries, and a package manager that makes it easier to program/interface with different robotic systems/components. It basically simplifies a lot of work that you would be doing on your own. While it is extremely useful, it also has some flaws. For example, it is bloated, can be tricky to configure, and can be sometimes difficult in making it do what you want it to.
      - the_spacebyte 6y ago
        It's an absolute mess of a software, to get running and if you're not paying attention you'll install 15+GB of packages you won't need. I've helped some friends with c++ assignments during college and with ROS they had to have dozens of terminal windows open running some command just to get things working.
    - vinnyr 6y ago
      It's a shame that ROS is getting this sort of reputation. It has it's merits, and is used by most robotics applications I have seen. It is akin to the python ecosystem, where there is A LOT of good software and packages out there, but there is also A LOT of garbage out there. The community is nice and supportive, and the framework has really matured recently, with ROS1 being "complete" and ROS2 getting off the ground with a lot of mature features like DDS
blueblisters 6y ago
If they were planning to open-source this all along, I'm curious if Ardupilot [1] would have worked for this. The Ardupilot flight stack is quite mature for Earth-based aircraft, I suppose they could make it work for Mars with a few modifications. [1]: https://github.com/ArduPilot/ardupilot https://github.com/ArduPilot/ardupilot
- 05 6y ago
  But they don't really need 90% of the stuff in Ardupilot - driver support for a myriad of sensors and other peripherals, MAVLink protocol, OSD, RC control... All they need is the PID loop and ESC/motor control, and they are using a hardened CPU for that, so the low level interface has to be rewritten. And the visual navigation stuff that's running on Snapdragon doesn't exist in Ardupilot anyway..
jimmyed 6y ago
One of the devs working on this library. AMA!
- techdragon 6y ago
  What do you think of the current equivalent software for satellites? NASA have a few options, there’s KubOS, and I’m sure there might be more I haven’t heard about. I’d love some insights and options from someone working on similarly “mission critical” software frameworks.
- okl 6y ago
  What is the relation between F' and cFS/cFE?
  - jimmyed 6y ago
    Disclaimer: I am an intern who recently joined the team F' is actually quite older than all those systems. Several generations of scientists and engineers have worked on it and the code's current form is a result of countless iterations on generations of software. One interesting tidbit I caught recently was how programs generated using cFS acted up in the magnetic field on Mars due to the bit patters of the instructions in the final compiled executable. F' fixed that.

189 points by zeristor 6y ago

zeristor 6y ago

How long before Rust will be mature enough for the task?

foobar33333 6y ago
Probably once people have decades of experience with it and know every single trap or quirk perfectly. Rust almost certainly could do the job now but stakes are so high no one would take that risk when its proven that C can do it and with enough auditing and conservatism, it can be done pretty safely.
- bri3d 6y ago
  I don't think the barrier is _people_ knowing the traps, as people are always fallible and any system relying on them knowing the "traps and quirks" is fundamentally pointless. I do think the barrier is, rather, _tools_ knowing the traps. Most systems in this class, FPrime included, rely extensively on code generation and model-to-code auditing, which, while usually not formally proven (unfortunately), is battle-tested. Now, these sorts of systems should actually be _easier_, in the long-term, to build in Rust, since the type system can enable a class of proof which simply was not historically possible, but for the time being, the tooling doesn't exist yet.
- cat199 6y ago
  > Probably once people have decades of experience with it and know every single trap or quirk perfectly. people were writing mission-critical C++ when C++ was new / only a few years old; with this in mind, rust is probably good to go with sufficient application/system testing that said, since C++ & associated tooling exists, there is more of an opportunity cost since, in the context of today, there are more alternatives that could be considered
  - carlmr 6y ago
    I think this is spot on. The tooling is there for C++, but human mistakes are much more prevalent, and the discipline to apply the tooling is not a given. There should be an industry push for certified Rust tooling, it would save the aerospace and auto industry billions. Or you could use the unsexy but also very good ADA 2012, which is already certified.
    - pjmlp 6y ago
      This is one of the reasons why NVidia went with Ada/SPARK for their security critical firmware project.
      - sterlind 6y ago
        iirc, SPARK has proof capabilities that outstrip the memory-safety guarantees of Rust. basically design by contract, where you can check loop invariants and statically verify complex preconditions and postconditions. I suppose the workflow would be to flesh out and check the abstract design in something like Coq or (maybe) TLAPS, generate a refinement into the SPARK code contracts, then implement the functions. Since the toolchains are verified there shouldn't be much surface area for bugs left.
        pjmlp 6y ago
        Yep, here some very good books about it, specially relevant given the main subject. "Building High Integrity Applications with SPARK" https://www.amazon.com/Building-High-Integrity-Applications-SPARK/dp/1107656842 https://www.amazon.com/Building-High-Integrity-Applications-... "Building Parallel, Embedded, and Real-Time Applications with Ada" https://www.amazon.com/Building-Parallel-Embedded-Real-Time-Applications/dp/0521197163 https://www.amazon.com/Building-Parallel-Embedded-Real-Time-... "Embedded Software Development for Safety-Critical Systems" https://www.amazon.com/Embedded-Software-Development-Safety-Critical-Systems/dp/0367338858 https://www.amazon.com/Embedded-Software-Development-Safety-...
- gregors 6y ago
  Here's a pretty interesting read regarding Lisp at JPL. http://www.flownet.com/gat/jpl-lisp.html http://www.flownet.com/gat/jpl-lisp.html I think the "safety" of "familiarity" vs pushing the envelope of what we can do technically are different things. We used to build brand new computers and operating systems from scratch specifically for these types of things. The risks are indeed high for managerial staff. I worked at a large quasi-government place. "you won't ever get fired for using Microsoft, Oracle, etc" was a tagline we heard often in non-critical systems, so I imagine there would need to be some major technical reason to switch. Now drones on the other hand... https://en.wikipedia.org/wiki/Iran%E2%80%93U.S._RQ-170_incident https://en.wikipedia.org/wiki/Iran%E2%80%93U.S._RQ-170_incid...
bobthebuilders 6y ago
Never. Rust will never be good enough to replace C.
- kamranjon 6y ago
  this is c++
mhh__ 6y ago
Keep in mind that for this kind of project you want static analysis and formal verification (model checking for example) rather than just day-to-day safety features. I.e. the Rust this, Rust that spam is a little naive to the task at hand, even though it would be a step up from C
- pensono 6y ago
  Is C++ complex enough that it is difficult to model, and therefore hard to apply in formal methods?
  - rurban 6y ago
    The problem is not the language, the problem are unbounded loops. Like linked lists vs vectors. Termination is theoretically impossible to prove, but practically you can handle it. Parts of the STL were formally verified. cprover (with satabs and cbmc) can handle C, C++ or Java. F' uses autogenerated classes, which helps a lot avoiding mistakes.
    - gugagore 6y ago
      Because the problem is unsolvable, there is a wide variety of "you can handle it"-ness that a language can have...
- OnlyOneCannolo 6y ago
  NASA even has their own sound static analyzer for memory safety. If you use something like that, and depending on the context, there isn't even necessarily a memory safety advantage to using Rust over C or C++. https://github.com/NASA-SW-VnV/ikos https://github.com/NASA-SW-VnV/ikos
- gregors 6y ago
  It was my understanding that when formal methods were used, they were used on very small subsets of code and not used in general. I do wonder about TLA+ and would love to hear more about how they use such tools. I know I've seen an older document that specifically prohibited use of malloc that the risk was too great. Is that still the case?
otabdeveloper4 6y ago
Use-after-free is a) probably the least important class of bugs for this sort of thing b) adequately solved with the existing C++ language features anyways. So what would be the point of rewriting in Rust? (Assume the people writing it aready have the C++ knowledge and tooling ready.)
- pjmlp 6y ago
  c) assuming they have ISO C++ minutiae level of language understanding, https://herbsutter.com/2020/02/17/move-simply/ https://herbsutter.com/2020/02/17/move-simply/
- hctaw 6y ago
  What about iterator invalidation or multiple mutable aliasing in concurrent code
  - otabdeveloper4 6y ago
    Iterator invalidation is a kind of use-after-free. Mutating aliased objects is, of course, usually the desired outcome and not a bug. It becomes a bug when your program's concurrency logic is not thought through, and there are no easy solutions here.

Linked_Liszt 6y ago

It's cool that this framework is getting some attention. In our college senior design project, we built a small prototype using this framework during a trade study. We got a few small UI fixes pushed upstream to the main repo. Our team even got to meet up with the maintainers for a few days as they were showing off the framework. It was one of the most interesting and unique software projects I've worked on. The framework itself is portable allowing for code sharing across multiple missions and hardware setups. According to the devs, in the space industry, software is so mission specific and intertwined that it's rarely reused. FPrime's "modules" create hard barriers between sections of the program, something I have mixed feelings about. Finally the "module" system allows for a very easy to use concurrency model, which I think is one of the strengths of the framework. (Though, take these words with a grain of salt as I was and still am wildly underqualified in the domain of embedded systems)

numpad0 6y ago

So it’s ROS replacement that doesn’t suck?

jvanderbot 6y ago
Half true!
- 0xFFC 6y ago
  Can you elaborate more on this?
  - nexthash 6y ago
    ROS stands for Robotic Operating System. It is a framework of different tools such as an abstraction layer, libraries, and a package manager that makes it easier to program/interface with different robotic systems/components. It basically simplifies a lot of work that you would be doing on your own. While it is extremely useful, it also has some flaws. For example, it is bloated, can be tricky to configure, and can be sometimes difficult in making it do what you want it to.
    - the_spacebyte 6y ago
      It's an absolute mess of a software, to get running and if you're not paying attention you'll install 15+GB of packages you won't need. I've helped some friends with c++ assignments during college and with ROS they had to have dozens of terminal windows open running some command just to get things working.
  - vinnyr 6y ago
    It's a shame that ROS is getting this sort of reputation. It has it's merits, and is used by most robotics applications I have seen. It is akin to the python ecosystem, where there is A LOT of good software and packages out there, but there is also A LOT of garbage out there. The community is nice and supportive, and the framework has really matured recently, with ROS1 being "complete" and ROS2 getting off the ground with a lot of mature features like DDS

blueblisters 6y ago

If they were planning to open-source this all along, I'm curious if Ardupilot [1] would have worked for this. The Ardupilot flight stack is quite mature for Earth-based aircraft, I suppose they could make it work for Mars with a few modifications. [1]: https://github.com/ArduPilot/ardupilot https://github.com/ArduPilot/ardupilot

05 6y ago
But they don't really need 90% of the stuff in Ardupilot - driver support for a myriad of sensors and other peripherals, MAVLink protocol, OSD, RC control... All they need is the PID loop and ESC/motor control, and they are using a hardened CPU for that, so the low level interface has to be rewritten. And the visual navigation stuff that's running on Snapdragon doesn't exist in Ardupilot anyway..

jimmyed 6y ago

One of the devs working on this library. AMA!

techdragon 6y ago
What do you think of the current equivalent software for satellites? NASA have a few options, there’s KubOS, and I’m sure there might be more I haven’t heard about. I’d love some insights and options from someone working on similarly “mission critical” software frameworks.
okl 6y ago
What is the relation between F' and cFS/cFE?
- jimmyed 6y ago
  Disclaimer: I am an intern who recently joined the team F' is actually quite older than all those systems. Several generations of scientists and engineers have worked on it and the code's current form is a result of countless iterations on generations of software. One interesting tidbit I caught recently was how programs generated using cFS acted up in the magnetic field on Mars due to the bit patters of the instructions in the final compiled executable. F' fixed that.