Аргументы __CPROVER_fence()

Я вижу код вроде __CPROVER_fence("RRfence", "RWfence");используются в таких проектах, как тестирование Linux RCU и оболочки pthread для анализа CBMC. Я просмотрел онлайн-документацию, но не нашел текста в строках, отправленных этой функции CBMC.

Какие параметры доступны для __CPROVER_fence?

Я считаю, что это аннотация / функция для обозначения барьеров / ограждений, выполняемых реальной реализацией. Т.е. это заглушка для анализа реальной функциональности. Очевидно, что параметры обозначают типы барьеров, но я не нашел ссылки на фактические параметры и соответствующие типы барьеров. То есть, "RRFence" - это ограничение чтения, то есть чтение до этой точки завершится перед чтением после этой точки (как предположение).

Источник

1 ответ

Используйте источник Луки.

Все обозначения являются «заборами», чтобы сказать, что какой-то примитив барьера ЦП предотвратил возникновение опасности. Таким образом, все предыдущие «чтение/запись» будут зафиксированы в кеше (или в основном хранилище (память L3) для «кумулятивных» вариантов) перед последующим «чтением/записью». «Функция» может принимать любую комбинацию/перестановку этих значений.

Действительно, как указал user20270 , существует восемь аннотаций, принятых . Подробности см. в Википедии об опасностях , а также в других цитируемых документах.

  • RRFence не представляет особой опасности, но может вызвать каскад событий
  • RWFence, это антизависимость, которая может быть проблематичной для зависимых элементов.
  • WRFence, конкретная опасность, включающая только одну переменную
  • WWFence, опасность вывода может возникнуть только с одной «переменной».
  • WWcumul
  • RRкумул
  • RWкумул
  • WRкумул

Версии 'cumul' аналогичны обычной 'fence' с той лишь разницей, что кеш сбрасывается в основную память (L3). Например, на процессоре ARM dmbИнструкция представляет собой обычную форму «забора», тогда как сброс кэша CP15 является типом «кумулятивного». «Забор» предназначен только для неупорядоченных проблем, таких как конвейер и буферы записи ?, а «кумулятивный» — для когерентности кеша.

Все обозначения являются «заборами», чтобы сказать, что какой-то примитив барьера ЦП предотвратил возникновение опасности. Таким образом, все предыдущие «чтение/запись» будут зафиксированы в основном хранилище (память L3) перед последующим «чтением/записью». «Функция» может принимать любую перестановку этих четырех значений.

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

Страница Software Verification for Weak Memory на CProver является розеттским камнем для этой темы. В основном это относится к инструменту «мушкетер», но дальнейшее чтение покажет, что многие концепции включены в инструмент CBMC. Даже URL-адрес страницы содержит «wmm», который также находится в каталоге «goto-instrument» как «wmm», где реализована эта функция.

  • Документ о слабой памяти - конец раздела 1 (стр. A:5) подробно описывает включение этих моделей в CBMC. Это модели TSO, PSO, RMO и Power. Их можно найти в cbmc/src/goto-instrument/wmm/wmm.h.
  • Software Verification for Weak Memory via Program Transformation описывает исправление для PostgreSQL и инструментарий кода Linux RCU; следовательно, упомянутый проект с открытым исходным кодом, вероятно, произошел от разработчиков слабой памяти CBMC, что дает возможность отсутствия онлайн-документации.

Каталог cbmc-concurrency и ansi-c содержат множество примеров использования CPROVER_fence()и другие примитивы моделирования памяти.

Пример кода проверки C для реализации pthread_mutex_lock()для анализа,

      inline int pthread_mutex_lock(pthread_mutex_t *mutex)
{
  __CPROVER_HIDE:;
  #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
  __CPROVER_assert(__CPROVER_get_must(mutex, "mutex-init"),
                   "mutex must be initialized");

  __CPROVER_assert(!__CPROVER_get_may(mutex, "mutex-destroyed"),
                   "mutex must not be destroyed");

  __CPROVER_assert(__CPROVER_get_must(mutex, "mutex-recursive") ||
                   !__CPROVER_get_may(mutex, "mutex-locked"),
                   "attempt to lock non-recurisive locked mutex");

  __CPROVER_set_must(mutex, "mutex-locked");
  __CPROVER_set_may(mutex, "mutex-locked");

  __CPROVER_assert(*((__CPROVER_mutex_t *)mutex)!=-1,
    "mutex not initialised or destroyed");
  #else
  __CPROVER_atomic_begin();
  __CPROVER_assume(!*((__CPROVER_mutex_t *)mutex));
  *((__CPROVER_mutex_t *)mutex)=1;
  __CPROVER_atomic_end();

  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence",
                  "WWcumul", "RRcumul", "RWcumul", "WRcumul");
  #endif

  return 0; // we never fail
}

Насколько я понимаю, он проверяет,

  • только один замок
  • блокировка инициализируется перед вызовом
  • замок не разрушается во время удержания
  • блокировка не инициализируется повторно во время удержания
  • все слабые элементы памяти упорядочения разрешаются (все кеши сбрасываются) после вызова.

Интересно, man pthread_mutex_lock()ничего не говорит о очистке кеша (включая буферы записи и т. д.). У нас есть инверсия приоритета, мертвая блокировка и т. Д. С программированием мьютекса / блокировки, но также это имеет цену на производительность памяти? Он должен явно сбрасывать все, поскольку мьютекс не привязан к определенному набору переменных. Аналогичный регрессионный тест показывает неудачи pthread_create()где буфер записи может оставить значение в неопределенном состоянии при запуске начального потока, если не вставлен барьер.

Кажется, что эта работа сравнительно недавняя (по некоторым стандартам), с документами, датированными 2013 годом, и фиксацией Linux RCU в 2016 году. Возможно, авторы хотят, чтобы API оставался гибким. Вероятно, они больше сконцентрированы на более приятной задаче проверки пруверов, и у них не было времени документировать этот интерфейс.

Источник
Другие вопросы по тегам