1) В каждом вычислении рано или поздно происходит попытка захвата ресурса при помощи указанного вызова *alloc*
#define c_start (pcbit_receive[2]@start)
#define c_exit  (pcbit_receive[2]@exit)
#define c_alloc (pcbit_receive[2]@alloc_lbl)

![](c_start -> (!c_exit U c_alloc))

2) В каждом вычислении, после успешного захвата ресурса рано или поздно ресурс освобождается при помощи вызова *free*
#define c_free  (pcbit_receive[2]@free_lbl)

![]((c_start && <>c_exit) -> ((c_alloc -> (!c_exit U c_free)) U c_exit))

3) На каждый вызов системной функции выделения и освобождения ресурса обязательно поступит отклик от менеджера  ресурсов
#define c_gimme    (pcbit_receive[2]@gimme_lbl) 
#define c_gimme_ok (pcbit_receive[2]@gimme_ok_lbl)
#define c_free_ok  (pcbit_receive[2]@free_ok_lbl)

![]((c_start && <>c_exit) -> ((c_gimme -> (!c_exit U c_gimme_ok)) && (c_free -> (!c_exit U c_free_ok))) U c_exit)

4) В критической секции (между вызовами spin_lock* и spin_unlock*) может находиться  не более одного процесса
#define c_forever_1 (pcbit_receive[2]@forever_lbl)
#define c_forever_2 (pcbit_receive[3]@forever_lbl)

<>(c_forever_1 && c_forever_2)

5) В ходе одной итерации функции функция kfree вызывается не более одного раза
#define c_kfree (pcbit_receive[2]@free_lbl)

![]((c_start && <>c_exit) -> ((c_kfree -> ((c_kfree U c_exit) || (c_kfree U (!c_kfree U c_exit)))) U c_exit))