Drivers use cmpxchg64, cmpxchg64_local to perform 64-bit operation, so
they can cross 32-bit and 64-bit platforms (it is a standard way).
Signed-off-by: NChen Gang <gang.chen@asianux.com>
Signed-off-by: NCatalin Marinas <catalin.marinas@arm.com>