Какое такое "почти"? Этого на таком уровне не может быть там видно вообще в принципе. Как в RTL-симуляции увидеть баг типа Rowhammer? Чтобы такое было видно, нужно делать некую физическую симуляцию (с учетом электромагнитных излучений) уже разведенного конкретным способом чипа. RTL-симуляция ничего про разводку чипа не знает, так что такого рода баги она не может отловить вообще никак.
Эмуляция (emulation) - это на аппаратном эмуляторе Synopsys ZeBu или Mentor Veloce. Вероятно в России (как ранее в СССР) словом "эмуляция" называют программную симуляцию.
Правильно ли я понимаю, что эти эмуляторы представляют из себя несколько запараллеленных FPGA, на которые распределяют эмулируемые части и потом тактируют это от одного источника клока? Или там какие-то другие решения, типа wavefront array processor? Современные GPU можно переориентировать под эти задачи?
И каким эмулятором можно ловить баги, когда один блок влияет на другой из-за электромагнитных помех?
А почему тесты, а не формальная верификация? Применим ли например https://github.com/rems-project/sail для верификации блока GPU, учитывая что в GPU тоже есть некая система команд? Что вообще сейчас используют для формальной верификации в этой области? И не очень понятна эта фраза
6 часов в софтвере и 8 часов на эмуляторе
Что значит "в софтвере"? Разве "в софтвере" не означает как раз эмуляцию?
Не, тут все не так однозначно. Вот https://godbolt.org/z/MzTd3fx7T для наглядности переписал на uint32_t и результат возвращается в uint64_t. Вручную записанная формула лучше компилируется, и никаких переполнений тут нет
#include <inttypes.h>
uint64_t sum_up_to2(uint32_t value)
{
return ((uint64_t)value*(value-1))/2;
}
uint64_t sum_up_to(uint32_t value)
{
uint64_t result = 0;
for (uint32_t x = 0; x < value; ++x) {
result += x;
}
return result;
}
Зачем коллаца? Рассмотрим какую-нибудь сортировку. Вот например такая реализация на Haskell:
bubbleSort :: Ord a => [a] -> [a]
bubbleSort = untilFixed bubblePass
where
bubblePass [] = []
bubblePass [x] = [x]
bubblePass (x:y:xs)
| x > y = y : bubblePass (x:xs)
| otherwise = x : bubblePass (y:xs)
untilFixed f x = let fx = f x
in if fx == x then x else untilFixed f fx
Такой код может быть переписан на STMLib относительно легко
(set-logic ALL)
(set-option :produce-models true)
; bubblePass :: [Int] -> [Int]
; Haskell:
; bubblePass [] = []
; bubblePass [x] = [x]
; bubblePass (x:y:xs)
; | x > y = y : bubblePass (x:xs)
; | otherwise = x : bubblePass (y:xs)
(define-fun-rec bubblePass ((s (Seq Int))) (Seq Int)
(ite (<= (seq.len s) 1)
; [] или [x]
s
; (x:y:xs)
(let ((x (seq.nth s 0))
(y (seq.nth s 1))
(len (seq.len s)))
(let ((xs (seq.extract s 2 (- len 2))))
; tailInput = if x > y then (x:xs) else (y:xs)
(let ((tailInput
(ite (> x y)
(seq.++ (seq.unit x) xs)
(seq.++ (seq.unit y) xs))))
; tailOutput = bubblePass tailInput
(let ((tailOutput (bubblePass tailInput)))
; head = if x > y then y else x
; результат: head : tailOutput
(seq.++ (seq.unit (ite (> x y) y x))
tailOutput)))))))
; untilFixed :: (a -> a) -> a -> a
; Haskell-специализация:
; bubbleSort = untilFixed bubblePass
(define-fun-rec untilFixed ((s (Seq Int))) (Seq Int)
(let ((fx (bubblePass s)))
(ite (= fx s)
s
(untilFixed fx))))
(define-fun bubbleSort ((s (Seq Int))) (Seq Int)
(untilFixed s))
(define-fun initialArray () (Seq Int)
(seq.++ (seq.unit 9)
(seq.++ (seq.unit 2)
(seq.++ (seq.unit 4)
(seq.++ (seq.unit 1)
(seq.++ (seq.unit 3)
(seq.++ (seq.unit 5)
(seq.++ (seq.unit 7)
(seq.++ (seq.unit 8)
(seq.++ (seq.unit 6)
(seq.unit 0)
))))))))))
(define-fun sortedArray () (Seq Int)
(bubbleSort initialArray))
(check-sat)
(get-value (initialArray sortedArray))
Вроде всё корректно. Тут я для примера сортирую список 9 2 4 1 3 5 7 8 6 0. Можно запустить это в Z3 и он действительно сортирует, только он не сможет доказать, что такая сортировка работает для общего случая. Для проверки сортировки тут требуется функция для проверки упорядоченности (для любых двух соседних элементов a, b должно быть верно, что a <= b) и что массив после сортировки является перестановкой изначального массива, и что для любых списков любой длины эти оба условия выполняются. Если так сделать, Z3 просто зависнет или отвалится по таймауту. Такое надо через Rocq, Idris, Agda и прочие proof assistant доказывать
И зачем завязываться на SMT-солверы? Может быть какие-то вещи они доказать не осилят, и придется доказывать на Coq Rocq или чем-то подобном? Насколько я помню, Frama-C переводит свои ASCL-контракты в WhyML, и там он может быть оттранслирован в кучу разных автоматических и интерактивных пруверов https://www.why3.org/#provers. Может быть вам тоже стоит использовать такой подход?
А до какого уровня авторы численных схем их оптимизируют, какие нюансы учитываются? Например, этот herbie "знает" о том, что в процессорах есть FMA инструкции (fused multiply-add) и может их использовать, в числовых схемах такое учитывают? Учитывается ли наличие SIMD инструкций (в подобных схемах могут явно указывать, что вот тут это уравнение должно считаться через SIMD?) ?
Но у вас ведь тоже на задачах газодинамики используется некий алгоритм разбиения пространства на некие куски, чтобы симуляцию этих кусков разбросать по отдельным вычислительным узлам. Каким образом вы решаете, на какие куски разделить пространство и как оптимальней его разбросать на разные ядра с учетом особенностей оперативной и кеш памяти? Этот LRnLA как раз об этом. Может тут еше подойдет полиэдральная модель оптимизации циклов https://xeno-by.livejournal.com/28122.htmlhttps://en.wikipedia.org/wiki/Frameworks_supporting_the_polyhedral_model
Может для вашей задачи получается, что некие области требуют более точного моделирования (с использованием более мелкой сетки) т.к. в них происходят более сложные процессы, и эту сетку можно динамически перестраивать, когда этот сложномоделируемый процесс (ударная волна или может турбулентность какая-то) будет смещаться в пространстве (т.е. придумать эвристику, которая отслеживала границы процесса и уплотняла под него сетку)? Применяется ли у вас что-то подобное?
Есть еще такой проект https://herbie.uwplse.org/ для оптимизации вычислений с плавающей запятой. Там можно находить некие компромиссные оптимизации (например теряем в точности 5% для такого-то диапазона входных значений, но зато считаем в 5 раз быстрее). Написан на Racket (диалект лиспа)
https://stackoverflow.com/questions/77846522/how-can-i-generalize-diamond-tiling-to-higher-dimensions вот тут например, в самом низу есть ссылки на ряд статей. Сразу скажу, я не специалист в этой области, так что напишу в рамках своего понимания. Насколько я понял, симулируются некие процессы в пространстве, пространство разбивается на некие кирпичики определенной формы, притом разбивается рекурсивно. Для симуляции некоей одной клетки нужно учитывать состояние соседних клеток вокруг нее, время в клетках вокруг допустим будет t, просимулировали процессы в клетке и получили ее состояние для времени t+n. И пространство можно каким-то хитрым образом разбивать на такие куски, чтобы простоя было меньше. Собственно, вот цитата из той ссылки:
The only hint I can find in the literature on how it may be done comes from a Russian research group at Keldysh Institute of Applied Mathematics. This group developed a series of different parallel spacetime decomposition algorithms in the last 20 years using a methodology called Locally-Recursive non-Locally Asynchronous (LRnLA) algorithms. LRnLa is not a single algorithm but a general guideline of how to design them. Basically: (1) The tessellation must should be a recursive process to utilize the entire memory hierarchy (it's not necessarily automatic, manual parameter tuning for different machines is allow as long as tiling algorithm itself can be generalized). (2) Parallelism should exist between different tiles, the dependency conflict problem should be solvable in some natural way. Using both requirements as starting point, researchers would manually examine the stencil dependencies and use their intuition in solid geometry to design custom algorithms to satisfy these goals. Unlike polyhedron compilers, these are custom solutions designed by human domain experts for human use, with geometric interpretations that ease implementations (but only from the perspective of mathematicians and physicists...).
Чтобы максимально избежать простоев железа необходимо запускать счет на каждом ядре и GPU сразу же, как только для него готовы входные данные. К моменту, когда ядро или GPU завершило обработку, для него должен уже быть готов новый входной массив, чтобы следующий цикл счета запускался без задержек.
Почитайте про LRnLA алгоритмы, вроде это как раз из этой области
Делать на уровне DSL то, что называется common subexpression elimination (CSE) чисто для того, чтобы компилятор быстрее компилировал - это еще имеет смысл, если куски подвыражений много раз повторяются и компилятор при оптимизации их долго сам находит и оптимизирует. А вот loop-invariant code motion это достаточно простая и понятная вещь, не думаю что компилятор будет сильно дольше компилировать (или хуже оптимизировать), если это не делать за него.
Я заметил, что некоторые выражения повторяются, но со смещением на 1 по одному из индексов (индексу самого внутреннего цикла). В принципе, это ожидаемо – мы вычисляем поток через правую грань ячейки, потом сдвигаемся на 1 вправо и снова вычисляем то же значение для уже левой грани текущей ячейки. Почему бы не вычислить его один раз и не сохранить для следующей итерации цикла?
Не знаю, есть ли специальное название для такой оптимизации, но некоторые компиляторы это делать умеют. Правда тут требуются некоторые моменты учесть, дать компилятору определенные гарантии https://godbolt.org/z/Eo4dxz3x5 Компилятор должен понимать, что вызываемая в теле цикла функция является функционально чистой, и что входной массив не изменяется. Clang эту оптимизацию сделать не осиливает
Дело в том, что кусочки выражений, которые подставляются в зависимости от условий, в численных схемах не такие уж и большие. В принципе, дешевле будет вычислять сразу обе ветки ветвления, а потом код вида ...
Проблема тут в том, что компилятор может на эти "подсказки" наплевать и всё равно сгенерировать бранч. Вот например https://godbolt.org/z/xx5vf3jrK тут branchless получился только для функции test4. Инструкция bltu это "branch if less than unsigned"
Лучше было бы для таких вещей специальные директивы для компилятора придумать, чтобы пометить конкретную область кода или функцию, в которой бранчи не использовать. Может быть такое уже есть где-то.
На вопрос про медианную сложность я там ответа не нашел. Или может я невнимательно читал? Временная сложность алгоритмов оценивается обычно по лучшему, среднему и худшему случаю. Лучший случай - число неких операций при самом лучшем случае входных данных. Средний - когда рассматриваем среднее арифметическое числа операций для всех возможных входных данных длины n. Худший - для худшего случая. А оцениваются ли алгоритмы по медианному критерию, т.е. когда есть такое число x, что в половине случаев алгоритм решает задачу за меньше чем x операций, в половине случаев решает задачу за более чем x операций? Или такая оценка не имеет смысла?
А делались ли медианные оценки временной сложности разных алгоритмов сортировки? Ну т.е. для размера массива n для всего множества входных данных, какой будет медианное значение сравнений (в половине случаев алгоритм будет делать меньше, в половине случаев больше сравнений)? И какая наименьшая медианная оценка из множества всех возможных алгоритмов?
Что-то я вообще запутался. Сначала вы пишете "в худшем случае", потом нижняя оценка. Big-omega это же про лучший случай. И "нижняя оценка" это тоже означает лучший случай. Т.е. такой случай, когда алгоритм выполняется быстрее всего.
Нижняя оценка для сортировки будет Ω(n). У пузырьковой она как раз такая, если на вход подать изначально сортированный массив. Он просто пробежится по всему массиву, попарно сравнивая соседние элементы.
Не существует универсального алгоритма .... находил бы перестановку элементов p такую, что .... используя меньше, чем O(n log n) попарных сравнений, т.е. сравнений двух конкретных элементов.
Что значит "универсального алгоритма"? O(n log n) это верхняя, нижняя или средняя оценка? Если предположить, что массив уже изначально сортирован, количество попарных сравнений для проверки этой гипотезы будет n-1.
Какое такое "почти"? Этого на таком уровне не может быть там видно вообще в принципе. Как в RTL-симуляции увидеть баг типа Rowhammer? Чтобы такое было видно, нужно делать некую физическую симуляцию (с учетом электромагнитных излучений) уже разведенного конкретным способом чипа. RTL-симуляция ничего про разводку чипа не знает, так что такого рода баги она не может отловить вообще никак.
Правильно ли я понимаю, что эти эмуляторы представляют из себя несколько запараллеленных FPGA, на которые распределяют эмулируемые части и потом тактируют это от одного источника клока? Или там какие-то другие решения, типа wavefront array processor? Современные GPU можно переориентировать под эти задачи?
И каким эмулятором можно ловить баги, когда один блок влияет на другой из-за электромагнитных помех?
А почему тесты, а не формальная верификация? Применим ли например https://github.com/rems-project/sail для верификации блока GPU, учитывая что в GPU тоже есть некая система команд? Что вообще сейчас используют для формальной верификации в этой области?
И не очень понятна эта фраза
Что значит "в софтвере"? Разве "в софтвере" не означает как раз эмуляцию?
Не, тут все не так однозначно. Вот https://godbolt.org/z/MzTd3fx7T для наглядности переписал на uint32_t и результат возвращается в uint64_t. Вручную записанная формула лучше компилируется, и никаких переполнений тут нет
Очень похоже на то, что писал Стивен Вольфрам
https://writings.stephenwolfram.com/2020/04/finally-we-may-have-a-path-to-the-fundamental-theory-of-physics-and-its-beautiful/ (есть перевод на хабре: https://habr.com/ru/articles/518206/)
Зачем коллаца? Рассмотрим какую-нибудь сортировку. Вот например такая реализация на Haskell:
Такой код может быть переписан на STMLib относительно легко
Вроде всё корректно. Тут я для примера сортирую список 9 2 4 1 3 5 7 8 6 0. Можно запустить это в Z3 и он действительно сортирует, только он не сможет доказать, что такая сортировка работает для общего случая. Для проверки сортировки тут требуется функция для проверки упорядоченности (для любых двух соседних элементов
a, bдолжно быть верно, чтоa <= b) и что массив после сортировки является перестановкой изначального массива, и что для любых списков любой длины эти оба условия выполняются. Если так сделать, Z3 просто зависнет или отвалится по таймауту. Такое надо через Rocq, Idris, Agda и прочие proof assistant доказыватьИ зачем завязываться на SMT-солверы? Может быть какие-то вещи они доказать не осилят, и придется доказывать на
CoqRocq или чем-то подобном? Насколько я помню, Frama-C переводит свои ASCL-контракты в WhyML, и там он может быть оттранслирован в кучу разных автоматических и интерактивных пруверов https://www.why3.org/#provers. Может быть вам тоже стоит использовать такой подход?Возможно я что-то путаю, но по-моему это называется refinement type (Как в Liquid Haskell) a не dependent type
А до какого уровня авторы численных схем их оптимизируют, какие нюансы учитываются? Например, этот herbie "знает" о том, что в процессорах есть FMA инструкции (fused multiply-add) и может их использовать, в числовых схемах такое учитывают? Учитывается ли наличие SIMD инструкций (в подобных схемах могут явно указывать, что вот тут это уравнение должно считаться через SIMD?) ?
Но у вас ведь тоже на задачах газодинамики используется некий алгоритм разбиения пространства на некие куски, чтобы симуляцию этих кусков разбросать по отдельным вычислительным узлам. Каким образом вы решаете, на какие куски разделить пространство и как оптимальней его разбросать на разные ядра с учетом особенностей оперативной и кеш памяти? Этот LRnLA как раз об этом. Может тут еше подойдет полиэдральная модель оптимизации циклов https://xeno-by.livejournal.com/28122.html https://en.wikipedia.org/wiki/Frameworks_supporting_the_polyhedral_model
Может для вашей задачи получается, что некие области требуют более точного моделирования (с использованием более мелкой сетки) т.к. в них происходят более сложные процессы, и эту сетку можно динамически перестраивать, когда этот сложномоделируемый процесс (ударная волна или может турбулентность какая-то) будет смещаться в пространстве (т.е. придумать эвристику, которая отслеживала границы процесса и уплотняла под него сетку)? Применяется ли у вас что-то подобное?
Есть еще такой проект https://herbie.uwplse.org/ для оптимизации вычислений с плавающей запятой. Там можно находить некие компромиссные оптимизации (например теряем в точности 5% для такого-то диапазона входных значений, но зато считаем в 5 раз быстрее). Написан на Racket (диалект лиспа)
https://stackoverflow.com/questions/77846522/how-can-i-generalize-diamond-tiling-to-higher-dimensions вот тут например, в самом низу есть ссылки на ряд статей. Сразу скажу, я не специалист в этой области, так что напишу в рамках своего понимания. Насколько я понял, симулируются некие процессы в пространстве, пространство разбивается на некие кирпичики определенной формы, притом разбивается рекурсивно. Для симуляции некоей одной клетки нужно учитывать состояние соседних клеток вокруг нее, время в клетках вокруг допустим будет t, просимулировали процессы в клетке и получили ее состояние для времени t+n. И пространство можно каким-то хитрым образом разбивать на такие куски, чтобы простоя было меньше. Собственно, вот цитата из той ссылки:
Почитайте про LRnLA алгоритмы, вроде это как раз из этой области
Делать на уровне DSL то, что называется common subexpression elimination (CSE) чисто для того, чтобы компилятор быстрее компилировал - это еще имеет смысл, если куски подвыражений много раз повторяются и компилятор при оптимизации их долго сам находит и оптимизирует. А вот loop-invariant code motion это достаточно простая и понятная вещь, не думаю что компилятор будет сильно дольше компилировать (или хуже оптимизировать), если это не делать за него.
Это должен уметь делать компилятор. https://en.wikipedia.org/wiki/Common_subexpression_elimination
А это https://en.wikipedia.org/wiki/Loop-invariant_code_motion
Не знаю, есть ли специальное название для такой оптимизации, но некоторые компиляторы это делать умеют. Правда тут требуются некоторые моменты учесть, дать компилятору определенные гарантии https://godbolt.org/z/Eo4dxz3x5
Компилятор должен понимать, что вызываемая в теле цикла функция является функционально чистой, и что входной массив не изменяется. Clang эту оптимизацию сделать не осиливает
Проблема тут в том, что компилятор может на эти "подсказки" наплевать и всё равно сгенерировать бранч. Вот например https://godbolt.org/z/xx5vf3jrK тут branchless получился только для функции test4. Инструкция bltu это "branch if less than unsigned"
Лучше было бы для таких вещей специальные директивы для компилятора придумать, чтобы пометить конкретную область кода или функцию, в которой бранчи не использовать. Может быть такое уже есть где-то.
На вопрос про медианную сложность я там ответа не нашел. Или может я невнимательно читал?
Временная сложность алгоритмов оценивается обычно по лучшему, среднему и худшему случаю. Лучший случай - число неких операций при самом лучшем случае входных данных. Средний - когда рассматриваем среднее арифметическое числа операций для всех возможных входных данных длины n. Худший - для худшего случая. А оцениваются ли алгоритмы по медианному критерию, т.е. когда есть такое число x, что в половине случаев алгоритм решает задачу за меньше чем x операций, в половине случаев решает задачу за более чем x операций? Или такая оценка не имеет смысла?
Да, теперь понятно.
А делались ли медианные оценки временной сложности разных алгоритмов сортировки? Ну т.е. для размера массива n для всего множества входных данных, какой будет медианное значение сравнений (в половине случаев алгоритм будет делать меньше, в половине случаев больше сравнений)? И какая наименьшая медианная оценка из множества всех возможных алгоритмов?
Что-то я вообще запутался. Сначала вы пишете "в худшем случае", потом нижняя оценка. Big-omega это же про лучший случай. И "нижняя оценка" это тоже означает лучший случай. Т.е. такой случай, когда алгоритм выполняется быстрее всего.
https://www.bigocheatsheet.com/ - тут у bubble sort в столбце Time Complexity указано Ω(n) для Time Complexity - Best
Нижняя оценка для сортировки будет Ω(n). У пузырьковой она как раз такая, если на вход подать изначально сортированный массив. Он просто пробежится по всему массиву, попарно сравнивая соседние элементы.
Что значит "универсального алгоритма"? O(n log n) это верхняя, нижняя или средняя оценка? Если предположить, что массив уже изначально сортирован, количество попарных сравнений для проверки этой гипотезы будет n-1.