Что-то Рифат сильно усложняет.

Предполагаем, что конвейер, буфер ветвлений, сопроцессор и память сделаны как надо. (* иначе остальные рассуждения -- бессмысленны *)

Верифицировать программу невозможно, если одна часть программы лезет в данные другой части программы.
Пример дурного кода:
## Код:
```
MODULE A;
VAR
  i*: INTEGER:
..........
MODULE B;
BEGIN
F.i := Random(infinity);
END B.
```


Пример уже кода получше:
## Код:
```
MODULE A;
CONST
  MAX_i = 1000;
VAR
  i-: INTEGER:
PROCEDURE Set_i(val:INTEGER);
BEGIN
  ASSERT(val<MAX_i);
  i := val;
END Set_i;
..........
MODULE B;
BEGIN
F.Set_i(Random(infinity));
END B.
```

Здесь контракт присвоения сделает своё чёрное дело. Память не общая + контролируемый доступ на присвоение.
Соответственно, присвоение не требует дополнительного контроля. Оберон-07 рулит.

На уровне присвоения гранулирование обеспечено.

Второй этап. Даже если значения правильные, один гринлет (* уж простите, сопоток -- может вызвать недопонимание *) может конкурировать за текущие значение с другим гринлетом за глобальный объект. Вот здесь диспетчер и нужен. Планировщик решает, что и когда будет исполняться, и диспетчер решает что исполняется. Т. е. СЕЙЧАС. И если какой-то глобальный объект нужен всем, а гринлет не успевает, диспетчер ему говорит: значит так зелёный: твой контекст сохраняю, досвидос. И когда наступает очередной квант этого гринлета -- диспетчер ему восстанавливает контекст (если он ещё актуален). Либо у гринлета есть альтернатива -- закончит работу с глобальным объектом досрочно.

Отсюда давно известное правило: глобальных объектов должно быть как можно меньше.

Это не доказательство правильности алгоритма гринлета. Вообще, при взаимодействии с открытым миром -- могут быть какие угодно алгоритмы (например, через сериализацию/экстернализацию -- динамическая подгрузка модулей). Как их проверять? Вторая проблема уже была озвучена в соседней ветке форума: как будем доказывать правильность доказательной части алгоритма?

Поэтому, я склоняюсь к варианту, когда нет потери контроля над гринлетами, и есть элементы контрактного программирования. Тут даже динамические языки могут что-то из себя изобразить.

З.Ы. Нечаянно подумал, что сериализация -- куда менее удачный термин, чем экстернализация. В википедии "сериализация" есть, а "экстернализации" -- нет.