Indan Zupancic

> > Please give one example where passing tagged pointers via IPC is imperative, and keep in mind that it can always be done via shared memory if really necessary....

> > Only accesses one register at a time, so doesn't need to go via the IPC buffer. > > By default it does? For example if you look at...

> Well again, we are 100% on the same page here. But "enforcing" no propagation of tags between address spaces doesn't have to do anything with making msg[] an array...

Welcome to one of the most tricky parts of using seL4, CSpace management! Instead of repeating myself more, I'll link to [a thread on the devel mailinglist](https://lists.sel4.systems/hyperkitty/list/[email protected]/thread/CUPYGM2I3E4IWLWZFCXBFWB3W26GUHAX/) which discusses some...

Why not just: ``` #define irqInvalid 255U ``` And for GIC SMP: ``` #define irqInvalid CORE_IRQ_TO_IRQT(-1, -1) ``` And get rid of those stupid globals. It compiles for me. (I...

> Because we need the value to have a symbolic name in the verification if we want to keep the proof generic. If it's a `#define`, the proof only sees...

> Considering that the generated invocation functions take responsibility for marshalling and unmarshalling the call into message registers for the general case, it's likely an oversight that they don't do...

Oh wow, I didn't know about `seL4_getFault`. That doesn't seem like a very convenient way of decoding errors.

Once we fix VPPI virtual timer interrupt not to use maskInterrupt, it's safe to resurrect and merge #1399. The only reason not to merge it before was because of the...

> The ICC_SRE_EL1 also needs to be saved and restored at vCPU switch - I will add this later here Is this really necessary? The only bit that EL1 can...