Здравствуйте, WolfHound, Вы писали:

WH>Всё что находится внутри requires, ensures и invariant работает исключительно на этапе компиляции и на результирующий код не влияет.

У формальной верификации есть одна небольшая, но очень противная особенность, из-за которой она и не получила должного распространения в настоящее время.

Для того, чтобы описать модель алгоритма сортировки, относительно которой будет верифицироваться его реализация, достаточно нескольких примитивно-рекурсивных функций. Однако же, в реальном мире, имеет место интерес к верификации, скажем, реализаций таких протоколов, как TLS или HTTP. Которые, для описания инвариантнов множества некоторых их состояний, потребуют использования частично-рекурсивных функций. То есть, для описания которых, потребуется полный по Тьюрингу язык.

И возникает справедливый вопрос: как в этом случае верифицировать корректность самой модели?

Здравствуйте, Pavel Dvorkin, Вы писали:

PD>что сделали бы по-другому ?

Изменил бы ориентацию Тьюрингу.

Здравствуйте, kochetkov.vladimir, Вы писали:

KV>Для того, чтобы описать модель алгоритма сортировки, относительно которой будет верифицироваться его реализация, достаточно нескольких примитивно-рекурсивных функций.
Покажи в каком месте моего кода находится эта модель?

KV>Однако же, в реальном мире, имеет место интерес к верификации, скажем, реализаций таких протоколов, как TLS или HTTP. Которые, для описания инвариантнов множества некоторых их состояний, потребуют использования частично-рекурсивных функций. То есть, для описания которых, потребуется полный по Тьюрингу язык.
Я не знаю ничего про TLS, но HTTP это же почти регулярный язык.
Из того что там не регулярное:
1)Прочитать число и считать количество байт равное этому числу.
2)Прочитать строку и считать всё до того места где эта строка вновь встретится.
Или я про что-то забыл?

KV>И возникает справедливый вопрос: как в этом случае верифицировать корректность самой модели?
Вот предикаты, которым должны соответствовать все сортировки. Верифицировать их нужно глазами. Благо они очень простые.

//Предикат который утверждает что отрезок [begin..end) отсортирован.
predicate SortedRange(a : array<int>, begin : int, end : int) 
  requires a != null;
  requires 0 <= begin <= end <= a.Length;
  reads a;
{
  forall i, j :: begin <= i < j < end ==> a[i] <= a[j]
}

//Предикат который утверждает что функция переставляет местами элементы массива [begin..end)
//и не меняет остальной массив
predicate PremutateRange(a : seq<int>, b : seq<int>, begin : int, end : int)
  requires |a| == |b|;
  requires 0 <= begin <= end <= |a|;
{
  (forall i :: 0 <= i < begin && end <= i < |a| ==> a[i] == b[i]) && 
  multiset(a[begin..end]) == multiset(b[begin..end]) &&
  multiset(a) == multiset(b) &&
  a[0..begin] == b[0..begin] && a[end..|a|] == b[end..|a|]
}

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

Здравствуйте, WolfHound, Вы писали:
WH>Ну и на практике нам нужно верифицировать не всё, а только некоторые свойства программы. Такие как не выход за приделы массива.
WH>А эта задача легко решается добавлением простейшего предиката индексеру массива.
Да, тут уже многие неявно начинают подменять верификацию type safety (которая, в частности, и гарантирует уважение к разделению прав доступа между процессами) на доказательство формальной корректности.

Сейчас, с точки зрения meltdown, интереснее возможность автоматически детектировать малварь, которая пользуется артефактами кэширования.
Ну, то есть мы выполняем заведомо запрещённое чтение, и пользуемся тем, что branch predictor считает срабатывание guard-а на i<Length маловероятным. Поэтому он там в конвеере уже обратился а a[i] и даже прочёл sampledata[a[i]], и только потом вылетел с IndexOutOfRangeException.
В общем, нам страшен только тот код, который после этого занимается замером производительности доступа к sampledata[].
1. Можно ли предотвратить такое вообще при помощи формальных методов детектирования?
2. Если нет — то будет ли угроза велика? Т.е. может ли злонамеренный код извлечь пользу из прочитанных таким образом данных?
У нас же нет возможности фиксировать адреса — пёс его знает, где рантайм расположит наш массив a; и где относительно него будут расположены данные чужих процессов.
Или мы просто будем сканировать память в надежде найти что-то типа номера кредитки, зная характерный формат данных?

Здравствуйте, Sinclair, Вы писали:

S>Сейчас, с точки зрения meltdown, интереснее возможность автоматически детектировать малварь, которая пользуется артефактами кэширования.
Проблема с атакой через побочный канал в том, что не понятно, как их формализовать.
И совсем не ясно что делать с атаками, о которых мы не знаем.

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

S>1. Можно ли предотвратить такое вообще при помощи формальных методов детектирования?
Насчёт формальных методов не знаю.
Но я думаю можно загрубить таймер. Если таймер будет тикать в 10 раз медленнее чем промах кеша, то мы не сможем извлечь информацию через этот канал. И этого должно быть достаточно для работы со звуком и видео.

S>2. Если нет — то будет ли угроза велика? Т.е. может ли злонамеренный код извлечь пользу из прочитанных таким образом данных?
S>У нас же нет возможности фиксировать адреса — пёс его знает, где рантайм расположит наш массив a; и где относительно него будут расположены данные чужих процессов.
Если мы будем размещать данные в случайном месте 64х битного адресного пространства, то крайне маловероятно что что-то можно будет найти.

S>Или мы просто будем сканировать память в надежде найти что-то типа номера кредитки, зная характерный формат данных?
Это возможно. Но весьма хлопотно.

Здравствуйте, WolfHound, Вы писали:

WH>Покажи в каком месте моего кода находится эта модель?

Её и не должно быть в коде. Инварианты и пред-/пост-условия, используемые в рамках формальной верификации, всегда описывают свойства некоторой подразумеваемой эталонной модели предметной области, относительно которой осуществляется верификация. В простейших случаях, типа сортировки, в явном построении этой модели нет необходимости, т.к. её свойства формулируются интуитивно. Если же говорить о верификации реальных систем, то там без построения такой модели обойтись не получится. Например, для верификации компилятора какого-либо языка, необходимо формальное описание, как грамматики языка, так и его семантики: денотационной -- для верификации компилятора относительно матмодели языка, интерпретационной -- для верификации кодогенератора, трансформационной -- для верификации средств метапрограммирования или транскомпиляции и т.п. Всё это вместе и составляет первую часть той модели, о которой я говорил.

WH>Я не знаю ничего про TLS, но HTTP это же почти регулярный язык.
WH>Из того что там не регулярное:
WH>1)Прочитать число и считать количество байт равное этому числу.

И это уже делает HTTP контекстно-зависимым языком (см. https://pdfs.semanticscholar.org/7d95/6ddef192f3a10b22bc41044566be396c751f.pdf, п3.3), для разбора которого требуется LBA, суть -- машина Тьюринга с ограниченной памятью.

WH>Вот предикаты, которым должны соответствовать все сортировки. Верифицировать их нужно глазами. Благо они очень простые.

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

WH>//Предикат который утверждает что функция переставляет местами элементы массива [begin..end)
WH>//и не меняет остальной массив

И вот тут мы приходим ко второй части модели. Если опираться на определение понятия алгоритма из теории формальных языков (т.е. что всякий алгоритм является распознавателем какого-либо формального языка), то первая часть лишь доказывает, что верифицируемый алгоритм распознаёт полное множество слов, принадлежащих некоторому языку. Но нам также надо ещё и доказать, что этот же алгоритм не распознаёт слова, принадлежащие дополнению данного языка. Дополнение КЗ-языка является КЗ-языком -> ещё одна МТ с ограниченной памятью, отсутствие которой нужно доказать. А доказать отсутствие чего-либо в общем случае "гораздо труднее", чем наличие

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

Для верификации криптографии, кстати, на практике используются специально заточенные под эту задачу DSL'и. Такие, как https://github.com/GaloisInc/cryptol, например. Просто потому, что описать даже примитивные криптоалгоритмы традиционными средствами верификации невероятно тяжело. И это при том, что за любым таким алгоритмом стоит совершенно строгая формальная модель. Что касается прочих классов уязвимостей, то частичные модели на данный момент, построены только для инъекций, некоторых подклассов атак повреждения памяти и гонок за ресурсами. Для всех остальных классов моделей нет, а значит и нет возможности верифицировать код на предмет их отсутствия.

WH>Ну и на практике нам нужно верифицировать не всё, а только некоторые свойства программы. Такие как не выход за приделы массива.

Уязвимость -- есть множество достижимых состояний приложения (конфигураций в терминологии Тьюринга), в которых для любого информационного потока нарушается любое из свойств защищённости (в общепринятой модели угроз это -- конфиденциальность, доступность, целостность, авторизованность и аутентичность). Для того, чтобы доказать безопасность приложения средствами частичной формальной верификации (т.е. когда верифицируется не всё), мы должны помимо всего прочего ещё и доказать, что верификация покрывает всё множество таких состояний. Не буду утверждать, что это неразрешимая проблема (хотя, IMO, так оно и есть), но вот то, что известных способов её решения на данный момент не существует -- совершенно точно.

Кстати, если найдётся время, могу порекомендовать доклад с нашей прошлой конфы на тему формальной верификации: https://www.youtube.com/watch?v=gKEOzRm7aaw&amp;feature=youtu.be Денис занимается верификацией компонентов ядра Linux в ИСП РАН для сами-догадаетесь-какого дистрибутива и с предметной областью знаком не понаслышке. Во второй части доклада как раз рассматриваются основные проблемы и ограничения формальной верификации (как связанных именно со спецификой С-кода, так и в общем).

Здравствуйте, kochetkov.vladimir, Вы писали:

Я тут говорил про верификацию safety. Ты же расширил тему на верификацию вообще всего. И ещё security притянул о которой речи вообще не шло.
При этом нужно всегда помнить, что без safety о security разговор можно даже не начинать.
И safety сама по себе является очень полезной штукой даже без security.

KV>Её и не должно быть в коде. ... Всё это вместе и составляет первую часть той модели, о которой я говорил.
К счастью для того о чём говорю я это всё не нужно.

KV>И это уже делает HTTP контекстно-зависимым языком (см. https://pdfs.semanticscholar.org/7d95/6ddef192f3a10b22bc41044566be396c751f.pdf, п3.3), для разбора которого требуется LBA, суть -- машина Тьюринга с ограниченной памятью.
Как это мешает верифицировать две простейшие функции?
Тут же всё намного проще чем сортировка.

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

KV>Для верификации криптографии, кстати, на практике используются специально заточенные под эту задачу DSL'и. Такие, как https://github.com/GaloisInc/cryptol, например. Просто потому, что описать даже примитивные криптоалгоритмы традиционными средствами верификации невероятно тяжело.
Я посмотрел по диагонали. Но ничего необычного кроме манипуляции последовательностями бит там не увидел.
Прямая поддержка этой фичи действительно сильно упрощает жизнь. Причём не только верификатору, но разработчикам алгоритмов. И потенциально из этого описания можно генерировать очень быстрый код.

Здравствуйте, WolfHound, Вы писали:

WH>В принципе я могу себе представить возможность закрыть некоторые классы атак через побочный канал если создавать железо и компилятор, заточенные на это.
WH>Но у таких систем будет относительно низкая производительность и относительно высокое энергопотребление.
Не, это не интересно.
S>>1. Можно ли предотвратить такое вообще при помощи формальных методов детектирования?
WH>Насчёт формальных методов не знаю.
WH>Но я думаю можно загрубить таймер.
Ну, как вариант. Но тоже — микроскопом по яйцам. Хочется чего-то гламурненького, хотя нутром чую, что невозможно это.
Скорее придётся отказаться от адресной арифметики вообще. Или как-то ещё гарантировать, что мы в принципе никогда не исполняем код типа

if(i<=a.Len)
  throw;
s+=a[i];// на самом деле к моменту throw операция уже выполнена и исказила кэш.

Варианты, которые я вижу:

• переписать guard как-то так:
  

    div ebx
    test eax, eax
    jnz out_of_range_handler 
    mov eax, myArray[edx] // в случае выхода за пределы мы сюда не попадём; но даже спекулятивный исполнитель полезет в адреса в пределах разрешённого нам блока

Да, это немношк удорожает проверки; но надо стремиться к устранению таких проверок на уровне JIT, чтобы в большинстве мест косвенный доступ был статически проверен.
WH>Если мы будем размещать данные в случайном месте 64х битного адресного пространства, то крайне маловероятно что что-то можно будет найти.
Ну вот как раз интересно — в той же Singularity есть ли какая-то доля статически размещённых данных?
Опасна ли она? Ну, то есть можно ли при её чтении пройти по цепочке — типа "в нулевой странице у нас всегда лежит ядро верификатора, в первой — код джита, в 56 у нас обычно попадает головная страница сессии ОС, а в ней по смещению 408 лежит указатель на структуру user, в которой восьмое поле — это ссылка на пароль в UTF-8"


S>>Или мы просто будем сканировать память в надежде найти что-то типа номера кредитки, зная характерный формат данных?
WH>Это возможно. Но весьма хлопотно.

Здравствуйте, Sinclair, Вы писали:

WH>>В принципе я могу себе представить возможность закрыть некоторые классы атак через побочный канал если создавать железо и компилятор, заточенные на это.
WH>>Но у таких систем будет относительно низкая производительность и относительно высокое энергопотребление.
S>Не, это не интересно.
А как по мне весьма интересно.
Если сделать специализированный крипточип который выполняет все команды за одинаковое время, все команды потребляют одинаковое количество энергии и компилятор доказал, что функция всегда выполняет одно и то же количество команд вне зависимости от данных.
То атаки через измерение времени исполнения и измерение потребления энергии отпадут.
Разумеется, этот чип будет исполнять исключительно криптографию.
Причём после того как мы получим симметричный сессионный ключ алгоритм шифрования канала передачи данных можно исполнять уже на обычном железе.

S>Ну, как вариант. Но тоже — микроскопом по яйцам. Хочется чего-то гламурненького, хотя нутром чую, что невозможно это.
Можно наконец начать доказывать процессоры.
Чтобы такое не повторилось.
Правда может найтись неожиданный вектор атаки через побочный канал.

S>Скорее придётся отказаться от адресной арифметики вообще.
Это невозможно. Её можно без потерь убрать из прикладного кода, но на уровне реализации без неё никуда.

S>Варианты, которые я вижу:
S>

S>
• переписать guard как-то так:
  S>

  S>  div ebx
  S>  test eax, eax
  S>  jnz out_of_range_handler 
  S>  mov eax, myArray[edx] // в случае выхода за пределы мы сюда не попадём; но даже спекулятивный исполнитель полезет в адреса в пределах разрешённого нам блока
  S>

  
  S>

S>Да, это немношк удорожает проверки; но надо стремиться к устранению таких проверок на уровне JIT, чтобы в большинстве мест косвенный доступ был статически проверен.
Я ничего не понял. Как это поможет исправить проблему с meltdown?

S>Ну вот как раз интересно — в той же Singularity есть ли какая-то доля статически размещённых данных?
Не знаю.
Но ничего не мешает при загрузке системы размещать данные по случайному адресу.
После чего обнулять загрузчик.

Здравствуйте, WolfHound, Вы писали:

WH>Я ничего не понял. Как это поможет исправить проблему с meltdown?
Это я туплю. У нас уже заполночь

Здравствуйте, MTD, Вы писали:

Знаешь, что такое типографские пункты?
Примерно то же, что и миллиметры, только меньше. Не помогает...

Здравствуйте, WolfHound, Вы писали:

WH>Я ничего не понял. Как это поможет исправить проблему с meltdown?
Основная идея — предотвратить попадание в конвеер кода, который обращается по невалидному указателю.
Как у нас выглядит meltdown?
Главный код — это обращение по адресу, который получается из разыменования злого указателя:

сhar tmp = *kernel_space_ptr;
char not_used = userspace_array[tmp * 4096];

Он построен на том, что разыменование указателя и чтение по нему выполняются до того, как будет проверена доступность страницы по *badPtr и брошено исключение.
После этого мы типа спокойно проверяем скорости доступа к разным частям userspace_array[].
В управляемой верифицируемой платформе понятия "указатель" нету, мы не можем разыменовать 0xBAADF00D.
Но есть массивы и ссылки.
Поэтому можно запилить аналог meltdown:

int i = 0xBAADFOOD;
var myData = new char[1];
var tmp = myData[i]; //выходим далеко за пределы массива
char not_used = userspace_array[tmp * 4096];

Ну, такой код не пройдёт ни компиляцию, ни верификацию — нам придётся пошаманить с i, чтобы компилятор думал, что есть хотя бы шанс уложиться внутрь myData.
Тогда верификатор потребует воткнуть проверку:

int i = 0xBAADFOOD;
...//Запутываем компилятор с верификатором
var myData = new char[1];
if(i>myData.Length) throw new IndexOutOfRangeException(); // без этой проверки верификатор не пропустит следующую строку
var tmp = myData[i]; //выходим далеко за пределы массива
char not_used = userspace_array[tmp * 4096];

Здесь у нас утечка ровно потому, что branch prediction успеет прочитать в not_used ещё до того, как выполнится проверка (чтобы гарантировать это, придётся написать чуть больше кода, но там ничего сложного нет).
То есть, в конвеере есть код, который прибавляет к myData значение, которое больше его длины.
Если мы заменим банальное сравнение на вычисление остатка, то уязвимость исчезнет:

int i = 0xBAADFOOD;
...//Запутываем компилятор с верификатором
var myData = new char[1];
if(i>myData.Length) // без этой проверки верификатор не пропустит следующую строку
  throw new IndexOutOfRangeException(); 
else
  i = i % myData.Length // на позитивном пути мы принудительно ограничиваем индекс
var tmp = myData[i]; //выходим далеко за пределы массива
char not_used = userspace_array[tmp * 4096];

Всё. В таком коде в конвеере никогда нет чтений за пределами массива, даже если i "пытается" за них выйти. Собсно, всё вшивается в реализацию джитом инструкции ldelem. Устранение избыточных проверок возлагаем на jit.

Pzz>А бывают некогерентные, но при этом с SMP? Если да, как у них в user space программируют?

Я не уверен здесь в терминологии. Просто несколько идентичных процессоров с собственными некогерентными кешами? Такое бывает. Например в SoC с которым сейчас работаю. Только там нет user-space. Программировать неудобно, и используется такая схема вынужденно — те процессоры которые влазят в бюджет по транзисторам не имеют когерентного кеша.
У нас это отдельные фирмваре, собирающиеся из обших исходников, общающиеся через память и железные фифо, в принципе очень похоже на общение разные процессов в нормальной ОС.

Здравствуйте, _wqwa, Вы писали:

_>Знаешь, что такое типографские пункты?

В отличии от тебя, знаю не только про пункты, интерлиньяж и т.п., а еще и про кодировки юникода

Здравствуйте, gardener, Вы писали:

G>Я не уверен здесь в терминологии. Просто несколько идентичных процессоров с собственными некогерентными кешами? Такое бывает. Например в SoC с которым сейчас работаю. Только там нет user-space. Программировать неудобно, и используется такая схема вынужденно — те процессоры которые влазят в бюджет по транзисторам не имеют когерентного кеша.

Я интересуюсь потому, что традиционные поточные API (напр., POSIX threads, C++ threads) просто не содержат необходимых операций, чтобы программировать компутер с некогерентным кэшом. Там не предусмотрено способа сказать процессору "сбрось кэш в таком-то месте" или "перечитай из памяти в таком-то месте".

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

Поэтому мне любопытно, если такое чудо существует, интересно, как люди на нем живут.

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

Pzz>В ядре или на самодельной железке с собственной средой программирования такой проблемы нет, потому что и операции нужные, скорее всего, предусмотрены, и legacy кода нет.

Достаточно просто должно быть запустить на разных процессорах отдельные экземпляры ОС (тот же Linux) и отдельные процессы. Общаться между собой наверное всеми механизмами, которые подразумевают обмен сообщениями (пайпс например). Общую память тоже не сложно сделать — mmap() требует MMU — здесь маппинг будет некешируемый. Модификация какая-то в кернеле потребуется само собой, но не очень много.

Потом например в Linux был (может и сейчас есть) сacheflush() system call, я его когда-то на MIPS использовал.

Насчет отдельных экземпляров. Если не путаю в MQX RTOS есть такая возможность. Экземпляры, обмен сообщениями.

N>Не-а. Он и за прошедшие 20 лет не решил эти проблемы, и не решил бы их и тогда.
N>Проблемы Itanium в том, что EPIC не работает с современной памятью и кэшами в мультипроцессорной системе.

А можно больше деталей?

Здравствуйте, gardener, Вы писали:

N>>Не-а. Он и за прошедшие 20 лет не решил эти проблемы, и не решил бы их и тогда.
N>>Проблемы Itanium в том, что EPIC не работает с современной памятью и кэшами в мультипроцессорной системе.

G>А можно больше деталей?

Можно.

Пусть у вас последовательность команд. Какая-то часть из них кодирует операции только с регистрами — считаем, они доступны всегда, и на чтение и на запись. Какая-то обращается к памяти. Вот тут начинаются проблемы. Если у вас обыкновенная DRAM, у неё самая длительная операция это закрыть неактуальную строку (переписать из её кэша, который в самой микросхеме DRAM, в собственно DRAM-часть) и открыть заказанную (прочитать и переписать в тот кэш на борту DRAM). Эта операция занимает, согласно вики на DDR4, минимум 37.5 нс. (DDR3 и выше — в таймингах типа 10-10-10 сложить все 3 числа и подсчитать в тактах в clock rate (не путать с data rate).) В более бюджетных — и выше. Умножьте это на частоту процессора в гигагерцах и получите количество его тактов, сколько он ждёт. А ещё надо добавить время на опознание, что данных нет ни в одном локальном кэше (обычно добавляется где-то до 30 тактов), нет ни у одного партнёра по SMP (может быть и ~50 тактов) и на чтение полной строки (64 байта на x86) из DRAM (ну, ещё десятка два тактов, там высокая параллельность) — спокойно можно добрать и до 300 тактов.
Это чрезвычайно высокая цифра, даже если сравнивать с супердорогими арифметическими операциями типа целочисленного деления (128/64 на x86, считается, до 90 тактов).

Теперь представим себе исполнение этих команд команд. На x86 вполне может быть, что пока 30-я по счёту только-только прочиталась из памяти, 25-я раскодирована, 20-й назначили все внутренние регистры и она ждёт выполнения, 15-я выполняется, 10-я закончила и результаты готовы, но ждёт, пока предыдущие завершат операции, результат 7-й сидит во write queue на выходе в кэш, для 5-й заканчивают синхронизацию между кэшами в SMP, 1-я наконец всё типа закончила (слила результат в кэш в строку, которая эксклюзивно принадлежит на запись текущему ядру). В это время 2-я задумчиво занимается делением, и её результаты будут ещё тактов через 40. Но она (2-я) пишет в регистр, поэтому не тормозит заметную остальных; её результаты будут применены только к 15-й команде, а результаты той — только к 24-й, поэтому с остальными можно работать. Я не преувеличиваю в цифрах — у Skylake, например, цепочка от "наконец заканчиваем, фиксируем результаты" до "выбрали, начинаем декодировать" может быть до 224 микроопераций.
Процессор сам вычисляет, какая команда от какой зависит. Есть очевидные зависимости по регистрам (типа, если 3-я записала в eax, а 5-я его читает, 5-я должна выполняться после 3-й). Есть зависимости по памяти (x86 настаивает на том, что все операции записи в память упорядочены по этим действиям записи — хотя вычисления в них не требуют такой зависимости). Получается такой себе DAG (направленный ациклический граф) исполнений, внутри которого заметная свобода.

А теперь чем отличается EPIC? Само название поясняет: Explicitly parallel instruction computing. Параллельность рассчитана на этапе написания машинного кода (обычно — компилятором). Причём не в терминах "данная команда хочет результаты той, что на 15 раньше по цепочке" — такое бы требовало слишком много места для записи — а в виде группировок типа "данные команды друг на друга не влияют" (см. ниже), "можно параллелить сколько угодно по вкусу" и "а вот тут мы знаем явную зависимость, надо завершить все предыдущие до всех последующих". В доке по Itanium это выглядит так:

>> An instruction group is a sequence of instructions starting at a given bundle address and slot number and including all instructions at sequentially increasing slot numbers and bundle addresses up to the first stop, taken branch, Break Instruction fault due to a break.b, or Illegal Operation fault due to a Reserved or Reserved if PR[qp] is one encoding in the B-type opcode space. For the instructions in an instruction group to have well-defined behavior, they must meet the ordering and dependency requirements described below.

и вот главные слова — "must meet the ordering and dependency requirements". Автору машкода надо явно определить группы, в которых взаимовлияние минимизировано, и зафиксировать их. Дальше в доке много страшных слов, но вот одни из ключевых:

>> Between instruction groups, every instruction in a given instruction group will behave as though its read occurred after the update of all the instructions from the previous instruction group.

Процессор не имеет права посчитать, что какая-то команда из IG1 может быть выполнена одновременно с какой-то последующей IG2, если между ними стоит явный stop. Даже прочесть данные из памяти в регистр — потому что это называется update of architectural state. Память тормозит? Жди.

>> Within an instruction group, every instruction will behave as though its read of the register state occurred before the update of the register state by any instruction (prior or later) in that instruction group, except as noted in the Register dependencies and Memory dependencies described below.
[...]
>> Register dependencies: Within an instruction group, read-after-write (RAW) and write-after-write (WAW) register dependencies are not allowed (except пара незначительных исключений)

А это, наоборот, в одной группе не может быть зависимостей (как уже сказал — надо отбирать только независимые действия). Хотел исхитриться и применить результаты чтения сразу же? Обломись, бабка, мы на корабле.

Дальше в доке много чего — 100500 поправок, уточнений и исключений, словно специально, чтобы запутать всех и усложнить компилятор до предела. Но смысл основной тот же: пока на тех архитектурах, где процессор вычисляет зависимости на ходу (как x86), одна команда не тормозит соседних "товарок", пока её результаты не нужны, и может быть выделена из основного потока — на IA-64 такой свободы нет, учись предсказывать задержки по памяти — то, чего в принципе предсказать невозможно на обычном современном железе (если вы не занимаетесь Meltdownʼом).

Резонный вопрос — а почему вообще Intel решил, что возможно такую архитектуру сделать эффективной? А вот тут надо заглянуть в историю и заметить, что тогда же его топ-менеджмент попался на две удочки одновременно — первая под названием Rambus, а вторая — NetBurst (Pentium 4 должен был по тем планам стать последним x86). Супербыстрая DRAM плюс ориентация на потоковые SIMD действия (для "мультимедиа") и пренебрежение всеми остальными классами задач. Чем тут поможет SIMD? А именно тем, что для основных задач хорошо предсказывается необходимость подчитать память — можно заранее (на одну-две IG) сказать prefetch на нужный кусок, пока выполняются предыдущие, оно уже в L1. Но тут наступил облом — не стала мультимедия единственным использованием компьютера, а Rambus мало того, что выпустила память с бо́льшими задержками, так и оказалось, что все новомодные усовершенствования это фикция, а заодно патентный буллинг (Intel потеряла ок. 4e8$$, насколько помню).

Так что EPIC эффективен только там, где вы можете строго ограничить время одной даже самой длительной команды. Видимо, из подобных соображений Intel исключил из IA-64 простое целочисленное деление — он знал, что это долго, но "не знал" того же про чтение DRAM. Если у вас SRAM (умножьте цену памяти на 10-20) — ok, вперёд. Если у вас DSP (тоже, считаем, SRAM) — тоже пойдёт, туда подобные архитектуры внедрились и устоялись. Но для "обычного" современного компа, для толстого сервера — ой, зась.

И вслед этому очевидный вопрос про "импортозаместительный" Эльбрус-4. На синтетических тестах он много чего показывает, но про реальные задачи идёт много подпольных отзывов про жуткие тормоза...

Здравствуйте, gardener, Вы писали:

G>Достаточно просто должно быть запустить на разных процессорах отдельные экземпляры ОС (тот же Linux) и отдельные процессы. Общаться между собой наверное всеми механизмами, которые подразумевают обмен сообщениями (пайпс например). Общую память тоже не сложно сделать — mmap() требует MMU — здесь маппинг будет некешируемый. Модификация какая-то в кернеле потребуется само собой, но не очень много.

Я не про имплементацию, а про семантику.

Понятно, что если не позволять нитям одного процесса расползаться по ядрам, то проблема сильно поуменьшится. Но не до конца, потому что есть еще shared memory. Делать ее некешируемой — это аццкие тормоза. Да и процессу не давать расползаться по ядрам тоже несколько обидно.

G>Насчет отдельных экземпляров. Если не путаю в MQX RTOS есть такая возможность. Экземпляры, обмен сообщениями.

MQX не связана обязательствами быть совместимой с традиционным API.