Разбавлю поток информации про графику и геймдев немного

Пару раз спрашивали, что такое формальная верификация алгоритма, и зачем она используется.

По сути, это процесс написания спецификации алгоритма (его описания) на одном из специальных языков, и последующая автоматическая проверка его корректности. Причем описывается не реализация, а именно сам алгоритм, в отрыве от деталей, языков программирования, и так далее.

Это позволяет математически доказать, что алгоритм валиден, не может находиться в некорректном состоянии ни при каких условиях, и так далее

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

Есть много языков для такого, перечислю несколько знакомых мне:

1. Rocq, он же раньше назывался Coq. Более старый и широкомасштабный. Построен больше на описании теорем и их доказательстве

2. TLA+, создан Лэмпортом и больше похож на бред математика, однако обладает собственной IDE на базе Eclipse под названием TLA Toolbox, а также отдельным набором инструментов проверки спецификаций. Больше используется для описания систем и процессов, чем теорем, хотя оно тоже возможно

3. Pluscal. По сути то же самое для TLA+, чем Typescript является для Javascript. То есть надстройка, которая превращается в своего более урезанного и проблемного собрата после сборки. В отличие от остальных, уже отдаленно напоминает языки программирования. Так как превращается в TLA+, то использует все те же инструменты и ту же IDE

Я больше знаком с TLA+/Pluscal, поскольку их используют для верификации распределенных алгоритмов, планировщиков задач и так далее

Например, Amazon в своих AWS с помощью TLA+ нашли баг, затрагивающий их сервисы S3 и DynamoDB, который требовал 35 шагов для воспроизведения и не был обнаружен ни тестами, ни двумя код ревью

По сути, процесс верификации на TLA+/Pluscal выглядит так:

1. Мы описываем на выбранном языке нашу систему, делаем спецификацию. Алгоритм работы, поведение, степень параллельности и тд

2. Задаем список ограничений, выполнение которых будем отслеживать. Отсутствие дедлоков, недоступность не более двух узлов, пересечения кворумов, приоритеты процессов - все, что угодно. Тут же задаем теоремы, доказательство которых нас интересует

3. Запускаем автоматическую верификацию нашей спецификации на каких-то исходных данных. Инструмент проверяет, что наши ограничения выполняются для любого возможного состояния системы в любой момент времени, что теоремы доказаны, и так далее. Если что-то не так - мы увидим, в каком состоянии оказалась система в момент нарушения какого-то ограничения, что даст нам возможность скорректировать баги в нашей спецификации

На Rocq я ничего не верифицировал, но со стороны там процесс другой и больше строится на пошаговом дедуктивном доказательстве теорем

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

Тем временем, Mozilla готовится к включению WebGPU в релизе FIrefox 141 на Windows

Остальные платформы подъедут позже, но для Windows пулл реквест с включением уже на ревью и ожидается в следующем выпуске браузера

С такими темпами адаптации, можно сказать, что через пару-тройку лет должно быть доступно уже повсеместно

Накидаю небольшую памятку по вероятностным структурам данных

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

Самый наверно известный представитель - Фильтр Блума (Bloom Filter). Позволяет очень быстро проверить принадлежность элемента ко множеству, при этом может давать ложноположительные срабатывания, но никогда не ложноотрицательные. Используется много где, например в базах данных для быстрой проверки, входит ли первичный ключ в сегмент или файл данных на диске без поиска по нему. Если фильтр сказал, что ключа там нет - его там гарантированно нет, что позволяет существенно оптимизировать время поиска (например в СУБД на базе LSM, где каждая SSTable хранится в отдельном файле). Также полезно для реализации кешей, блеклистов и прочих случаев, когда нам нужно быстро исключить возможность принадлежности элемента ко множеству. Ключевым свойством является полная независимость сложности поиска элемента от количества элементов в фильтре. Вдобавок, всего 10 бит на одно хранимое значение снижают вероятность ложноположительного обращения до 1%

Также есть развитие идей фильтра Блума в виде Cuckoo Filter и Quotient Filter, которые уже поддерживают удаление элементов, но более сложны в реализации и потребляют больше памяти.

Из другого есть Count-Min Sketch, который позволяет очень эффективно подсчитать частоту элементов в потоке данных, но с небольшой вероятностью ее завышения. Больше подходит для анализа трафика, рекомендаций и подобного

Далее идет HyperLogLog, занятная штука, позволяющая найти количество уникальных элементов во множестве, но имеющая незначительную вероятность ошибки (около 1% в типичных применениях). Всего 1.5 кбайт памяти достаточно для анализа более чем 10^9 элементов. Используется для подсчета уникальных посетителей систем, аналитики и работы с большими данными

Также есть T-Digest, который может быстро найти распределение элементов по перцентилям, однако тоже имеет некую погрешность. Часто используется в A/B тестах, иногда в машинном обучении и других сферах

Еще можно добавить Lossy Counting, позволяющий найти N самых частых элементов во множестве с минимальными затратами памяти за счет удаления самых редких элементов в процессе работы. Чаще всего встречается в разного рода аналитике

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

Например, Google Chrome использует фильтры Блума для быстрого распознавания вредоносных URL, а Medium для своей рекомендательной системы, отсеивая уже просмотренные посты. В то время как HyperLogLog напрямую доступен в Redis через команды pfadd и pfcount для подсчета количества уникальных событий

Эти структуры данных явно не относятся к тем, что часто нужны на практике, но знание об их существовании может выручить в том редком случае, когда они все же пригодятся

Последнее время стараюсь если и прокрастинировать, то все равно делать что-то полезное

Например, вместо диссертации пишу многострадальный гайд по графике на wgpu

Все равно ощущение, что займет это годы, но так хоть какой-то прогресс будет

А если летом защищусь и решу вопрос с призывом, то еще больше времени появится

Дописал вторую главу туториала, вроде бы

Постоянно нахожу, что еще можно дописать или отредактировать, но пока вроде всё устраивает

Вышло 3954 слова без учета блоков кода или 4627 с ними (диаграммы тоже считаются за блоки кода, поскольку они в формате Mermaid)

Надеюсь, что следующие главы будут поменьше, но как будто ощущение, что нет)

Такими темпами, может быть закончу базовый раздел в этом десятилетии)

откопал старое сообщение про типы рендера, решил сюда закинуть для истории

1. Forward render, когда все просто рисуется напрямую (если вы "просто рендерите", то, скорее всего, у вас именно он).

Конечно, в современных движках уже используются модифицированные алгоритмы (Tiled Forward, Clustered Forward, Forward+ и тд), но общий принцип плюс-минус один.

Из плюсов:

- легко работать с прозрачностью

- поддерживает msaa

- имеет низкие требования к пропускной способности видеопамяти

Из минусов:

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

- все современные продвинутые реализации требуют компьют шейдеров.

- методы постобработки все равно иногда требуют данные, которых нет в форварде, и приходится мучаться с z препассами и прочим, по сути вводя куски деферред подхода для части данных (например гораздо тяжелее SSAO и SSR реализовать, чем в деферреде).

- плохо переживает мелкие треугольники на экране

2. Deferred render, когда всё рисуется в два этапа - сначала заполняем специальный g-буфер данными, потом на базе него уже рисуем саму сцену. Именно этот способ чаще всего используется в современных игровых движках, из-за простоты и преимуществ

Из плюсов:

- про него очень много информации

- работает даже на очень древнем железе

- масштабируемость зависит больше от размера экрана, а не сложности сцены.

- легче переживает мелкие треугольники на экране.

- постобработке нужны данные из g-буфера, а тут они уже и так есть, то есть легче всякие красивости наводить, включая PBR.

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

из минусов:

- msaa не работает, сглаживание тут в принципе тяжело сделать нормально.

- прозрачность тоже очень тяжело реализовать, настолько, что часто делают отдельный форвард проход для прозрачных объектов.

- в среднем по больнице требует больше пропускную способность видеопамяти, хотя есть более заморочные современные реализации, которые это потребление уменьшают

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

например, Doom 2016 сделан на гибридном рендере. У них сначала маленький пре-пасс для заполнения куска g-буфера, а потом используют его + данные рендера прошлого кадра для рендера текущего, из-за чего отражения отстают на один кадр от самой сцены

4. Новый подход через буфер видимости.

Он чем-то похож на деферред, но вместо рендера текстур в g-буфер, там заполняется числовой буфер с идентификаторами объектов и их треугольников, что позволяет их очень эффективно упаковать, например, в u32. Вообще про это есть доклад от Интела, но уже есть и реализации в разных самописных движках, например цикл из 4 статей про реализацию на DirectX 12 (не самую оптимальную кстати). И в целом есть еще разные варианты этого алгоритма, от разных авторов в разных статьях/докладах

из плюсов:

- работает даже быстрее деферреда, и очень хорошо масштабируется.

- если у форварда запуски фрагментного шейдера зависят от количества источников света, а у деферреда от g-буфера, то тут все привязано к пикселям на экране, и для многих вещей будет только один запуск на один пиксель

- очень нетребователен к пропускной способности видеопамяти, если реализовывать "чистый" буфер видимости, а не использовать его для заполнения g буфера и последующего деферреда

из минусов:

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

Тот самый доклад Интела про Visiblity Buffer

и упомянутая серия статей про реализацию на DirectX 12

она не совсем оптимальна, потому что, как и в Unreal Engine, автор использует visibility buffer только для наполнения g буфера, который потом идет в обычный деферред пайплайн. А это, по сути, обнуляет половину преимуществ visibility buffer по сравнению с использованием только его вместо деферреда, таких как низкая зависимость от пропускной способности видеопамяти

http://filmicworlds.com/blog/visibility-buffer-rendering-with-material-graphs/

в целом, Nanite из Unreal Engine является мутацией подхода c Visibility Buffer, но он не очень эффективен.

Потому что при использовании visibility buffer нам вообще не нужен g-буфер, мы можем напрямую работать с идентификаторами в компьютах и очень сильно всё ускорить.

А Nanite использует буфер видимости исключительно чтобы ускорить заполнение g-буфера, который потом используется уже у них в обычном деферред пайплайне.

В общем, они сделали более простую реализацию, которая лучше интегрируется в существующий код движка, но далеко не самая оптимальная при этом

собственно, почти все продвинутые варианты этих подходов довольно заморочные, но или дают хороший буст производительности, или решают какие-то проблемы

и почти все эти продвинутые варианты требуют компьют шейдеров, то есть кроссплатформерный опенгл в пролете

если подытожить, то есть простая памятка

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

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

буфер видимости потенциально лучше, но очень заморочный и по нему меньше информации, поэтому для инди вряд ли стоит того

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

следовательно, там он показывает даже лучшие результаты, чем на обычных пк

также, люди, пробовавшие разные подходы, пишут, что в среднем деферред оказывается быстрее даже форвард+, если нужен хоть какой-то постпроцессинг вроде SSAO

https://www.reddit.com/r/GraphicsProgramming/comments/1kmrura/deferred_rendering_vs_forward_rendering_in_aaa/

Немного подробнее про деферред рендер, так как считаю его сейчас оптимальным выбором для инди

В наивном варианте он сводится к рендеру в 2 прохода:

1. Через MRT (Multiple Render Targets) делаем обычную отрисовку наших мешей, но вместо вывода на экран пишем их параметры в отдельные текстуры. Обычный набор - позиции, нормали, альбедо (цвет) и спекулар (отражаемость). Потом можно расширять под PBR другими текстурами по необходимости

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

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

Если в наивном форвард рендере нам надо считать свет для каждого фрагмента объекта, даже если он в итоге не будет освещен, и делать это для каждого источника света

То в деферреде на итоговом прогоне освещения мы идем чисто по пикселям экрана и семплим текстуры G Buffer для расчета света.

Отсюда независимость сложности расчета света в деферреде от сложности сцены - сама сцена посчитана на построении G Buffer, для света мы работаем только с итоговыми пикселями

Но тут и минусы - видеопамять и пропускная способность видеокарты тратятся на хранение G Buffer и взаимодействие с ним. А также полупрозрачность требует отдельного форвард прогона. И не работает MSAA, приходится реализовывать более сложные способы сглаживания

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

Однако, указанная выше реализация все еще очень неоптимальна, потому что даже в ней, мы вынуждены во фрагментном шейдере прохода освещения рассчитывать свет для pixels * number of lights, то есть каждый источник света участвует в расчетах каждого пикселя, даже если физически в сцене объект на нем слишком далеко и не может быть засвечен. Что все равно дорого, пусть и гораздо лучше обычного форварда

есть несколько дальнейших оптимизаций

1. Light volumes. Старый прием, хорош отсутствием необходимости использовать компьют шейдеры, и на этом все

Сводится к тому, что мы заранее для каждого источника света рассчитываем освещаемое им пространство (тот самый "объем"). Например, сферу

И далее, когда у нас идет проход расчета освещения, мы вместо полноэкранного квада просто рисуем эти объемы (сферы, конусы и тд). И считаем свет только в их пределах, Таким образом, мы отсекаем из расчетов источники света, которые находятся слишком далеко

У данного подхода есть ряд минусов:

- нужно рендерить по объекту на источник света, то есть большой overdraw и плохо масштабируется на большое количество источников

- сложности с глубиной, камерой внутри освещенных объемов и т.д.

2. Deferred Lighting (оно же Light Pre-Pass). Тоже старая техника

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

Можно совмещать с light volumes

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

На данный момент встречается редко

3. Tiled Deferred Shading. Более современное решение, требует компьют шейдеров

Идея в следующем: в компьют шейдере делим экран на тайлы (обычно 8х8 или 16х16). Для каждого тайла строим список источников света, пересекающих его область видимости (tile frustum). Это может быть просто список индексов из глобального массива источников света

Далее считаем свет по пикселям тайла, учитывая только его источники освещения. Ну и пишем результат в буфер освещения

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

Прикреплю ниже презентацию этого подхода с бенчмарками с SIGGRAPH 2010

Из минусов же:

- большое использование видеопамяти на все эти буферы индексов тайлов, причем оно зависит и от разрешения.

- 2д тайлы не знают глубины. При большом динамическом диапазоне по Z в одном тайле может оказаться много источников света

4. Clustered Deferred Shading. Современный, очень оптимизированный, но довольно сложный в реализации вариант

Это развитие идеи Tiled Deferred Shading.

Вместо 2д тайлов мы разбиваем в 3д - каждый frustum еще нарезается логарифмически по Z, таким образом получаем кластеры.

Аналогично, строим список источников света, но уже для каждого кластера отдельно. Соответственно, при расчете освещения, каждый кластер учитывает только свои источники света, что решает вопрос глубины

Тут довольно много оптимизаций, например можно делать куллинг кластеров по октодереву

Также эти списки источников света для кластеров можно потом переиспользовать, например в отдельном прогоне для прозрачности

Реализация довольно трудоемка, однако выдает очень внушительные результаты - в изначальном докладе их реализация куллила 1048576 случайно распределенных источников света за 6 миллисекунд, в то время как Tiled Deferred Shading справился с той же задачей за 342 миллисекунды

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

Сам доклад тоже скину