Имхо есть шансы у Salt, особенно если появятся удобные средства модульного и интеграционного тестирования стейтов/формул. Да, есть плагин к kitchen — но это только интеграционное, и с multi-node там все грустно. И есть внутренняя система тестов — но если я правильно понимаю для тестирования своих стейтов их придется положить внутрь сальтовских исходников, что вообще за гранью...
автор уже предложил пример использования TLA, поэтому возникает вопрос — а чем ваш вариант будет лучше? Можно подробнее расписать нажатия кнопок (обезьяний подход), можно подробнее описать происходящее внутри, ну и можно ещё что-то общее добавит
Скажем так — у автора относительно большая задача, в которую нужно отдельно вникать, что отвлекает от изучения собственно инструмента, почти нет теории, сразу прыжок на абстракцию над TLA+ (т.е. PCAL). Что думал написать я — небольшое введение в принципы, стоящие за TLA+, и дальше очень простой практический пример в TDD стиле (начиная буквально с 3-х строчника на чистом TLA и заканчивая моделью выложенной на гитхаб), в процессе объясняя по мере необходимости как синтаксические конструкции, так и теоретические вещи типа концепций stuttering и weak/strong fairness.
Меня автор фактичски подцепил на TLA своей первой статьей, в качестве тренировки я реализовал (причем в TDD стиле) модель протокола надежной передачи сообщений в сети с возможными потерями, огреб в процессе всяких приколов и уже давно думаю запилить статью-туториал на эту тему, но не хватает мотивации. Если интерес есть — могу попробовать взять себя в руки и все-таки сделать ее.
Ну на самом деле на Alloy тоже можно моделировать трейсы, аналогичные тем, что делает TLC (просто ввести некий time в структуру состояния системы с возможностью закольцовывания "суффикса" и наложить ограничения на возможнные переходы — аналог тех самых actions из TLA). Где-то даже статьи были на эту тему со сравнением перфоманса, и там тоже все неоднозначно. Если интересно — могу еще раз найти и кинуть ссылками.
Хм, а это не тот самый Niklas, который вел отличный блог про движок bitsquid, который в какой-то момент стал autodesk stingray, и у которого были весьма похожие статьи еще в 2010, 2011 и 2015?
как можно использовать текстуру до того, как она действительно готова
Из того, что сам видел (nvidia, opengl):
попытались загрузить заранее все текстуры — видеопамяти не хватило, драйвер начал свопить текстуры в системную память, как только текстура требуется для отрисовки — она свопится назад в видеопамять — фриз
попытались стримить текстуры — заранее создаем и мапим GL_PIXEL_UNPACK буфер, в параллельном потоке пишем, сигнализируем основному когда закончили, в основном делаем unmap и создаем/апдейтим из буфера текстуру. И если ее попытаться использовать сразу же — драйвер зафризится, потому что на самом деле процесс апдейта на видеокарте еще не закончился. Когда-то с этим можно было бороться только выжиданием 2-3 кадра "наугад", потом завезли fence-объекты, стало легче, но ими еще пользоваться нужно уметь
что значит «стриминг динаической геометрии» — в смысле загрузка новых данных на ГП каждый кадр?
Ну да. Например скининг сильно low-poly моделек (дальние LODы) бывает выгоднее на CPU считать. Другой пример — GUI.
Неужели разрабы 2х самых популярных игр в мире настолько плохи/бедны что не могут исправить эту вопиющую проблему?
В реалиях разработки под PC пытаться сделать stutter-free движок — это как ходить по минному полю. Очень легко нарваться на фризы в драйвере на миллисекунды или десятки миллисекунд:
при использовании текстуры до того, как она действительно готова к использованию
при использовании шейдера с новой комбинацией параметров (некоторые драйверы могут в этой ситуации внезапно решить — а не попробовать ли нам микрокод "вот прям ща" пооптимизировать?)
куча подводных камней со стримингом динамической геометрии и массивов параметров для шейдеров
куча подводных камней в реализациях разных графических драйверов
Вроде как вулкан/DX12 как раз призваны избавить от таких неожиданностей, но в то же время эти API еще более низкоуровневые и сложные в использовании
Alloy же, при поиске моделей, просматривает все состояния вплоть до заданного предела. TLС тоже просматривает (в основном режиме работы) все состояния порождаемые TLA+ формулой.
Теоретически никто не запрещает в property-based тестах генерировать не случайные состояния, а вообще все (в пределах заданных ограничений), но из-за комбинаторного взрыва это может быть очень медленно. Если TLC тупо брутфорсит все пространство состояний — это ведь ничем не лучше, или там все-таки есть какие-то оптимизации? Alloy — да, за счет использования SAT-солвера может проверить пространство состояний гораздо быстрее, но как вы сами показали в статье далеко не все модели можно им проверить в принципе.
Выразительность: Alloy и TLA+ напрямую с тестами тяжело сравнивать, так как выразительные свойства Alloy и TLA+ намного лучше, так как там мы пишем декларативно и на высоком уровне абстракции. Например, в тестах мне явно нужно писать функцию сортировки или функцию проверки того, что массив отсортирован, в Alloy (и в TLA+ тоже, только синтаксис немного другой) я пишу предикат, где описываю нужное мне свойство: pred sorted [s: seq Obj] { all disj x,y: s.elems | x < y => s.idxOf[x] < s.idxOf[y]}
Питон тоже умеет очень даже декларативно и коротко:
def is_sorted(s: List) -> bool:
return all(a <= b for a, b in zip(s, s[1:]))
Например, на базе тестов нельзя нормально искать контр-примеры к конфигурации какой-либо системы.
Ну почему же? Вот пример такого теста для протокола binary agreement: https://github.com/poanetwork/hbbft/blob/master/tests/binary_agreement.rs#L64 Насчет учета классов эквивалентности — к сожалению, не уверен, что правильно понимаю о чем речь, можете показать пример и/или кинуть ссылкой почитать именно в этом контексте?
TLA+ позволяет довольно просто описать несколько взаимодействующих процессов системы
При наличии небольшого фреймворка такое можно провернуть и в "обычных" языках программирования. Вот пример теста, который проверяет кучу инвариантов для протокола смены лидера (в частности, упрощенно, что если он начался, то в итоге закончится и все запросы выполненные хотя бы на одной ноде окажутся в очереди на выполнение всеми нодами): https://github.com/hyperledger/indy-plenum/blob/master/plenum/test/consensus/test_sim_view_change.py#L9 Причем проверяет это непосредственно для продакшн-кода на большом количестве конфигураций, а за счет инъекции всех внешних зависимостей (в частности времени, шедулера и сетевого стека) тест работает повторяемо и достаточно быстро. Багов в начальной имплементации кстати этот тест наловил прилично.
К сожалению, пока я вижу только следующие плюсы (с оговорками):
Alloy, и возможно TLC, могут эффективнее перебирать пространства состояний (но при этом Alloy довольно ограничен в том, какие свойства в принципе поддаются проверке)
Alloy и TLA+ заточены под быстрое прототипирование высокоуровневых моделей (но при этом те же генераторы состояний и тесты инвариантов придется дублировать и для продакшн кода)
В общем, я все это не к тому, что "TLA не нужен" — мне этот подход очень даже понравился, в каком-то смысле есть ощущение, что это как бы следующая ступенька над обычными спецификациями и генеративными тестами по их мотивам, но просто ощущения скорее всего будет недостаточно, чтобы "продать" эту идею менеджменту, при том, что мы уже используем property-based тестирование.
Во-первых — спасибо за статью, много нового узнал. А во-вторых — пока читал не отпускала мысль: это очень похоже на property based testing, даже у Hillel Wayne в блоге оно неоднократно упоминается. Так вот, вопрос: даст ли какие-то преимущества использование Alloy/TLA+ по сравнению с написанием хорошо изолированной бизнес-логики, покрытой property based тестами? Понятно, что скорее всего на Alloy прототип можно набросать быстрее, чем даже на каком-нибудь питоне, но потом все равно придется писать реализацию, проверять на соответствие прототипу (глазами?) и крыть теми же тестами с проверками инвариантов — и разве генерация тест кейсов не даст те же плюшки, что и Alloy? Или там есть еще какие-то неочевидные преимущества?
Я не автор статьи, но ваш комментарий не мог меня оставить равнодушным.
а на какой срок вы заказывали сертификат? На 1 год?
В статье было явно указано — 3 года
вы потеряли около 30 дней. Рыночная стоимость 80$ в год (80/12=6$), именно эту сумму вы потеряли
Вы это серьезно? Отзыв сертификата — это серьезные репутационные и финансовые (если проект был монетизирован) потери для владельца.
Только что пробовали скачать и установить ваш софт, но сертификат не действителен, что говорит в пользу того, что другие центры не спешат выдавать вам сертификат. Никого не обвиняем, но это сухие факты.
Нет, это как раз завуалированное обвинение. Даже со стороны выглядит очень мерзко.
А теперь в целом — даже если автор статьи умышленно или неумышленно распространял малварь — вместо того, чтобы предоставить доказательства вы пользуетесь тактикой FUD, голословно втаптывая автора в грязь. Если прямо сейчас у вас нет доказательств — нейтральные ответы "мы разбираемся" были бы намного уместнее того, что вы тут развели.
Свои модули и фильтры — это хорошо, но почему не использовать роли и action-плагины? Роли пишутся на том же ансибле и могут вызывать модули и другие роли (в том числе с кастомными параметрами), и вполне поддаются интеграционному тестированию. Если хочется более сложную логику — есть action-плагины, которые с точки зрения плейбука выглядят как модули, но выполняются на стороне контроллера, а не хоста, и поэтому так же могут вызывать другие action-плагины и модули. Плюс за счёт того, что пишутся на питоне могут быть покрыты уже и юнит-тестами. А вот вызывать из своих модулей другие не получится — модули обязаны быть self-contained.
Не за что. Кстати, решил поискать не было ли статей на хабре про эту штуку, и внезапно — статья от Southbridge: habr.com/ru/company/southbridge/blog/306488. История действительно похоже циклична
А вы случайно не Decentralized Identifiers DID пытаетесь изобрести? Ну и вообще можно погуглить тему Self-Sovereign Identity...
Имхо есть шансы у Salt, особенно если появятся удобные средства модульного и интеграционного тестирования стейтов/формул. Да, есть плагин к kitchen — но это только интеграционное, и с multi-node там все грустно. И есть внутренняя система тестов — но если я правильно понимаю для тестирования своих стейтов их придется положить внутрь сальтовских исходников, что вообще за гранью...
Скажем так — у автора относительно большая задача, в которую нужно отдельно вникать, что отвлекает от изучения собственно инструмента, почти нет теории, сразу прыжок на абстракцию над TLA+ (т.е. PCAL). Что думал написать я — небольшое введение в принципы, стоящие за TLA+, и дальше очень простой практический пример в TDD стиле (начиная буквально с 3-х строчника на чистом TLA и заканчивая моделью выложенной на гитхаб), в процессе объясняя по мере необходимости как синтаксические конструкции, так и теоретические вещи типа концепций stuttering и weak/strong fairness.
Меня автор фактичски подцепил на TLA своей первой статьей, в качестве тренировки я реализовал (причем в TDD стиле) модель протокола надежной передачи сообщений в сети с возможными потерями, огреб в процессе всяких приколов и уже давно думаю запилить статью-туториал на эту тему, но не хватает мотивации. Если интерес есть — могу попробовать взять себя в руки и все-таки сделать ее.
P.S. Конечная версия "тренировочной" модели на чистом TLA+ и на PCAL есть на гитхабе: https://github.com/skhoroshavin/tla_playground
Ну на самом деле на Alloy тоже можно моделировать трейсы, аналогичные тем, что делает TLC (просто ввести некий time в структуру состояния системы с возможностью закольцовывания "суффикса" и наложить ограничения на возможнные переходы — аналог тех самых actions из TLA). Где-то даже статьи были на эту тему со сравнением перфоманса, и там тоже все неоднозначно. Если интересно — могу еще раз найти и кинуть ссылками.
Имхо — это больше похоже таки на backtrace. И что делать — после небольшой тренировки становится понятно.
Хм, а это не тот самый Niklas, который вел отличный блог про движок bitsquid, который в какой-то момент стал autodesk stingray, и у которого были весьма похожие статьи еще в 2010, 2011 и 2015?
Слышал, что в некоторых странах автомобильные радар-детекторы нелегальны, и "пользователей" вполне успешно ловят как раз по сигналу гетеродина.
Из того, что сам видел (nvidia, opengl):
Ну да. Например скининг сильно low-poly моделек (дальние LODы) бывает выгоднее на CPU считать. Другой пример — GUI.
В реалиях разработки под PC пытаться сделать stutter-free движок — это как ходить по минному полю. Очень легко нарваться на фризы в драйвере на миллисекунды или десятки миллисекунд:
Вроде как вулкан/DX12 как раз призваны избавить от таких неожиданностей, но в то же время эти API еще более низкоуровневые и сложные в использовании
Теоретически никто не запрещает в property-based тестах генерировать не случайные состояния, а вообще все (в пределах заданных ограничений), но из-за комбинаторного взрыва это может быть очень медленно. Если TLC тупо брутфорсит все пространство состояний — это ведь ничем не лучше, или там все-таки есть какие-то оптимизации? Alloy — да, за счет использования SAT-солвера может проверить пространство состояний гораздо быстрее, но как вы сами показали в статье далеко не все модели можно им проверить в принципе.
Питон тоже умеет очень даже декларативно и коротко:
Ну почему же? Вот пример такого теста для протокола binary agreement: https://github.com/poanetwork/hbbft/blob/master/tests/binary_agreement.rs#L64 Насчет учета классов эквивалентности — к сожалению, не уверен, что правильно понимаю о чем речь, можете показать пример и/или кинуть ссылкой почитать именно в этом контексте?
При наличии небольшого фреймворка такое можно провернуть и в "обычных" языках программирования. Вот пример теста, который проверяет кучу инвариантов для протокола смены лидера (в частности, упрощенно, что если он начался, то в итоге закончится и все запросы выполненные хотя бы на одной ноде окажутся в очереди на выполнение всеми нодами): https://github.com/hyperledger/indy-plenum/blob/master/plenum/test/consensus/test_sim_view_change.py#L9 Причем проверяет это непосредственно для продакшн-кода на большом количестве конфигураций, а за счет инъекции всех внешних зависимостей (в частности времени, шедулера и сетевого стека) тест работает повторяемо и достаточно быстро. Багов в начальной имплементации кстати этот тест наловил прилично.
К сожалению, пока я вижу только следующие плюсы (с оговорками):
В общем, я все это не к тому, что "TLA не нужен" — мне этот подход очень даже понравился, в каком-то смысле есть ощущение, что это как бы следующая ступенька над обычными спецификациями и генеративными тестами по их мотивам, но просто ощущения скорее всего будет недостаточно, чтобы "продать" эту идею менеджменту, при том, что мы уже используем property-based тестирование.
Во-первых — спасибо за статью, много нового узнал. А во-вторых — пока читал не отпускала мысль: это очень похоже на property based testing, даже у Hillel Wayne в блоге оно неоднократно упоминается. Так вот, вопрос: даст ли какие-то преимущества использование Alloy/TLA+ по сравнению с написанием хорошо изолированной бизнес-логики, покрытой property based тестами? Понятно, что скорее всего на Alloy прототип можно набросать быстрее, чем даже на каком-нибудь питоне, но потом все равно придется писать реализацию, проверять на соответствие прототипу (глазами?) и крыть теми же тестами с проверками инвариантов — и разве генерация тест кейсов не даст те же плюшки, что и Alloy? Или там есть еще какие-то неочевидные преимущества?
Могу ошибаться, но мне кажется, что pidar всё таки к матерным относится
Я не автор статьи, но ваш комментарий не мог меня оставить равнодушным.
В статье было явно указано — 3 года
Вы это серьезно? Отзыв сертификата — это серьезные репутационные и финансовые (если проект был монетизирован) потери для владельца.
Нет, это как раз завуалированное обвинение. Даже со стороны выглядит очень мерзко.
А теперь в целом — даже если автор статьи умышленно или неумышленно распространял малварь — вместо того, чтобы предоставить доказательства вы пользуетесь тактикой FUD, голословно втаптывая автора в грязь. Если прямо сейчас у вас нет доказательств — нейтральные ответы "мы разбираемся" были бы намного уместнее того, что вы тут развели.
Свои модули и фильтры — это хорошо, но почему не использовать роли и action-плагины? Роли пишутся на том же ансибле и могут вызывать модули и другие роли (в том числе с кастомными параметрами), и вполне поддаются интеграционному тестированию. Если хочется более сложную логику — есть action-плагины, которые с точки зрения плейбука выглядят как модули, но выполняются на стороне контроллера, а не хоста, и поэтому так же могут вызывать другие action-плагины и модули. Плюс за счёт того, что пишутся на питоне могут быть покрыты уже и юнит-тестами. А вот вызывать из своих модулей другие не получится — модули обязаны быть self-contained.