Reduce sizes of pthreads-related types

[zvonimir]

Our model of pthreads mostly leverages C int type for various pthreads types and structure fields. That is fine when mathematical integers are used to model C integers. However, when bit-vectors are used, I wonder if in many situations using (typically) 32 bit integers is an overkill, and if we would gain performance by reducing those to smaller bit-widths when possible.