Диссертация (1149932), страница 4
Текст из файла (страница 4)
скомпилированная программа может быть эффективноисполнена на целевом процессоре. Так, модели C/C++11 [4] и Java [3] разработанытаким образом, чтобы обычные операции чтения и записи3 могли быть скомпилированы без вставки барьеров памяти в случае компиляции в платформы x86,Power и ARM.Подобные схемы компиляции будут называться эффективными в рамкахданного исследования.
Соответственно, как было видно из рассмотренных схемкомпиляции из модели SC в модель Power, для этих моделей не существует эффективной компиляции. Очевидно, что для того, чтобы существовала эффективнаясхема компиляции из модели языка программирования в модель целевой платформы, должно выполняться следующее утверждение: модель исходного языкадолжна позволять все сценарии поведения для программы без барьеров, которыепозволяет целевая модель памяти для скомпилированной версии программы, в которой также не используются барьеры. Аналогично требованию на корректностьоптимизаций, наличие эффективной схемы компиляции увеличивает число слабых поведений, допускаемых моделью языка программирования.3Вразделе 1.3.3 будут рассмотрены различные модификаторы, которыми могут быть помечены инструкции работы с памятью в модели C/C++11, и “обычные операции чтения и записи” будут соответствовать атомарным расслабленным и неатомарным инструкциям.
Все инструкции работы с памятью изпримеров программ, приведённых к этому моменту, были “обычными”.191.2.3Гарантии программистуТребование о том, что модель памяти языка программирования должнапредоставлять разумные гарантии программисту звучит крайне неформально. Попробуем сформулировать его более конкретно.Очевидно, что программист должен иметь представление о том, как ведетсясебя программа, над которой он работает, а поведение программы как раз определяется моделью памяти. Как следствие, желательно, чтобы модель памяти быламаксимально простой и понятной, а также существовал формальный инструментарий для рассуждения о программах в рамках модели. Простота — это оченьсубъективный критерий, особенно при сравнении слабых моделей памяти, тогдакак наличие и выразительная сила инструментов анализа может быть использована для более точного сопоставления моделей.Существуют различные методы для анализа программ. Среди них стоит отметить методы проверки моделей (model checking) [45, 46] и верификации по Хоару (Hoare logic) [47].
Оба метода хорошо зарекомендовали себя в приложениик модели SC [48–63]. Существуют также работы, посвященные слабым моделямпамяти [64–69]. В последних отмечается, что если модель памяти разрешает сценарии поведения программ с т.н. “значениями из воздуха” (out-of-thin-air values,OOTA), то класс свойств, которые могут быть проверены или доказаны для программ в рамках таких моделей, существенным образом ограничивается. В частности, модель памяти C/C++11 разрешает такие сценарии.Что же такое “значения из воздуха”? К сожалению, на данный момент несуществует точного определения [5], однако существует набор примеров такихповедений, а также следующий признак наличия “значений из воздуха”. Если всценарии поведения программы, в которой нет арифметических выражений, появляется некоторое значение (например, это значение присваивается переменнойили записывается в память), причём это значение явным образом не фигурируетв тексте программы, то такой сценарий обладает “значениями из воздуха”.Рассмотрим следующую программу LB-OOTA (load buffering, буферизациячтения):[x] := 0; [y] := 0;(LB-OOTA)a := [x]; b := [y];[y] := a[x] := b20В этой программе нет арифметических операций и 0 является единственным значением, которое явным образом встречается в тексте программы.
По приведенному выше признаку любой сценарий поведения этой программы, в результате которого значение переменной a или b отличается от 0, обладает “значениемиз воздуха”. Такие сценарии разрешаются для этой программы в рамках моделиC/C++11 [4].Рассмотрим другую программу, некоторые сценарии поведения которой врамках модели C/C++11 также считаются [5] обладающими “значениями из воздуха”, но не подпадающую под сформулированный выше признак:[x] := 0; [y] := 0;a := [x];b := [y];if aif bthen [y] := 1then [x] := 1else skipelse skipfifi(IF-OOTA)Казалось бы, что единственным результатом исполнения этой программы можетбыть [a = 0, b = 0], но модель C/C++11 также разрешает [a = 1, b = 1].Сценарии поведения со “значениями из воздуха” всегда имеют некоторуюциклическую зависимость между встречаюшимися в них значениями. Как следствие, они не проявляются на современных процессорах4 и не могут быть получены как результат разумной оптимизации.
То, что некоторые модели разрешаюттакие сценарии, обычно является результатом того, что в рамках подхода, выбранного для задания модели, тяжело или невозможно запретить “значения из воздуха” и, при этом, не запретить нужные оптимизации [71].1.3Существующие модели памяти языков программированияСреди моделей памяти, разработанных для языков программирования, естькак используемые на практике, т.е. являющиеся частями стандартов языков [30,31, 72, 73], так и теоретические [1, 35–39]. Далее в этом разделе обсуждаются модели памяти языков Javа [73] и C/C++ [30,31], выделяются их достоинства и недостатки, а также рассматривается, как упомянутые недостатки решаются в существующих теоретических моделях.4 Сценарииповедения со “значениями из воздуха” проявляются на процессорах семейства DECAlpha [70], но данная архитектура снята с производства.211.3.1Виды моделей памятиНа данный момент существует два основных подхода к описанию моделейпамяти — аксиоматический (декларативный) и операционный, которые в некоторых работах смешиваются.
Аксиоматические модели памяти представляют сценарии поведения программ в виде графов, которые должны соответствовать определенным аксиомам. Модели памяти Java и C/C++, описанные ниже, являютсяпримерами аксиоматических моделей. Преимуществами аксиоматических моделей является относительная простота для задания глобальных свойств сценарияповедения программы, таких как наличие некоторого тотального порядка над подмножестве событий (вершин графа) определенного вида.
Также аксиоматическиемодели проще для представления в логических языках, таких как Alloy [74] иRosette [75, 76], что используется для автоматического сравнения моделей [77] игенерации моделей по набору примеров [78].Сценарий поведения в рамках операционных моделей представляется каксерия переходов некоторой абстрактной машины. Преимуществом таких моделей является то, что они дают представление об исполнении программы. Какследствие, между моделью памяти, которая обычно определяет поведение только подмножества языка, связанное с его многопоточной компонентой, и описанием остальных конструкций языка имеется прослеживаемая связь, которую нужно дополнительно устанавливать для аксиоматических моделей [79].
Также длябольшинства операционных моделей возможно разработать интерпретатор, чтопозволяет пошагово отлаживать многопоточные алгоритмы.1.3.2Модель памяти JavaВпервые модель памяти для языка Java была представлена в стандарте 1996года [72]. Эта модель обладала рядом фундаментальных недостатков [80,81] и была заменена на новую модель [3], которая дальше будет упоминаться как модельпамяти Java, или JMM (Java memory model). Основной задачей при разработкеJMM было разработать модель без “значения из воздуха”, но разрешить базовыекомпиляторные оптимизации. К сожалению, JMM не удовлетворяет последнемутребованию [44]: в рамках JMM некорректными являются оптимизации удаление чтения после чтения (redundant read after read elimination), удаление чтенияпосле записи (redundant read after write elimination), удаление записи после чте-22ния (redundant write after read elimination), добавление неиспользуемого чтения(irrelevant read introduction) и другие.Сценарий поведения программы в JMM представляется как граф, в которомвершинами являются события (actions, events), происходящие в памяти, а помеченными ребрами — отношения на событиях.
События бывают нескольких типов,из которых основными являются: чтение, запись, захват замка (lock), высвобождение замка (unlock). События чтения и записи, в свою очередь, бывают обычные(non-volatile) и синхронизирующие (volatile). Первые действуют на обычных локациях в памяти (переменных), тогда как синхронизирующие – на изменчивых(volatile) локациях. Изменчивые локации выделены как локации, посредством которых происходит синхронизация.Отметим пять отношений, используемых в сценариях поведения JMM.
Первое отношение, программный порядок (program order, po), для каждого потокаявляется тотальным порядком на событиях, относящихся к этому потоку. Второе отношение, “читает из” (reads from, rf), связывает событие записи с читающими из него событиями. Третье отношение, синхронизационный порядок(synchronization order, so), является тотальным порядком на синхронизирующихсобытиях и событиях захвата и высвобождения замков; оно должно быть согласовано с отношениями po и rf на синхронизирующих событиях. Четвёртое отношение, “синхронизируется с” (synchronizes-with, sw), связывает события a и b, еслиrf связывает a и b и эти события действуют над изменчивой локацией, или еслиони связаны с помощью so и a является высвобождением некоторого замка, а b— захватом этого же замка. Пятое отношение, “предшествует” (happens-before,hb), является транзитивным замыканием объединения отношений po и sw; именно это отношение определяет порядок на событиях из определения 1 для JMM.Сценарий поведения в JMM считается корректным, если для него выполняются аксиомы модели.
Одной из аксиом является то, что событие чтения неможет читать из события записи, если они связаны отношением hb и существуетсобытие записи в ту же локацию, которое находится между ними в отношении hb.Формально это можно выразить следующим образом:∀r, w. rf(w, r) ∧ hb(w, r) ⇏ ∃w′ . loc(w) = loc(w′ ) ∧ hb(w, w′ ) ∧ hb(w′ , r),где loc — это функция, которая по событию возвращает локацию, над которойсобытие оперирует. В силу этой аксиомы JMM запрещает результат [a = 1, b = 0]23q : Wvolatile (y,0)p : W(x,0)r : W(x,1)rft : Rvolatile (y,1)s : Wvolatile (y,1)swu : R(x,0)Рис.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
