ARM GCC inline assembly

Introduction

Just now I want to print the ARM CP15 registers' value in a C function, I know I need the inline assembly technology. After read some codes in linux kernel and searched the internet, I have got some simple idea.

Examples
Read ARM ID code:

u32 val;
__asm__ __volatile__ ("mrc p15, 0, %0, c0, c0, 0" : "=r" (val));
printk("ARM ID code: 0x%x\n", val);

Write TTB:

u32 val
/*... */
__asm__ __volatile__ ("mcr p15, 0, %0, c2, c0, 0" : : "r" (val));

For more information, see:
http://www.ibiblio.org/gferg/ldp/GCC-Inline-Assembly-HOWTO.html