/** Violently terminates the thread. This should only be used as a last
resort, as the thread gets no chance to clean up. */
void kill();
/** Violently terminates the thread. This should only be used as a last
resort, as the thread gets no chance to clean up. */
void kill();