Hi, indeed, the patch doesn't keep separate copies of debug registers and just directly sets cp15.* values, as I was not aware of the issue—thanks for the detailed explanation.
I remain available to implement the required fixes, but I'd need some guidance on how to proceed. Thanks, -- Francesco