4 ms·

Well... it's non-trivial to use seL4 correctly. It has all of the facilities to build something great and very little rails to ensure that you actually do. CAmk

Well... it's non-trivial to use seL4 correctly. It has all of the facilities to build something great and very little rails to ensure that you actually do. CAmkES, the component framework to help you do that, is... challenging in all the wrong ways. The proof evidence is very hard to extend meaningfully for new platforms, and you're limited to environments which have a sufficient MMU. We're starting with seL4 and building a whole Rust-based userland around it, and creating a whole pile of compile-time assurances along the way to make sure we're not inadvertently doing something dangerous or stupid with the rope seL4 gives you. It's worth it for us. However, it is a colossal pain in the ass. That said, in the coming months we're likely to open source some of our progress in making it easier and more reliable to work with, integrate with, and otherwise leverage seL4 for certain use cases.

Scramblejams 8y ago
Deets would be appreciated. Sounds interesting.
thenewwazoo 8y ago
I'm super interested in the work you're doing. I spent a couple of weekends building bindings and trampolines to get Rust binaries linked into Chibi/OS and FreeRTOS and it worked really well. I've always wanted to work with seL4, so I downloaded the source and started working through the tutorials and... oh dear. There ended my experiments trying to add Rust into the mix. So if there's any way I can subscribe or otherwise keep abreast of the work you're doing, I'd love to do that. As an aside, I wonder just how much async/await in Rust will obviate the need for small kernels in deeply embedded applications. If I can do blocking IO with my peripherals and use the async state machines to do "task" switching, well... who needs tasks and capabilities? It'd land somewhere on the "language OS" side of an embedded OS almost.
- guywhocodes 8y ago
  >If I can do blocking IO with my peripherals and use the async state machines to do "task" switching, well... who needs tasks and capabilities? It'd land somewhere on the "language OS" side of an embedded OS almost. Waiting directly on the resource like that would require exclusive access quite often though?
- im_down_w_otp 8y ago
  At the moment we're light on marketing materials & outreach. We've been heads down bootstrapping and working with early customers. When we open source things in the coming weeks & months they'll all land on GitHub, https://github.com/auxoncorp https://github.com/auxoncorp, so that's probably the lowest touch way of observing what we're up to as things mature.
- Matthias247 8y ago
  async/await in embedded is actually an interesting thing, that i also evaluated. I think it can't be an alternative to preemptive RTOS kernels, since the cooperative nature doesn't allow to process things within guaranteed deadlines. Therefore I think async/await might end up more as an add-on to RTOS: All time-critical things are run within independent RTOS tasks. And all the remaining and less critical stuff could potentially be run inside a single-threaded async/await scheduler. While Rust seems to be promising here, I'm not sure whether the current async/await implementation will really allow for this. I experimented a bit with it, and found lots of issues where async/await lead to severe memory bloat (composing 3 async functions that do not a lot things requiring a 20kB task allocation). The compatibility with Futures and the requirement to move async fns to compose them before using them (which requires extra stack - which again ends up as extra heap/task memory) plays a bit against it. But these things are also worked on, so let's seee how it works out.
  - deleted 8y ago
    [deleted]

Scramblejams 8y ago

Deets would be appreciated. Sounds interesting.

thenewwazoo 8y ago

I'm super interested in the work you're doing. I spent a couple of weekends building bindings and trampolines to get Rust binaries linked into Chibi/OS and FreeRTOS and it worked really well. I've always wanted to work with seL4, so I downloaded the source and started working through the tutorials and... oh dear. There ended my experiments trying to add Rust into the mix. So if there's any way I can subscribe or otherwise keep abreast of the work you're doing, I'd love to do that. As an aside, I wonder just how much async/await in Rust will obviate the need for small kernels in deeply embedded applications. If I can do blocking IO with my peripherals and use the async state machines to do "task" switching, well... who needs tasks and capabilities? It'd land somewhere on the "language OS" side of an embedded OS almost.

guywhocodes 8y ago
>If I can do blocking IO with my peripherals and use the async state machines to do "task" switching, well... who needs tasks and capabilities? It'd land somewhere on the "language OS" side of an embedded OS almost. Waiting directly on the resource like that would require exclusive access quite often though?
im_down_w_otp 8y ago
At the moment we're light on marketing materials & outreach. We've been heads down bootstrapping and working with early customers. When we open source things in the coming weeks & months they'll all land on GitHub, https://github.com/auxoncorp https://github.com/auxoncorp, so that's probably the lowest touch way of observing what we're up to as things mature.
Matthias247 8y ago
async/await in embedded is actually an interesting thing, that i also evaluated. I think it can't be an alternative to preemptive RTOS kernels, since the cooperative nature doesn't allow to process things within guaranteed deadlines. Therefore I think async/await might end up more as an add-on to RTOS: All time-critical things are run within independent RTOS tasks. And all the remaining and less critical stuff could potentially be run inside a single-threaded async/await scheduler. While Rust seems to be promising here, I'm not sure whether the current async/await implementation will really allow for this. I experimented a bit with it, and found lots of issues where async/await lead to severe memory bloat (composing 3 async functions that do not a lot things requiring a 20kB task allocation). The compatibility with Futures and the requirement to move async fns to compose them before using them (which requires extra stack - which again ends up as extra heap/task memory) plays a bit against it. But these things are also worked on, so let's seee how it works out.
- deleted 8y ago
  [deleted]