Свобода вмешательства

В информатике — свобода от помех это метод доказательства частичной правильности параллельные программы с общими переменными. Логика Хоара была введена ранее доказывать корректность последовательных программ. В своей кандидатской диссертации (и документы, вытекающие из него ) под руководством советника Дэвида Грайса , Сьюзен Овики расширил эту работу, чтобы применить ее к параллельным программам.

Параллельное программирование использовалось с середины 1960-х годов для кодирования операционных систем как наборов. параллельных процессов (см., в частности, Дейкстра. ), но не было формальный механизм доказательства правильности. Рассуждения о чередующемся выполнении последовательность отдельных процессов была трудной, была подвержена ошибкам, и не масштабировался. Свобода вмешательства применяется к доказательствам, а не к последовательностям выполнения; показывает, что выполнение одного процесса не может повлиять на корректность доказательство другого процесса.

С помощью интерференции была доказана корректность ряда сложных параллельных программ. свобода, а свобода вмешательства составляет основу для большей части последующих работ по разработка параллельных программ с общими переменными и доказательство их корректности. Статья Овицкого-Гриса. Методика аксиоматического доказательства для параллельных программ I. получил премию ACM 1977 года за лучшую работу по языкам программирования и системы.

Примечание. Лэмпорт представляет аналогичную идею. Он пишет: «После написания первоначальной версии этой статьи, мы узнали о недавней работе Овицкий. " Его статья не получила такого большого внимания, как Овики-Грис, возможно, потому, что в ней использовались блок-схемы вместо текста программных конструкций, таких как оператор if и цикл while . Лэмпорт обобщал Флойда метод пока Овицкий-Грис обобщал Метод Хоара. По сути, во всех последующих работах в этой области используются тексты, а не блок-схемы. Еще одно отличие упомянуто ниже в раздел «Вспомогательные переменные» .

Принцип невмешательства Дейкстры.

Эдсгер В. Дейкстра представил принцип невмешательства в EWD 117: «Программирование как человеческая деятельность», написанное примерно в 1965 году. Этот принцип гласит, что: Правильность целого можно установить, приняв во внимание учитывать только внешние характеристики (сокращенные характеристики ) деталей, а не их внутреннее строительство. Дейкстра обрисовал общие шаги по использованию этого принципа:

1. Дайте полную характеристику каждой отдельной детали.
2. Убедитесь, что проблема решена в целом, когда доступны части программы, соответствующие их спецификациям.
3. Создавайте отдельные части, соответствующие их спецификациям, но независимо друг от друга и от контекста, в котором они будут использоваться.

Он привел несколько примеров применения этого принципа за пределами программирования. Но его использование в программировании является основной проблемой. Например, программист, использующий метод (подпрограмму, функцию и т. д.), должен полагаться только на его спецификацию, чтобы определить, что он делает и как его вызывать, и никогда на его реализацию.

Спецификации программ написаны на логике Хоара , предложенной сэром Тони Хоаром . как показано в спецификациях процессов S1 и S2 :

  {pre-S1 }       {pre-S2 }
  С1                 С2
  {после S1 }     {до S2 }

Значение: если выполнение Si в состоянии, в котором предусловие pre-Si истинно, завершается, то по завершении выполняется постусловие. пост-Си верно.

Теперь рассмотрим параллельное программирование с общими переменными. Характеристики двух (или подробнее) процессы S1 и S2 заданы через их пред- и постусловия, реализации S1 и S2 и мы предполагаем, что даны , которые удовлетворяют их требованиям. характеристики. Но при параллельном выполнении их реализаций, поскольку они используют общие переменные, состояние гонки может возникнуть ; один процесс изменяет общую переменную на значение это не предполагается при доказательстве другого процесса, поэтому другой процесс не работает должным образом.

Таким образом, принцип невмешательства Дейкстры нарушается.

В своей кандидатской диссертации 1975 г. в области компьютерных наук , Корнелльский университет , написано под Советник Дэвида Грайса Сьюзен Овики разработала понятие свободы вмешательства . Если процессы S1 и S2 удовлетворяют свободе вмешательства, то их параллельное выполнение будет работать по плану. Дейкстра назвал эту работу первым значительным шагом на пути применения логики Хоара к параллельным вычислениям. процессы. Чтобы упростить обсуждение, мы ограничим внимание только двумя параллельными процессами: хотя Овицкий-Грис позволяет больше.

Свобода от помех с точки зрения схемы доказательства

Овицкий-Грис представил схему доказательства для тройки Хоара {P}S{Q }. Он содержит все данные, необходимые для доказательства правильности {P}S{Q } с использованием аксиом и правил вывода логики Хоара . (В этой работе используются оператор присваивания x: = e , if-then и if-then-else операторы , а также цикл while .) Хоар ссылался на схемы доказательства в своих ранних работах; для свободы вмешательства ее необходимо было формализовать.

Схема доказательства {P}S{Q предусловия P и заканчивается постусловием Q. } начинается с Два утверждения в фигурных скобках { и }, расположенные рядом друг с другом, указывают на то, что первое должно подразумевать второе.

Пример: Схема доказательства для {P} S {Q } где S :
х : = а; если е , то S1 еще S2

  {П }
  {P1[х/а] }
  х : = а;
  {P1 }
  если e , то {P1 ∧ e }
                 С1
                 {Q1 }
        иначе {P1 ∧ ¬ e }
                 С2
                 {Q1 }
  {Q1 }
  {Q }

P ⇒ P1[x/a] должно выполняться, где P1[x/a] обозначает P1 с каждым появление x заменено . на (В этом примере S1 и S2 являются базовыми операторами, такими как оператор присваивания, пропуск или оператор ожидания .)

Каждому утверждению T в схеме доказательства предшествует предварительное условие pre-T , за которым следует постусловие post-T и {pre-T}T{post-T } должно быть доказуемо с использованием некоторой аксиомы или правила вывода логики Хоара. Таким образом, схема доказательства содержит всю информацию, необходимую для доказательства {P}S{Q правильности }.

Теперь рассмотрим два процесса S1 и S2 , выполняемые параллельно, и их характеристики:

  {pre-S1 }       {pre-S2 }
  С1                 С2
  {сообщение-S1 }     {сообщение-S2 }

Чтобы доказать, что они работают параллельно, потребуется ограничить их следующим образом. Каждое выражение E в S1 или S2 может относиться не более чем к одной переменной y , которая может быть изменяется другим процессом во время E оценки , и E может ссылаться на y не более одного раза. Аналогичное ограничение справедливо и для операторов присваивания x: = E.

Согласно этому соглашению, единственным неделимым действием должна быть ссылка на память. Например, предположим, что процесс S1 ссылается на переменную y, а S2 изменяет y . Значение S1 получает для y должно быть значением до или после того, как S2 изменит y , а не каким-то ложным промежуточным значением.

Определение отсутствия помех

утверждение T не мешает доказательству { Важным нововведением Овицкого-Гриса было определение того, что означает, что P}S{Q }. Если выполнение T не может опровергнуть ни одно утверждение, данное в доказательстве схему {P}S{Q }, то это доказательство остается в силе даже в условиях одновременного выполнения S и T .

Определение . Оператор T с предварительным условием pre-T не мешает доказательству {P}S{Q }, если выполняются два условия:

(1) {Q ∧ пре-T} T {Q }
(2) Пусть S' будет любым оператором внутри S , но не внутри оператора await (см. следующий раздел). Тогда {pre-S' ∧ pre-T} T {pre-S' }.

Прочтите последнюю тройку Хоара следующим образом: Если состояние таково, что и Т, и S' могут быть выполнено, то выполнение T не приведет к фальсификации pre-S' .

Определение . Схема доказательства для {P1}S1{Q1 } и {P2}S2{Q2 } не вызывает помех, если выполняется следующее. Пусть T — оператор ожидания или присваивания (который не присутствует в await ) процесса S1 . Тогда T не мешает доказательству {P2}S2{Q2 }. Аналогично для T процесса S2 и {P1}S1{Q1 }.

Заявления начинаются и ждут

Для работы с параллелизмом были введены два утверждения. Выполнение оператора cobegin S1 // Коенд S2 выполняет S1 и S2 параллельно. Он завершается, когда оба S1 и S2 завершаются .

Выполнение await оператора await B , затем S задерживается до тех пор, пока условие B не станет истинным. Затем оператор S выполняется как неделимое действие — оценка B является частью этого неделимого действия. Если два процесса ожидают одного и того же условия B , когда оно становится истинным, один из них продолжает ждать, пока другой продолжает выполняться.

Оператор await не может быть эффективно реализован, и его не предлагается вставлять в язык программирования. Скорее, он предоставляет средства представления нескольких стандартных примитивов, таких как семафоры: сначала выражайте операции с семафорами как await s , а затем применяйте методы, описанные здесь.

Правила вывода для await и cobegin :

ждать
⁠ {P ∧ B} S {Q} / {P} ждут B , затем S {Q} ⁠

начинать
⁠ {P1} S1 {Q1}, {P2} S2 {Q2}
без помех / {P1∧P2} cobegin S1//S2 coend {Q1∧Q2} ⁠

Вспомогательные переменные

не Вспомогательная переменная встречается в программе, но вводится при доказательстве правильности, чтобы сделать рассуждения более простыми или даже возможными. Вспомогательные переменные используются только при присвоении вспомогательных переменных, поэтому их введение не меняет программы для любых входных данных и не влияет на значения переменных программы. Обычно они используются либо в качестве программных счетчиков, либо для записи истории вычислений.

Определение . Пусть AV — набор переменных, которые появляются в S' только в присваиваниях. x: = E , где x находится в AV . Тогда AV — набор вспомогательных переменных для S' .

Поскольку набор AV вспомогательных переменных используется только при присвоении переменных в AV , удаление всех присвоений им не меняет корректность программы, и мы имеем правило вывода AV исключения:

  ⁠ {P} S' {Q} / {P} S {Q} ⁠

AV — набор вспомогательных переменных для S' . Переменные в AV не встречаются P или Q. в S получается из S' удалением всех присвоений переменным в AV .

Вместо использования вспомогательных переменных в систему доказательства можно ввести программный счетчик, но это усложняет систему доказательств.

Примечание: Подходящий обсуждает логику Овицкого-Гриса в контексте рекурсивных утверждений, то есть эффективно вычислимые утверждения. Он доказывает, что все утверждения доказательства изложены может быть рекурсивным, но это уже не так, если вспомогательные переменные используются только в качестве счетчиков программы, а не для записи истории вычислений. Лэмпорт в своей аналогичной работе использует утверждения о позициях токенов вместо вспомогательных переменных, где токен на краю блок-схемы аналогичен программному счетчику. Нет понятия исторической переменной. Это указывает на то, что подходы Овики-Гриса и Лэмпорта не эквивалентны. когда оно ограничено рекурсивными утверждениями.

Тупик и прекращение

Овицкий-Грис касается в основном частичной правильности: {P} S {Q } означает: если S выполнено в состояние, в котором P истинно, завершается, тогда Q истинно для состояния после завершения. Однако Овицкий-Грис также дает некоторые практические приемы, использующие информацию, полученную из частичного доказательства правильности для получения других свойств правильности, включая свободу от тупиковой ситуации, завершения программы и взаимного исключения.

Программа находится в тупике, если все процессы, которые не завершились, выполняются. жду заявлений и никто не может продолжить, потому что их условия ожидания ложны. Овицкий-Грис обеспечивает условия, при которых тупиковая ситуация невозможна.

Овики-Грис представляет правило вывода для полной корректности цикла while . Он использует связанная функция, которая убывает с каждой итерацией и положительна, пока условие цикла истинно. Апт и др. покажите, что это новое правило вывода не удовлетворяет свободе вмешательства. Тот факт, что связанная функция положительна, пока условие цикла истинно, не был включен в тест на интерференцию. Они показывают два способа исправить эту ошибку.

Простой пример

Рассмотрим утверждение:
       {х=0}
       cobegin await true, затем x: = x+1
// ждем true , затем x: = x+2
       сопредседатель
       {х=3}

Схема доказательства:

{х=0}
С: начать
       {х=0}
       {х=0 ∨ х=2}
       S1: дождитесь истины , затем x : = x+1
       {Q1: x=1 ∨ x=3}
     //
       {х=0}
       {х=0 ∨ х=1}
       S2: дождитесь истины , затем x : = x+2
       {Q2: x=2 ∨ x=3}
     сопредседатель
{(x=1 ∨ x=3) ∧ (x=2 ∨ x=3)}
{х=3}

Чтобы доказать, что S1 не мешает доказательству S2, необходимо доказать две тройки Хоара:

(1) {(x=0 ∨ x=2) ∧ (x=0 ∨ x=1} S1 {x=0 ∨ x=1}
(2) {(x=0 ∨ x=2) ∧ (x=2 ∨ x=3} S1 {x=2 ∨ x=3}

Предварительное условие (1) сводится к x=0 , а предварительное условие (2) сводится к x=2 . Отсюда легко видеть, что эти тройки Хоара верны. Две аналогичные тройки Хоара необходимы, чтобы показать, что S2 не мешает доказательству S1 .

Предположим, что S1 заменен оператором ожидания на присваивание х: = х+1 . Тогда схема доказательства не удовлетворяет требованиям, поскольку задание содержит два вхождения общей переменной x . Действительно, значение x после выполнения оператора cobegin может быть 2 или 3.

Предположим, что S1 заменен на ожидания оператор . await true then x: = x+2 , так что это то же самое, что S2 . После выполнения S выполнен x должно быть равно 4. Чтобы доказать это, поскольку два присваивания одинаковы, необходимы две вспомогательные переменные: одна для указания того, был ли ; S1 другой — S2 был ли выполнен . Мы оставляем изменение схемы доказательства на усмотрение читателя.

Примеры формально доказанных параллельных программ

А. Найтипос . Напишите программу, которая находит первый положительный элемент массива (если он есть). Один процесс проверяет все элементы массива в четных позициях и завершается, когда находит положительное значение или когда ничего не найдено. Аналогично другой процесс проверяет элементы массива в нечетных позициях массива. Таким образом, в этом примере рассматриваются циклы while . Он также не имеет операторов ожидания .

Этот пример принадлежит Барри К. Розену. Решение в Овицкий-Грис, вместе с программой, схемой доказательства и обсуждением свободы вмешательства занимает менее двух страниц. Свободу помех проверить довольно легко, поскольку имеется только одна общая переменная. Напротив, Розен статья использует Findpos в качестве единственного работающего примера в этой 24-страничной статье.

Схема обоих процессов в общей среде:

cobegin : ... продюсер
     дождаться входа-выхода < N, затем пропустить ;
     добавить: b[в моде N]:= следующее значение;
     отметка: в: = в+1;
     ...
  //
     потребитель: ...
     дождитесь входа-выхода > 0 , затем пропустите ;
     удалить: это значение:=
        б[выход мод N];
     разметка: выход: = выход+1;
сопредседатель
...

B. Проблема потребителя/производителя ограниченного буфера . Процесс-производитель генерирует значения и помещает их в ограниченный буфер b размера N ; потребительский процесс удаляет их. Они действуют с переменной скоростью. Производитель должен дождаться, если буфер b полон; потребитель должен ждать, если буфер b пуст. В Овицкий-Грис, показано решение в общей среде; затем он встраивается в программу, которая копирует массив c[1..M] в массив d[1..M] .

Этот пример демонстрирует принцип, позволяющий свести к минимуму проверки взаимодействий: поместите как можно больше в утверждение, которое инвариантно истинно везде в обоих процессах. В этом случае утверждение представляет собой определение ограниченного буфера и границ переменных, которые указывают, сколько значений было добавлено в буфер и удалено из него. Помимо самого буфера b , две общие переменные записывают количество входных значений, добавленных в буфер, и количество выходных значений , удаленных из буфера.

C. Реализация семафоров . В своей статье о мультипрограммной системе THE Дейкстра представляет семафор sem как примитив синхронизации: sem — целочисленная переменная, на которую можно ссылаться только двумя способами, как показано ниже; каждая представляет собой неделимую операцию:

1. P(sem) : Уменьшите sem на 1. Если теперь sem < 0 , приостановите процесс и поместите его в список приостановленных процессов, связанных с sem .

2. V(sem) : увеличьте sem на 1. Если теперь sem ≤ 0 , удалите один из процессов из списка приостановленных процессов, связанных с sem , чтобы его динамический прогресс снова стал допустимым.

Реализация P и V с использованием операторов ожидания :

П (без):
       жди правда тогда
          начать как: = as-1;
              если sem < 0, то
                w[этот процесс]: = true
          конец ;
          ожидайте ¬w[этот процесс]
                тогда пропусти

Вопрос(Я):
       жди правда тогда
          начать как: = as+1;
              если sem ≤ 0 , то
                 начни выбирать такой ​
                                   что w[ p ];
                            ш[ р ]: = ложь
                 конец
          конец

Здесь w — это массив процессов, ожидающих, поскольку они были приостановлены; изначально w[p] = false для каждого процесса p . Можно изменить реализацию, чтобы всегда будить самый длинный приостановленный процесс.

D. Сбор мусора «на лету» . На Летней школе в Марктобердорфе 1975 года Дейкстра обсуждал оперативный сборщик мусора как упражнение для понимания параллелизма. Структура данных, используемая в традиционной реализации LISP, представляет собой ориентированный граф, в котором каждый узел имеет не более двух исходящих ребер, любое из которых может отсутствовать: исходящее левое ребро и исходящее правое ребро. Все узлы графа должны быть достижимы из известного корня. Изменение узла может привести к появлению недоступных узлов, которые больше нельзя будет использовать и которые называются мусором . Сборщик мусора «на лету» имеет два процесса: саму программу и сборщик мусора, задача которого — идентифицировать мусорные узлы и поместить их в список свободных, чтобы их можно было использовать снова.

Грайс считал, что свободу от помех можно использовать, чтобы доказать правильность оперативного сборщика мусора. С помощью Дейкстры и Хоара он смог провести презентацию в конце Летней школы. результатом чего стала статья в CACM.

E. Проверка решения чтения/записи с помощью семафоров . Куртуа и др. используйте семафоры, чтобы дать две версии проблемы чтения/записи без доказательств. Операции записи блокируют как чтение, так и запись, но операции чтения могут выполняться параллельно. Овицкий предоставляет доказательство.

Алгоритм Ф. Петерсона , решение взаимного исключения двух процессов проблема была опубликована Петерсоном в двухстраничной статье. Шнайдер и Эндрюс предоставляют доказательство правильности.

Зависимости от интерференционной свободы

На изображении ниже, сделанном Ильей Сергеем, показан поток идей, реализованных в логике, связанной с параллелизмом. В основе лежит свобода вмешательства. Файл Семейное древо CSL (PDF) содержит ссылки. Ниже мы суммируем основные достижения.

Historical graph of program logics for interference freedom

• Рели-Гарантия . 1981. Свобода вмешательства не композиционна. Клифф Джонс восстанавливает композиционность путем абстрагирования помех в два новых предиката в спецификации: условие доверия записывает, какое вмешательство должен выдерживать поток, а условие гарантии устанавливает верхнюю границу вмешательства, которое поток может причинить своим родственным потокам. Сюй и др. обратите внимание, что Rely-Guarantee представляет собой новую формулировку свободы вмешательства; По их словам, выявление связи между этими двумя методами дает глубокое понимание верификации программ с общими переменными.
• КСЛ . 2004. Логика разделения поддерживает локальные рассуждения, согласно которым в спецификациях и доказательствах программного компонента упоминается только часть памяти, используемая этим компонентом. Логика параллельного разделения (CSL) была первоначально предложена Питером О'Хирном , Мы цитируем: «метод Овицкого-Гриса предполагает явную проверку невмешательства между компонентами программы, в то время как наша система исключает вмешательство неявным образом, в силу способа построения доказательств».
• Создание параллельных программ . 2005-2007 гг. Фейен и ван Гастерен показать, как использовать Овики-Гриса для разработки параллельных программ, но отсутствие теории прогресса означает, что проекты обусловлены только требованиями безопасности . Донгол, Голдсон, Муидж и Хейс расширили эту работу, включив в нее «логику прогресса», основанную на Чанди и Мисры языке Unity , адаптированную к модели последовательного программирования. Донгель и Голдсон описать логику их прогресса. Гольдсон и Донгол показать, как эта логика используется для улучшения процесса проектирования программ, алгоритма Деккера на примере для двух процессов. Донгол и Муидж представить дополнительные методы создания программ, используя алгоритм взаимного исключения Петерсона в качестве примера . Донгол и Муидж покажите, как уменьшить вычислительные затраты при формальных доказательствах и выводах, и снова выведите алгоритм Деккера, что приведет к некоторым новым и более простым вариантам алгоритма. Муидж изучает правила расчета для связи Unity «отводы к» . Наконец, Донгол и Хейс обеспечить теоретическую основу и доказать правильность логики процесса.
• ОГРА . 2015. Лахав и Вафеиадис усиливают проверку на свободу помех, чтобы создать (цитируем из аннотации) «OGRA, программную логику, которая подходит для рассуждений о программах во фрагменте выпуска-получения модели памяти C11». Они предоставляют несколько примеров его использования, включая реализацию примитивов синхронизации RCU.
• Квантовое программирование . 2018. Ин и др. распространить свободу вмешательства на квантовое программирование. Трудности, с которыми они сталкиваются, включают переплетенный недетерминизм: недетерминизм, включающий квантовые измерения, и недетерминизм, вызванный параллелизмом, происходящим в одно и то же время. Авторы формально проверяют параллельный квантовый алгоритм Брави-Госсета-Кёнига, решающий задачу линейной алгебры, давая, по их словам, впервые безусловное доказательство вычислительного квантового преимущества.
• ПОГ . 2020. Раад и др. представляют POG (Persistent Owicki-Gries), первую программную логику для рассуждений о технологиях энергонезависимой памяти, в частности Intel-x86.

Тексты, в которых обсуждается свобода вмешательства

• О методе мультипрограммирования , 1999. Ван Гастерен и Фейен обсуждают формальную разработку параллельных программ исключительно на идее свободы вмешательства.
• О текущем программировании , 1997. Шнайдер использует свободу помех как основной инструмент при разработке и проверке параллельных программ. Дана связь с темпоральной логикой, поэтому могут быть доказаны произвольные свойства безопасности и живучести. Предикаты управления устраняют необходимость во вспомогательных переменных для расчета программных счетчиков.
• Верификация последовательных и параллельных программ , 1991, 2009. Этот первый текст, посвященный верификации структурированных параллельных программ, написанный Аптом и др ., выдержал несколько изданий за несколько десятилетий.
• Проверка параллелизма: введение в композиционные и некомпозиционные методы , 2112. Де Ровер и др. представляют систематическое и всестороннее введение в композиционные и некомпозиционные методы доказательства для проверки параллельных программ на основе состояний.

Реализация свободы помех

• 1999: Нипков и Ньето представляют первую формализацию свободы интерференции и ее композиционную версию, метод гарантии-полагания, в средстве доказательства теорем: Isabelle/HOL.
• 2005: Докторская диссертация Абрахама предлагает способ доказать правильность многопоточных Java-программ в три этапа: (1) аннотировать программу для создания схемы доказательства, (2) использовать инструмент Verger для автоматического создания условий проверки и (3) использовать теорему прувер PVS для интерактивного доказательства условий проверки.
• 2017: Дениссен сообщает о реализации Овицкого-Гриса на «готовом к проверке» языке программирования Dafny . Дениссен отмечает простоту использования Дафни и его расширения, что делает его чрезвычайно подходящим для обучения студентов свободе от помех. Его простота и интуитивность перевешивают недостаток некомпозиционности. Он перечисляет около двадцати учреждений, которые учат свободе вмешательства.
• 2017: Амани и др. объединяют подходы Hoare-Parallel, формализации Овики-Гриса в Isabelle/HOL для простого языка while, и SIMPL, общего языка, встроенного в Isabelle/HOL, для обеспечения формального обоснования программ на C.
• 2022: Далванди и др. представляют первую среду дедуктивной проверки в Isabelle/HOL для C11-подобных программ со слабой памятью, основанную на кодировании Овицкого-Гриса Нипковом и Ньето в средстве доказательства теорем Изабель.
• 2022: Эта веб-страница описывает верификатор Civl для параллельных программ и дает инструкции по его установке на ваш компьютер. Он построен на основе Boogie, средства проверки последовательных программ. Крагл и др. описать, как в Civl достигается свобода от помех, используя их новую идиому спецификации, давать инварианты . Можно также использовать спецификации в стиле «полагайся-гарантируй». Civl предлагает комбинацию линейной типизации и логики, которая позволяет экономно и локально рассуждать о непересекаемости (например, логика разделения). Civl — первая система, предлагающая уточнение структурированных параллельных программ.
• 2022. Эсен и Рюммер разработали TRICERA, автоматизированный инструмент проверки с открытым исходным кодом для программ на языке C. Он основан на концепции ограниченных предложений Хорна и обрабатывает программы, работающие в куче, с использованием теории куч. Доступен веб-интерфейс для онлайн-тестирования. Для управления параллелизмом TRICERA использует вариант правил доказательства Овики-Гриса с добавлением явных переменных для представления времени и часов.