Added two more styles of lock spec with explicit share; I believe they can be proved equivalent to the existing ones, but I don't have the proofs.