On Thu, 27 Mar 2025 at 03:07, Anton Burtsev <aburt...@flux.utah.edu> wrote:
> Hi William > > Thank you for bringing this up! I've heard of this technique and that's > why I wanted to explicitly clarify this use case. Intuitively it feels > extremely hard to get right -- transactions that can abort on any memory > access, yet you want to recover to some clean state. That's the thing though, they can't abort on any memory access, only on access to the volatile message mapped into a (usually statically known) location. You can reduce the state space further by only reading/writing from the message from a single place in the program - doing your unmarshalling up front, and building your output right before notifying the client. > Imagine trying to > verify something like this -- it's concurrency on steroids. I.e., I get > it, maybe it's possible, especially with some careful programming > primitives but it seems very very hard and impractical. > > Is there a link to source code? > Sorry, I don't know if there are any public examples of this technique. I'd like to release some drivers I have that use this (specifically, they abort the transaction and return to open wait), but that is a bit involved right now. In practice though, it involves restoring the registers of the driver process to a previously known-safe state, which means dropping the message currently being handled on the floor. presumably the caller was fine with this. -- William ML Leslie _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
