Semaphore

Propriétés :
soit np(s) le nombre d'instructions P pour s,
soit mv(s) le nombre d'instructions V pour s,
soit e₀(s) la valeur initiale du sémaphore s.
On a :

e(s) = e₀(s) - np(s) + nv(s)

soit nf(s) le nombre de processus qui ont franchi P(s).

nf(s) £ np(s)

Théorème :

nf(s) = min( np(s), e₀(s) + nv(s))