во всех этих server push меня смущает только пару вопросов:
1) клиенту может это все и не нужно (мобильный интернет)
2) у клиента уже есть эти данные закешированные, все что ему хочется знать это 304 NOT MODIFIED
не могу понять почему многие текущие разработки идут по принципу:
1) у пользователя простаивает cpu, надо его загрузить хоть чем-то
2) у пользователя простаивает канал в интернет, давайте мы по push закешируем весь сайт и пару поддоменов в нагрузку, может понадобится
ну дублирование не совсем корректное название, особенно что она очень легковесная, но хорошо.
по поводу друида: вы данные в него предполагали напрямую заливать?
просто везде где сталкивался с метриками мы гнали их через очередь, мало ли как индексатор себя поведет
независимо это cassandra/hbase/druid
1) HBase — Есть мастер нода – SPOF. мастеров в кластере несколько, выбираются кворумом, выпадение даже текущего не влияет на работу кластера (сам делал rolling restart всего кластера под нагрузкой, вышестоящие приложения лишь замечали небольшой скачек latency, драйвер сам детектил поведение и повторял запрос в новую ноду)
2) Druid — Долгове́чность — немного не понял, так как:
а) данные поступают в систему из kafka, пока блок не окажется в deepstorage то offset в kafka не комитится, данные всегда в очереди доступны
б) так как данные по большему immutable (сегменты полностью immutable, метаданные в реляционке лежат), то гарантии сохранности лежат или на deepstorage (это s3/hdfs зачастую) или как у вас резервирования sql базы сделано.
можете добавить сюда еще:
одно на нашем собственном Java-фреймворке, который основан на Spring и другое на kraken.js, с использованием express, dust.js и другого открытого кода.
никто не знает, кто что и как комитил в этот собственный фреймворк.
Отдельно смущает количество страниц в секунду, неужели там настолько тяжелые вызовы api?
причем стоит добавить, что aggregate с последующим «count: {$sum: 1}» работает на порядки медленнее, чем делать find(...).count() из-за особенностей реализации, разница в некоторых случаях у меня была миллисекунды-секунды vs минуты.
index используется в обоих случаях, но по разному
count может пробежаться по индексу и просто посчитать количество входов
агрегаты всегда производят материализацию объектов найденых, а уже потом только прибавляют 1, в итоге получаем fetch и disk io.
1. мы говорим о следующих пунктах:
а) интеллектуальная собственность (я тут полностью согласен с решением суда, вопрос по API возник бы рано или поздно, зато сейчас прецедент есть)
б) авторские права на код (не на сам язык, сам язык для разработки чего-либо никто не запрещал, копировать со сменой лицензии и вырезанием авторских прав есть запрет). Это если бы вы попытались использовать рантайм для Python/Lua от http://www.activestate.com/ и перетянули в свой «my-super-python-lua» дистрибутив стандартные библиотеки от них, а потом жаловались что вас за Python/Lua судят.
2. сам код openjdk под GPLv2, как и ядро linux, разрабатывай-открывай, либо не открывай, но тогда используй внутри не распространяя никому (хватает закрытых кастомных сборок jdk со специфическими патчами и никто никого не судит). GPL не означает «что хочу, то и делаю».
Вот поэтому за судом и следила вся индустрия, так как если бы судья сказал что «api действительно является ИС», то тогда бы попали все, нельзя было бы сделать ни одну стороннюю реализацию любого api, даже моки уже попадали бы под нарушение. Но судья попался грамотным и сказал обратное, поэтому все спят спокойно. Можно и реализовывать и применять.
А за копипасту со сменой лицензии доказали, что любой умный человек реализует почти таким же методом, вплоть до именования переменных.
Назовите пример открытых технологий, а то куда не посмотришь, то везде оказываются ограничения:
— ms за патенты в linux судиться,
— MPEG-LA за кодеки с гуглом (хотя тот считает что vp8-vp9 свободные кодеки),
— Yahoo! показывал что у него есть патенты на идею адблоков,
— про .net не говорю даже, там вообще все на «мы код открыли и обещаем за патенты не судить, честное слово» (почему тогда не открыли под нормальной лицензией, а то верить на слово ещё то удовольствие)
Поэтому и хотелось бы получить:
1) пример ОТКРЫТОЙ технологии
2) критерии открытости (свободно копировать, использовать, продавать изменения не показывая их)
ещё раз:
1) интеллектуальная собственность на API (тут все следили так как это касается не только google vs oracle, но и все в индустрии, так как процесс был знаковый)
2) авторское право на исходники (вопросы к копипасту с удалением headers об авторах и лицензии)
по второму подробней:
взять код под GPL лицензией и сказать, что теперь это apache лицензия и дальше вы если хотите, то сорцы закрывайте (а апач это позволяет) нельзя по условиям gpl, так как это нарушение, именно за это по второму пункту и были претензии.
Причем gpl => apache не относится конкретно к java, за это можно на любой gpl продукт попасть в суд, но никто же не говорит что gpl несвободная лицензия. Вернее говорят apache и bsd, что gpl недостаточно свободная, но каждый понимает свободу по своему.
то есть если есть сторонний продукт, который занимается раскидыванием jdk по машинкам в домене, но он платный хоть и можно скачать бесплатно, то это делает сразу же java несвободное технологией?
так под эту тему любое можно подвести:
1) .net несвободная технология, так как для нормальной работы если я скачаю нелицензионный windows мне ms счета выставит
2) js несвободная технология, так как за использование пиратского IE с windows для запуска ms опять счета выставит
3) sql несвободная технология, так как за его использование на oracle/db2/mssql некоторые компании счета выставляют
4) etc. можно продолжать аналогии до бесконечности
отличайте технологию и экосистему с продуктами
то что можно бесплатно скачать, не значит что данный продукт бесплатен
и уж тем более сторонние продукты не определяют свободность-открытость технологии
основные вопросы к Google были по 2 пунктам:
1) интеллектуальная собственность на API (тут все следили так как это касается не только google vs oracle, но и все индустрии)
2) авторское право на исходники (вопросы к копипасту с удалением headers об авторах)
видел =) за самим граалем уже давно посматриваю, хотя сейчас они планы чуть урезали, чтобы выйти сразу хоть с чем-то в прод, а уже потом добивать фичами
последнее время в этой части движение активное началось, помимо грааля зашевелились ibm http://www.eclipse.org/omr/
по осени дополнительно и свою версию jit открыли, в перспективе рассчитывают целиком свою версию jvm выложить и дальше двигаться по принципу Oracle «есть открытая версия, а есть наша сертифицированная с поддержкой, разница минимальная». http://openj9.mybluemix.net/
давно существуют алгоритмы и сборщики на подсчете ссылок, но у них есть свои проблемы:
1) атомарное увеличение-уменьшение количества ссылок не самая быстрая операция, а там нужна именно атомарная, так как часто мы не знаем куда убежала ссылка на объект и какие потоки еще держат данный объект
2) полностью вопроса с паузами он не снимает, хотя и делает на порядки более предсказуемым поведение.
Про второй пункт более подробно:
представьте что у Вас имеется структура в виде дерева и в программе держится только корень,
в какой-то момент корень выходит из зоны видимости и следовательно может быть собран,
после того как собран корень уменьшаются счетчики на объекты которые держались корнем и они тоже отправляются на удаление
и так проходит по всем элементам
в итоге у Вас возникает проблема, что выход из блока и инвалидация всего одной ссылки вызывает каскадную нагрузку на работу с памятью и очень часто предсказать Вы не можете в каком месте это выстрелит.
в классических языках с поколениями пройдет фаза mark и потом copy в новую область все кто выжил, а не будет вызываться пачка мелких удалений, просто пометим всю область как мусор и занулим.
p.s. известный факт: иногда из программы проще выйти по exit сразу в операционную систему, чем аккуратно освободить все участки памяти по очереди =) это касается любого managed языка
и верификация с математикой нам тут ничем не помогут, так как они не спасают от аппаратных сбоев, они не спасают от направленной атаки (Rowhammer уже приводил), они не спасают от направленного внедрения (когда человек сам запускает тот же вирус или он оказывается установленным еще на заводе изготовителе).
Shubinpavel уже вам ответил за космос: проблема зачастую в ресурсах (время, деньги, человеки) когда сознательно идут на срезание улов и уход от поставленных требований к проверке надежности, но чтобы было хоть что-то, а не воздушные замки в мечтах.
NASA имеет бюджет, любой спутник или ракета имеет бюджет, поэтому иногда возможно рискнуть и попытаться запустить сейчас с вероятностью неудачи в 0.001% чем пропустить запуск и ждать следующих 4-5 лет для появления окна запуска. В случае неудачи у вас есть риск строить такой же аппарат еще 8 лет, но это сознательный риск.
Не задумывались почему даже на Curiosity обновление прошивки заливали уже после достижения Марса: в момент отправки оно просто не было готово, не хватает ресурсов.
Написали мы софт, верифицировали, а потом
1) трактористы Васи порвали экскаватором оптику (реальный случай пропадания аплинка между РБ и Россией, в тот момент там свыше 50% всего внешнего канала было, сколько рвут кабелей океанических вообще помолчим).
2) ударили молнии и вторая половина датацентров легла (случай с амазоном)
Распределенные технологии, такие как интернет, по определению строятся на ненадежных системах, чем больше узлов в системе тем выше вероятность отказа. Поэтому для интернета стоит задача другая: как из ненадежных элементов построить достаточно устойчивую систему. Отмирание отдельной клетки не убивает организм (рак отдельная песня, но и с ним частично борются), выпадение одного сервера не ложит yandex/google/facebook (для них вылеты целиком стоек никак не сказываются на работе, даже падение целого датацентра не остановит работу). Те же DDoS это полностью правильная работа, но датацентр можно положить, тут не спасет никакая верификация.
Поэтому отдельные части верифицировать можно, но чем крупнее система, тем больше нужно полагаться на общую устойчивость, а не на то, что у нас каждый элемент будет работать правильно и идеально и никогда не сбоить.
использовать ненадежный МРТ сейчас за цену Х
или его появление в 10 клиниках в мире через 20 лет за цену 1000*X
я выбираю первый вариант, так как в некоторых случаях это нужно здесь и сейчас, а не через год, не говоря уже о больших сроках. многие новые разработки являются уникальными, либо используют новые физ-мат модели и переиспользовать просто нечего, поэтому фраза оказывается ложной:
>> Заоблачной стоимость будет только если каждый производитель каждый раз будет заново писать и верифицировать весь свой код, а если будут использованы ранее верифицированные открытые компоненты, то стоимость вырастет не сильно.
даже с обычной жизни мы постоянно сталкиваемся с вероятностями в медицине:
экспресс тесты на беременность/ВИЧ/диабет.
и вот тут мы начинаем спускаться уже глубже:
ядро для os для атомных, космических и медицинских вещей и так далеко не обычное используется, говорить, что там меньше архитектур и fs я бы точно не стал, так как хватает всего, поэтому и разработки такие дорогие, что продукты очень часто близки к уникальным или тираж очень маленький.
«а всё остальное на условном кроссплатформенном хаскеле нужно писать» — все любят повторять это как мантру, раз математический язык, то все хорошо, но почему-то все забывают уточнять, что как только поменялась немного модель данных, то с хаскелем все очень весело становится, про разворачивание ошибок компиляции отдельный вопрос (это все вытекает из математики).
иногда проще поступить по принципу эрланга: если что-то падает, дай ему упасть.
Но в нашем случае продолжаем работать и принимать решения уже на оставшихся данных, так как любая физическая сущность всегда может упасть или начать возвращать неправильные данные (можете посмотреть количество сбоев обычной RAM в датацентрах, интересная статистика, посмотрите на последние уязвимости Rowhammer), то есть ваша программа формально будет вести себя правильно, но данные ей будут поступать некорректные.
вот тут подходим к другому пункту:
верифицированный L4 это по сути минимальный гипервизор, который почти ничего не умеет.
В самом linux kernel от ядра как таковое совсем малый процент
первое место по объему это драйвера
дальше уже arch (все-таки количество поддерживаемых архитектур зашкаливает, сравните с seL4 который 4 вида arm и одни ia32 тянет)
и третье место за fs.
то есть формализовать только какой-то subset от ядра не проблема даже для монолита.
а вот формализовать все ядро действительно нету шансов
к тому же если посмотрите на последние уязвимости-ошибки, то окажется что по отдельности они не несут никаких деструктивных вещей, зачастую это даже ожидаемое их поведение, но вот грамотное построение цепочек из 10-15 таких недоуязвимостей создают большую дыру и тут даже верификация и микроядро не поможет, так как каждое из действий будет считаться допустимым, а истинная проблема возникнет на стыковке и объединении всех модулей
>> В новую версию принято более 13 тысяч исправлений от примерно 1500 разработчиков, размер патча — 41 Мб (изменения затронули 11303 файлов, добавлено 627751 строк кода, удалено 278958 строк).
вопрос: сколько людей и сколько времени будет проходить верификация только нового кода?
8700 строк кода — 12 человек — 4 года
348793 новых строк кода — ? человек — ? лет
дополнительно учитываем, что сложность верификации совсем нелинейна относительно объема кода (лично я допускаю что ближе к экспоненте)
Да, многие вещи в ядре дублируются и тд, тех же fs вагон и маленькая тележка, но все они кому-то нужны, так как специализированны под конкретные требования, нельзя написать одну fs которая удовлетворит всех, а потом её верифицировать и все счастливые.
p.s. сам регулярно прогоняю статический анализ по своему код, но это далеко не верификация, так как она будет не просто дорого, а очень дорого, проще переписать 10 раз с нуля под изменившиеся требования, чем 10 лет пилить морально устаревшее решение
>> Опять не понял, но сейчас в InFilter просто запрос в Set, скорее всего HashSet
посыпаю голову пеплом, уже пофиксили (к версии 0.9.2) =) но это было всего 2 марта, если откроете фикс который он делал, то там хорошо написано: Currently, InDimFilter is translated to «or + selector filters». Value matcher can use hash set for faster filtering.
List<DimFilter> fields = Lists.<DimFilter>newArrayList(new SelectorDimFilter(dimensionName, value));
for (String val : values) {
fields.add(new SelectorDimFilter(dimensionName, val));
}
dimFilter = new OrDimFilter(fields);
Обратите внимание на ValueMatcher: он последовательно применяет для каждого selector проверку пока кто-то не сработает. На больших объемах в IN это было достаточно плохо.
В принципе сейчас действительно уже проще, когда смотрел плотно эту часть, там с интерфейсами конкретно под эту задачу было сложнее. Сейчас же просто проверку вместо Set на что-то еще сделать не проблема, а если добавить какой bloom для больших наборов так вообще может оказаться очень хорошо.
>> А можно тут подробнее? Это какой тип запроса?
вот так сразу не вспомню точно условия, но насколько помню было «granularity»: «all» и порядочно сегментов.
1) клиенту может это все и не нужно (мобильный интернет)
2) у клиента уже есть эти данные закешированные, все что ему хочется знать это 304 NOT MODIFIED
не могу понять почему многие текущие разработки идут по принципу:
1) у пользователя простаивает cpu, надо его загрузить хоть чем-то
2) у пользователя простаивает канал в интернет, давайте мы по push закешируем весь сайт и пару поддоменов в нагрузку, может понадобится
по поводу друида: вы данные в него предполагали напрямую заливать?
просто везде где сталкивался с метриками мы гнали их через очередь, мало ли как индексатор себя поведет
независимо это cassandra/hbase/druid
1) HBase — Есть мастер нода – SPOF. мастеров в кластере несколько, выбираются кворумом, выпадение даже текущего не влияет на работу кластера (сам делал rolling restart всего кластера под нагрузкой, вышестоящие приложения лишь замечали небольшой скачек latency, драйвер сам детектил поведение и повторял запрос в новую ноду)
2) Druid — Долгове́чность — немного не понял, так как:
а) данные поступают в систему из kafka, пока блок не окажется в deepstorage то offset в kafka не комитится, данные всегда в очереди доступны
б) так как данные по большему immutable (сегменты полностью immutable, метаданные в реляционке лежат), то гарантии сохранности лежат или на deepstorage (это s3/hdfs зачастую) или как у вас резервирования sql базы сделано.
если я что-то неправильно понял, то уточните
одно на нашем собственном Java-фреймворке, который основан на Spring и другое на kraken.js, с использованием express, dust.js и другого открытого кода.
никто не знает, кто что и как комитил в этот собственный фреймворк.
Отдельно смущает количество страниц в секунду, неужели там настолько тяжелые вызовы api?
index используется в обоих случаях, но по разному
count может пробежаться по индексу и просто посчитать количество входов
агрегаты всегда производят материализацию объектов найденых, а уже потом только прибавляют 1, в итоге получаем fetch и disk io.
поэтому сравнения вообще ни о чём =)
а) интеллектуальная собственность (я тут полностью согласен с решением суда, вопрос по API возник бы рано или поздно, зато сейчас прецедент есть)
б) авторские права на код (не на сам язык, сам язык для разработки чего-либо никто не запрещал, копировать со сменой лицензии и вырезанием авторских прав есть запрет). Это если бы вы попытались использовать рантайм для Python/Lua от http://www.activestate.com/ и перетянули в свой «my-super-python-lua» дистрибутив стандартные библиотеки от них, а потом жаловались что вас за Python/Lua судят.
2. сам код openjdk под GPLv2, как и ядро linux, разрабатывай-открывай, либо не открывай, но тогда используй внутри не распространяя никому (хватает закрытых кастомных сборок jdk со специфическими патчами и никто никого не судит). GPL не означает «что хочу, то и делаю».
А за копипасту со сменой лицензии доказали, что любой умный человек реализует почти таким же методом, вплоть до именования переменных.
Назовите пример открытых технологий, а то куда не посмотришь, то везде оказываются ограничения:
— ms за патенты в linux судиться,
— MPEG-LA за кодеки с гуглом (хотя тот считает что vp8-vp9 свободные кодеки),
— Yahoo! показывал что у него есть патенты на идею адблоков,
— про .net не говорю даже, там вообще все на «мы код открыли и обещаем за патенты не судить, честное слово» (почему тогда не открыли под нормальной лицензией, а то верить на слово ещё то удовольствие)
Поэтому и хотелось бы получить:
1) пример ОТКРЫТОЙ технологии
2) критерии открытости (свободно копировать, использовать, продавать изменения не показывая их)
1) интеллектуальная собственность на API (тут все следили так как это касается не только google vs oracle, но и все в индустрии, так как процесс был знаковый)
2) авторское право на исходники (вопросы к копипасту с удалением headers об авторах и лицензии)
по второму подробней:
взять код под GPL лицензией и сказать, что теперь это apache лицензия и дальше вы если хотите, то сорцы закрывайте (а апач это позволяет) нельзя по условиям gpl, так как это нарушение, именно за это по второму пункту и были претензии.
Причем gpl => apache не относится конкретно к java, за это можно на любой gpl продукт попасть в суд, но никто же не говорит что gpl несвободная лицензия. Вернее говорят apache и bsd, что gpl недостаточно свободная, но каждый понимает свободу по своему.
так под эту тему любое можно подвести:
1) .net несвободная технология, так как для нормальной работы если я скачаю нелицензионный windows мне ms счета выставит
2) js несвободная технология, так как за использование пиратского IE с windows для запуска ms опять счета выставит
3) sql несвободная технология, так как за его использование на oracle/db2/mssql некоторые компании счета выставляют
4) etc. можно продолжать аналогии до бесконечности
отличайте технологию и экосистему с продуктами
то что можно бесплатно скачать, не значит что данный продукт бесплатен
и уж тем более сторонние продукты не определяют свободность-открытость технологии
основные вопросы к Google были по 2 пунктам:
1) интеллектуальная собственность на API (тут все следили так как это касается не только google vs oracle, но и все индустрии)
2) авторское право на исходники (вопросы к копипасту с удалением headers об авторах)
последнее время в этой части движение активное началось, помимо грааля зашевелились ibm
http://www.eclipse.org/omr/
по осени дополнительно и свою версию jit открыли, в перспективе рассчитывают целиком свою версию jvm выложить и дальше двигаться по принципу Oracle «есть открытая версия, а есть наша сертифицированная с поддержкой, разница минимальная». http://openj9.mybluemix.net/
в
>> Начиная с Java 9, Graal можно использовать как JVM плагин.
первичная идея была предоставить интерфейс JIT для поддержки сторонних реализаций
http://openjdk.java.net/jeps/243
Но есть сборки jvmci и для java 8, так что при желании можно гонять уже сейчас
>> А следующие части не относятся к OpenSource
>> Поддержка AOT
но тут пошли поезда от Марка Райнхольда и случился http://openjdk.java.net/jeps/295
в итоге core часть от graal уже войдет и в кодовую базу java 9
1) атомарное увеличение-уменьшение количества ссылок не самая быстрая операция, а там нужна именно атомарная, так как часто мы не знаем куда убежала ссылка на объект и какие потоки еще держат данный объект
2) полностью вопроса с паузами он не снимает, хотя и делает на порядки более предсказуемым поведение.
Про второй пункт более подробно:
представьте что у Вас имеется структура в виде дерева и в программе держится только корень,
в какой-то момент корень выходит из зоны видимости и следовательно может быть собран,
после того как собран корень уменьшаются счетчики на объекты которые держались корнем и они тоже отправляются на удаление
и так проходит по всем элементам
в итоге у Вас возникает проблема, что выход из блока и инвалидация всего одной ссылки вызывает каскадную нагрузку на работу с памятью и очень часто предсказать Вы не можете в каком месте это выстрелит.
в классических языках с поколениями пройдет фаза mark и потом copy в новую область все кто выжил, а не будет вызываться пачка мелких удалений, просто пометим всю область как мусор и занулим.
p.s. известный факт: иногда из программы проще выйти по exit сразу в операционную систему, чем аккуратно освободить все участки памяти по очереди =) это касается любого managed языка
Верифицировать и гарантировать работу ВСЕХ составляющих дорого, долго и не имеет смысла.
Shubinpavel уже вам ответил за космос: проблема зачастую в ресурсах (время, деньги, человеки) когда сознательно идут на срезание улов и уход от поставленных требований к проверке надежности, но чтобы было хоть что-то, а не воздушные замки в мечтах.
NASA имеет бюджет, любой спутник или ракета имеет бюджет, поэтому иногда возможно рискнуть и попытаться запустить сейчас с вероятностью неудачи в 0.001% чем пропустить запуск и ждать следующих 4-5 лет для появления окна запуска. В случае неудачи у вас есть риск строить такой же аппарат еще 8 лет, но это сознательный риск.
Не задумывались почему даже на Curiosity обновление прошивки заливали уже после достижения Марса: в момент отправки оно просто не было готово, не хватает ресурсов.
1) трактористы Васи порвали экскаватором оптику (реальный случай пропадания аплинка между РБ и Россией, в тот момент там свыше 50% всего внешнего канала было, сколько рвут кабелей океанических вообще помолчим).
2) ударили молнии и вторая половина датацентров легла (случай с амазоном)
Распределенные технологии, такие как интернет, по определению строятся на ненадежных системах, чем больше узлов в системе тем выше вероятность отказа. Поэтому для интернета стоит задача другая: как из ненадежных элементов построить достаточно устойчивую систему. Отмирание отдельной клетки не убивает организм (рак отдельная песня, но и с ним частично борются), выпадение одного сервера не ложит yandex/google/facebook (для них вылеты целиком стоек никак не сказываются на работе, даже падение целого датацентра не остановит работу). Те же DDoS это полностью правильная работа, но датацентр можно положить, тут не спасет никакая верификация.
Поэтому отдельные части верифицировать можно, но чем крупнее система, тем больше нужно полагаться на общую устойчивость, а не на то, что у нас каждый элемент будет работать правильно и идеально и никогда не сбоить.
или его появление в 10 клиниках в мире через 20 лет за цену 1000*X
я выбираю первый вариант, так как в некоторых случаях это нужно здесь и сейчас, а не через год, не говоря уже о больших сроках. многие новые разработки являются уникальными, либо используют новые физ-мат модели и переиспользовать просто нечего, поэтому фраза оказывается ложной:
>> Заоблачной стоимость будет только если каждый производитель каждый раз будет заново писать и верифицировать весь свой код, а если будут использованы ранее верифицированные открытые компоненты, то стоимость вырастет не сильно.
даже с обычной жизни мы постоянно сталкиваемся с вероятностями в медицине:
экспресс тесты на беременность/ВИЧ/диабет.
и вот тут мы начинаем спускаться уже глубже:
ядро для os для атомных, космических и медицинских вещей и так далеко не обычное используется, говорить, что там меньше архитектур и fs я бы точно не стал, так как хватает всего, поэтому и разработки такие дорогие, что продукты очень часто близки к уникальным или тираж очень маленький.
«а всё остальное на условном кроссплатформенном хаскеле нужно писать» — все любят повторять это как мантру, раз математический язык, то все хорошо, но почему-то все забывают уточнять, что как только поменялась немного модель данных, то с хаскелем все очень весело становится, про разворачивание ошибок компиляции отдельный вопрос (это все вытекает из математики).
иногда проще поступить по принципу эрланга: если что-то падает, дай ему упасть.
Но в нашем случае продолжаем работать и принимать решения уже на оставшихся данных, так как любая физическая сущность всегда может упасть или начать возвращать неправильные данные (можете посмотреть количество сбоев обычной RAM в датацентрах, интересная статистика, посмотрите на последние уязвимости Rowhammer), то есть ваша программа формально будет вести себя правильно, но данные ей будут поступать некорректные.
верифицированный L4 это по сути минимальный гипервизор, который почти ничего не умеет.
В самом linux kernel от ядра как таковое совсем малый процент
первое место по объему это драйвера
дальше уже arch (все-таки количество поддерживаемых архитектур зашкаливает, сравните с seL4 который 4 вида arm и одни ia32 тянет)
и третье место за fs.
то есть формализовать только какой-то subset от ядра не проблема даже для монолита.
а вот формализовать все ядро действительно нету шансов
к тому же если посмотрите на последние уязвимости-ошибки, то окажется что по отдельности они не несут никаких деструктивных вещей, зачастую это даже ожидаемое их поведение, но вот грамотное построение цепочек из 10-15 таких недоуязвимостей создают большую дыру и тут даже верификация и микроядро не поможет, так как каждое из действий будет считаться допустимым, а истинная проблема возникнет на стыковке и объединении всех модулей
>> В новую версию принято более 13 тысяч исправлений от примерно 1500 разработчиков, размер патча — 41 Мб (изменения затронули 11303 файлов, добавлено 627751 строк кода, удалено 278958 строк).
вопрос: сколько людей и сколько времени будет проходить верификация только нового кода?
8700 строк кода — 12 человек — 4 года
348793 новых строк кода — ? человек — ? лет
дополнительно учитываем, что сложность верификации совсем нелинейна относительно объема кода (лично я допускаю что ближе к экспоненте)
Да, многие вещи в ядре дублируются и тд, тех же fs вагон и маленькая тележка, но все они кому-то нужны, так как специализированны под конкретные требования, нельзя написать одну fs которая удовлетворит всех, а потом её верифицировать и все счастливые.
p.s. сам регулярно прогоняю статический анализ по своему код, но это далеко не верификация, так как она будет не просто дорого, а очень дорого, проще переписать 10 раз с нуля под изменившиеся требования, чем 10 лет пилить морально устаревшее решение
посыпаю голову пеплом, уже пофиксили (к версии 0.9.2) =) но это было всего 2 марта, если откроете фикс который он делал, то там хорошо написано: Currently, InDimFilter is translated to «or + selector filters». Value matcher can use hash set for faster filtering.
Or в свою очередь доходит до OrFilter
Обратите внимание на ValueMatcher: он последовательно применяет для каждого selector проверку пока кто-то не сработает. На больших объемах в IN это было достаточно плохо.
В принципе сейчас действительно уже проще, когда смотрел плотно эту часть, там с интерфейсами конкретно под эту задачу было сложнее. Сейчас же просто проверку вместо Set на что-то еще сделать не проблема, а если добавить какой bloom для больших наборов так вообще может оказаться очень хорошо.
>> А можно тут подробнее? Это какой тип запроса?
вот так сразу не вспомню точно условия, но насколько помню было «granularity»: «all» и порядочно сегментов.