| digraph mutex_states { |
| // States |
| free; |
| locked; |
| unlocking; |
| dead; |
| |
| // Valid transitions |
| dead -> free [ label="initialized" ]; |
| free -> locked [ label="locked" ]; |
| locked -> unlocking [ label="unlocked\nby owner" ]; |
| unlocking -> free [ label="unlock completed" ]; |
| unlocking -> locked [ label="lock changed owner" ]; |
| free -> dead [ label="destroyed" ]; |
| |
| // Bad transitions |
| dead -> locked [ style=dotted, label="locked\nafter destroy" ]; |
| dead -> free [ style=dotted, label="unlocked\nafter destroy" ]; |
| |
| locked -> free [ style=dotted, label="unlocked\nby non-owner" ]; |
| locked -> dead [ style=dotted, label="destroyed\nwhile locked" ]; |
| } |