__bitlock
__acquires(__bitlock(bitnum, addr))
__acquire(__bitlock(bitnum, addr));
__cond_acquires(true, __bitlock(bitnum, addr))
__acquire(__bitlock(bitnum, addr));
__releases(__bitlock(bitnum, addr))
__release(__bitlock(bitnum, addr));
__releases(__bitlock(bitnum, addr))
__release(__bitlock(bitnum, addr));
__acquires(__bitlock(0, b))
__releases(__bitlock(0, b))
__acquires(__bitlock(0, bkt))
__acquires(__bitlock(0, bucket))
__releases(__bitlock(0, bkt))
__releases(__bitlock(0, bkt))
__release(__bitlock(0, bkt));
int counter __guarded_by(__bitlock(3, &bits));