Первые два условных оператора (строчки 17, 22) кода на C моделируются наличием ветки с goto exit; в первом if модели на Промеле.

Далее возможны следующие варианты:
1) третий условный оператор (строка 28) ведет к ветке else (строка 104), тогда либо выполняется return либо код продолжит выполнение. это смоделировано наличием веток skip; и goto exit; в первом if модели на Промеле;
2) выполнится kzalloc, затем произойдет проверка его успешности. эти действия смоделированы явно.
  2.1) далее либо сработает return (в усл. операторах на строках 49, 70 или 95)
  2.2) либо произойдет kfree, а лишь затем return
  2.3) ни один условный оператор (строки 49, 70, 79, 95) не сработает
  все эти варианты и представлены во вложенном if (строка 46) в коде на Промеле. 
  
Затем все просто. Выполняется вход в критическую секцию. Моделируется возможное зацикливание на строке 131. Выполняется выход из критической секции.
Для реализации монопольного доступа к критической секции используется алгоритм Петерсона.

В канал передается идентификатор отправителя, тип сообщения - от менеджера или от процесса, тип операции - выделение памяти, освобождение (или резултат - успешно или нет).

Магические вычитания 2 и 3 в lock_section() из-за того, что pid у экземпляров pcbit_receive равны 2 и 3, а не 0 и 1 (0 - init, 1 - memory_manager).