Hi Marc,

On 2015/12/1 1:56, Marc Zyngier wrote:

Same remark here as the one I made earlier. I'm pretty sure we don't
call any CP15 reset because they are all shared with their 64bit
counterparts. The same thing goes for the whole series.

Ok, I see. But within the 64bit reset function, it needs to update the
32bit register value, right? Since when accessing these 32bit registers,
it uses the offset c9_PMXXXX.

Thanks,
-- 
Shannon