+/**
+ * The basic encoding idea is that (void *) either:
+ * -# points to a full record (RaceRecord) or
+ * -# encodes the information in a 64 bit word. Encoding is as
+ * follows:
+ * - lowest bit set to 1
+ * - next 8 bits are read thread id
+ * - next 23 bits are read clock vector
+ * - next 8 bits are write thread id
+ * - next 23 bits are write clock vector
+ */