To allow reasoning about an entire class of types of schedules /
processor modules, it's useful to have named definitions for various
invariants that processor models ensure. Let's collect these centrally
where we introduce processor models and schedules.