/* Buffers are identified by a 32-bit opaque ID. We divide the ID
* into a buffer number (low bits) and a cookie (high bits). The buffer number
/* Buffers are identified by a 32-bit opaque ID. We divide the ID
* into a buffer number (low bits) and a cookie (high bits). The buffer number