Anna Lyons

Can you please provide more context? AFAICT this PR does the following: * Adds a new type of log buffer for use debugging, which is more flexible as it doesn't...

I don't think this patch is worth the verification effort. There are many patches which have significant impacts in the queue for verification. Our engineering processes have always weighed verification...

Thanks for raising this for early feedback, this is excellent as it helps us get on the same page before too much time is invested. Please state explicitly what is...

@alwin-joshy thanks for the reply. I am indeed quite familiar with the issues that come up when writing fastpaths for the kernel, especially the scheduling context parts, since I designed...

oh and on check domain time - you definitely don't want to fastpath the domain switch.

Can we keep the deprecated files, even if they are empty? I'm sure we will deprecate more things in future, and it's good to have an established pattern/placeholder to put...

> > Can we keep the deprecated files, even if they are empty? I'm sure we will deprecate more things in future, and it's good to have an established pattern/placeholder...

I believe seL4_Signal is intended to be fire and forget. That said, I've noted before that the error handling in the kernel api isn't always consistent. It could make sense...

The only reason I didn't treat the idle thread specially is it was less code - so I hoped less proof pain, obviously not :). Ideally the idle thread would...

Signed CLA has been sent. This looks good to merge history wise, just let me know if you want any changes.