Skip to content
flowss
Start freeChecking your session
Petri Nets templates

Mutex / critical section

Two competing threads share a single mutex token — only one can hold it at a time.

Petri NetsUML & SoftwarePetri Nets syntax docs
Template previewPetri Nets
Mutex with two threadsThread 1 idle≤1Thread 2 idle≤1Mutex≤1T1 acquireenabledT2 acquireenabledT1 critical≤1T2 critical≤1T1 releaseT2 releaseReachable markings35 places · 4 transitionsTerminatesneverruns for everLive transitions4/4every one firesSafe places5/5bound ≤ 1 tokenConservation laws3every place covered3 reachable markings, 5 places, 4 transitions — bounded, deadlock-free, and every transition fires.Conservation law: Mutex + T1 critical + T2 critical = 1, at every reachable marking, for ever. No firing of any transition can change it — that is proved from the incidence matrix, not observed ove…Conservation law: Thread 2 idle + T2 critical = 1, at every reachable marking, for ever. No firing of any transition can change it — that is proved from the incidence matrix, not observed over a se…Conservation law: Thread 1 idle + T1 critical = 1, at every reachable marking, for ever. No firing of any transition can change it — that is proved from the incidence matrix, not observed over a se…

Make it your own.

title Mutex with two threads

place P1_Idle    tokens 1 "Thread 1 idle"
place P2_Idle    tokens 1 "Thread 2 idle"
place Mutex      tokens 1 "Mutex"
transition T1_Acq "T1 acquire"
transition T2_Acq "T2 acquire"
place P1_Critical "T1 critical"
place P2_Critical "T2 critical"
transition T1_Rel "T1 release"
transition T2_Rel "T2 release"

P1_Idle -> T1_Acq
Mutex   -> T1_Acq
T1_Acq  -> P1_Critical

P1_Critical -> T1_Rel
T1_Rel  -> Mutex
T1_Rel  -> P1_Idle

P2_Idle -> T2_Acq
Mutex   -> T2_Acq
T2_Acq  -> P2_Critical

P2_Critical -> T2_Rel
T2_Rel  -> Mutex
T2_Rel  -> P2_Idle