О конформности Си-программ Михаил Посыпкин ИСП РАН

Содержание доклада Понятие конформности Си-программы. Причины нарушения конформности. Недетерминизм выражений языка Си. Операционная семантика Си по Норришу. Теорема о детерминизме выражений в языке Си. Открытые проблемы, связанные с детерминизмом выражений.

Стандарт Си JTC1/SC22/WG14 N794 Programming languages - C Стандарт Си определяет семантику программ с точностью до некоторых параметров, которые могут задаваться реализацией (implementation-defined) или вообще не быть специфицированы - допускается любой вариант (unspecified). Пример определяемого реализацией параметра: размер типа в байтах. Пример неспецифицированного параметра: порядок вычисления операндов бинарной операции.

Конформная реализация Реализация, которая соответствует всем однозначно определенным в стандарте параметрам. компилятор + система поддержки времени выполнения + аппаратное обеспечение – пример конформной реализации

Строго-конформная программа Программа называется строго конформной, если ее наблюдаемое поведение не зависит от параметров, определяемых реализацией, неспецифицированных или неопределенных. Строго конформная программа одинаково выполняется любой конформной реализацией. Таким образом строго- конформная программа является максимально переносимой.

Причины нарушения строгой- конформности Зависимость от параметров, определяемых реализацией. Зависимость от неспецифицированных параметров. Неопределенное поведение.

Зависимость от параметров, определяемых реализацией Ошибочный (отсутствие переносимости) цикл: int a, b, i; unsigned char *p, *q; p = (unsigned char*)&a; q = (unsigned char*)&b; for(i = 0; i < 4; i ++) q[i] = p[i]; Корректный цикл: for(i = 0; i < sizeof(int); i ++) q[i] = p[i];

Неопределенное поведение Неопределенное поведение означает, что любое поведение является допустимым. Примеры: операции с указателями на неинициализированную память деление на 0 выход значения выражения за границы типа

Недетерминированная семантика выражений в языке Си порядок вычисления операндов арифметических бинарных операций не определен порядок вычисления аргументов при вызове функций не определен порядок вступления в силу побочных эффектов частично определен

Примеры (x = 1) + (y = 2) (x = 1) + (x = 2) f() + g() fg

Последовательная точка Последовательная точка – это такое состояние выполнения программы, при котором все порожденные ранее побочные эффекты должны реализоваться. К последовательным точкам относятся: конец «полного» выражения (выражение в операторе выражения, инициализаторе, условии операторов, влияющих на поток управления, операторе return) после первого операнда в операциях && || :?,

Примеры (x = 1), (y = 2) (x = 1), (x = 2) f() && g() f g f == 0

Корректность обращения к памяти Между предыдущей и последующей последовательными точками значение любого объекта должно изменяться не более одного раза. Значение изменяемого объекта может считываться только для определения сохраняемого значения.

Эффект последовательной точки x + ((x = 3), 4) x +, = x 3 4 x +, = x 3 4 undef7

Присваивание x = x + 1; = + x1 x

Формальная модель последовательной точки Informative Annex D. C99 Standard (Clive Feather) Операциям доступа к памяти и последовательным точкам ставятся в соответствия события. На основе дерева абстрактного синтаксиса устанавливается частичный порядок на множестве событий. Если существует полный порядок на множестве событий, в котором существует чтение после записи либо запись после записи по одному и тому же адресу, то поведение не определено.

Пример Выражение: (x=y) + x; События: {1:R y} {2:W x} {3:R x} Частичный порядок: {1} < {2} Возможные полные порядки: {1} {2} {3} {1} {3} {2} {3} {1} {2}

Недостатки модели C. Feather В случае вызовов функций анализ будет слишком сложным Требуются значения конкретных адресов => требуется произвести вычисление => не очевидно, что при измененном порядке событий значения сохранятся

Динамическая семантика выражений языка Си по Норришу набор условий SOS – структурная операционная семантика (Plotkin)

Состояние программы

Недетерминизм в вычислении выражений

Побочный эффект

Пример правила для последовательной точки

Теорема о детерминизме Си- выражений Теорема (Norrish) Если выражение не содержит операций последовательной точки, то результат его вычисления однозначно определен.

Эффект последовательной точки x + ((x = 3), 4) x +, = x 3 4 x +, = x 3 4 undef7

Неопределенное поведение в выражениях с последовательной точкой Результатом выражения является неопределенное поведение, если хотя бы один из возможных путей выполнения приводит к неопределенному поведению. Гипотеза. Результат вычисления однозначно определен?

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

Конфлюентность * * * * * * локальная конфлюентность конфлюентность Для отношений с конечными цепями (Newman 1942)

Конфлюентность влечет детерминизм * * ** конечное

Корректное завершение e e * E * * A Свойство коммутативности (только для корректных выражений)

Корректное завершение A Свойство локальной конфлюентности для применения побочного эффекта A A ** A

Корректное завершение E Свойство локальной конфлюентности для арифметических редукций E E ** E

Корректное завершение коммутативность и конфлюентность

Некорректное завершение Теорема. Если хотя бы при одном вычислении появляется неопределенное поведение, то оно рано или поздно появляется и при любом другом вычислении. * * *

Открытые вопросы Уточнение формальной модели последовательной точки Доказательство или опровержение теоремы о детерминизме любых выражений в языке Си (возможно в упрощенном варианте) Статическая проверка достаточных условий неопределенного поведения

Спасибо за внимание