Indan Zupancic

The driver uses a [SET_REGISTER ](https://github.com/seL4/seL4/blob/master/src/drivers/timer/am335x-timer.c#L36) macro which loops till value is set for some registers, but only for MCS. It was introduced in commit cd956d576. Maybe the same applies...

The datasheet can be found [here](https://www.ti.com/lit/ug/spruh73q/spruh73q.pdf?ts=1660604848840). It recommends enabling posted mode, but I don't see the driver doing that. It says: _Refer to the AM335x errata for advisories associated with...

> I think looping until the value is set makes sense as a fix as it's likely a synchronization issue. Why would it only be needed for MCS though? I...

> The main use case I can think is to skip threads stuck on a spin lock that might be waiting for a thread blocked on a notification to kick...

> In practice I doubt it's a serious issue. I fear it is, as it gives unpredictable behaviour and unfairness, with no control by high priority tasks about how lower...

@gernotheiser Yeah, sorry, I got confused.

> Not 100% sure this is applicable in your context but I think it is so… It doesn't seem to be: - Your first link is about IRQ coalescing in...

> Both are dependent on appending the notification rather than adding it to the head of the queue. FIFO ordering is standard for queue handling, it's seL4 that is strange...

> So deciding to change the implementation to start putting all unblocked threads at the back of the ready queues can potentially have a big impact to the performance of...

> The present behaviour certainly leads to a DOS attack on non-MCS. Deliberate DOS is something else, that's usually easily done. I'm more concerned about behaviour under high load with...