extern unsigned int get_uncached_mask       ();
extern void         set_uncached_mask       (unsigned int);