Max ops per thread.

HBAcqRel is an HBGenerator that implements acquire/release.

HBModel is a generalized memory model with a plug-in happens-before graph generator.

HBSC is a HBGenerator that implements sequential consistency.

HBTSO is an HBGenerator that implements TSO.

HBUnordered is an HBGenerator that implements fully relaxed memory order where the *only* order observed is local program order.

An OutcomeSet records the set of permissible outcomes of an execution.

SCModel models all loads and stores as sequentially consistent.

TSOModel models all loads and stores as TSO operations, possibly with additional barriers.

HBGenerator generates a happens-before graph.

MemState stores the memory state of an executing program.

An Outcome represents the outcomes of all instructions in an execution.