model: mutex synchronization -> re-check release sequences