// If we have less writers than the buffer space available, we should
// not loose events.
// assert(NUMPROCS + NUMSWITCH > BUFSIZE || events_lost == 0);

[]((have_events_lost) -> (!buffer_large_enough))