The placement of pre-lock conditions' definition seems wrong. Would it be better to place it below the list of steps and reference it as a step in the algorithm for lock()? As it is, I assume it is meant to be optionally run before invoking the mandatory numbered steps. But the interleaving of "You MUST:, MAY do this, steps" throws me off.