У людей вообще в принципе не получается писать "надежные и поддерживаемые программы" в смысле гарантированного отсутствия багов, если они начинают превышать размер в 10К строк.
Даже с привлечением отдельных институтов, которые могут годами делать "математически обоснованную" формальную верификацию, для тех же 10К строк. И CoQ и прочие "облегчалки", в корне ничего не меняют, солверы взрываются, сложность верификации с определенного объема(обычно как раз те самые 3-10К) начинает расти экспоненциально. Особенно если мы говорим о реальной системе с побочными эффектами.
"seL4, a third-generation microkernel of L4 provenance, comprises 8,700 lines of C code and 600 lines of assembler. Its performance is comparable to other high-performance L4 kernels."
"The project was conducted in three phases. First an initial kernel with limited functionality (no inter- rupts, single address space and generic linear page ta- ble) was designed and implemented in Haskell, while the verification team mostly worked on the verifi-cation framework and generic proof libraries. In a second phase, the verification team developed the abstract spec and performed the first refinement while the development team completed the design, Haskell prototype and C implementation. The third phase consisted of extending the first refinement step to the full kernel and performing the second refinement. The overall size of the proof, including framework, libraries, and generated proofs (not shown in the table) is 200,000 lines of Isabelle script."
Конечно я не большой специалист в вопросе, но тут есть как минимум два фактора, это деградация полупроводникового материала под воздействием излучения, и второй вероятность единичных сбоев под воздействием космической радиации.
Последний фактор даже в земных условиях имеет место быть, поэтому в сервера стараются ставить ECC память.
В общем случаи, процессор это изначально полностью детерминированная система, состоящая из десятков или сотен миллионов логических вентилей и ячеек памяти(триггеры, регистры, статическая память), к тому же практически всегда конвейеризированная. В принципе, достаточно единичного bit flip, в не удобном месте(как в логике так и памяти), чтобы это привело к катастрофическим последствиям, конечно не сгорит, но "зависнуть" или перевести систему в невалидное состояние может.
Если мы примем вероятность отсутствия сбоя в течении такта на единичном элементе p, то отсутствие сбоя во всех элементах это p^n(при n=10^7), или вероятность сбоя: 1 - p^n. Достаточно очевидно, что даже относительно не большое увеличение вероятности сбоя единичного элемента, может вести к катастрофическим последствиям для параметров надежности всей системы.
Единственная причина, почему эта махина относительно надежно работает, состоит в том, что она изначально была спроектирована, с учетом воздействия различных факторов в земных условиях. В том числе целостности сигнала, начиная от техпроцесса, и кончая DRC(design rule check), в процессе разработки.
Одним из ключевых "защитных" факторов, от космической радиации является магнитное поле земли, которое очевидно будет нелинейно менять ее интенсивность в зависимости от высоты. Поэтому low earth orbit и толстые стенки МКС, это совсем не тоже самое, что и спутник на более высокой орбите.
Уверен что никакую статистику собирать и не надо, так как это все должно довольно реалистично воспроизводиться в лабораторных условиях.
Чисто из моих наблюдений. Не компетентные программисты, на больших проектах, пишут одинаково не масштабируемый говнокод, что на Си, что на плюсах. При этом часто ловишь себя на мысле, уж лучше бы на плюсах писали, там хотя бы есть из коробки, не такие ужасные строки, контейнеры и управление ресурсами(RAII и умные указатели). Да и объектность, хотя бы в какой-то мере мотивирует разбрасывать функционал по классам, а не писать сплошную лапшу.
Или если вы предполагаете, подобный ход развития событий, лучше сразу взять какую ни буть Java или С#.
Такой код обычно, не плохо оптимизируется numba, приближаясь по скорости к нативному. Но разве это кого-то волнует, когда стоит цель переписать на раст.
Лично я не фанат раста, но еcли быть честным, то почти весь unsafe это взаимодействие со сторонними библиотеками, в частности PAM API. В этом собственно и лежит одна из проблем "переписывания" на раст, пока вся система не замкнута на раст или хорошо изолированна, будут торчать unsafe. Но вообще это проблема любого интеропа.
Еще и "call" с "ret" и оптимизация в OoO. Плюсом дополнительный интероп с кодом с другим ABI, допилить TLS, и прочие манипуляции со стэком вроде эмуляции контекста и корутин. Особой потери не будет но в районе десятка процентов вполне.
Так осталось дело за малым, реализовать работоспособный прототип, в процессе чего возникнут еще подводные камни. Замерить падение производительности. И убедить людей это использовать. Но в среднем люди не очень любят, когда им предлагают лечить перхоть гильотиной.
PS: начать можно с анализа, можно ли в принципе сделать защищенный стек содержащий только адреса возврата, на x64.
Так речь шла про x86/x64 я не уверен, что защищенный стек там можно в принципе реализовать(защитой страниц, сегментов или чего угодно), даже если принять накладные расходы на второй стек для данных. А так да есть железки с защитой от подмены адресов возврата.
Это ломает кучу ABI. По поводу последствий подобного подхода надо смотреть на реальный прототип, хотябы исследовательский, которого нет, и думаю ни просто так. А не рассуждать о преимуществах сферического коня в ваккуме. Тем более что последствия от подобных уязвимостей в определенноц степени закрываются NX битом, но конечно не до конца.
К сожалению в x86/x64 один железнячный стек, а реализация в софте второго скорее всего ведет к различным неприятным последствиям, в плане производительности и совместимости. Данная концепция насколько я знаю нигде не была реализованна ни только M$.
Причем тут стэк и адреса возврата? Вообщето одним из основных нововведений защищенного режима была страничная адресация, позволяющая создать плоское защищенное виртуальное адресное пространство процесса. А сегменты это анахронизм, который давно закопали, и не в одной современной ОС, прежде всего *nix они не используются.
PS: если вы про аллокацию локальных переменных на стеке, то это стандартная реализация семантики большинства нативных языков программирования, в частности Си, и его потомков. Теоретически можно делать два стека один под адреса возврата, другой под данные, но такого в процессоре физически нет, и видимо концепция ни очень прижилась.
Под моделью данных я как раз имел ввиду, нормализованное хранилище состояния/данных приложения, а не стандартные model/view из qt. Слой данных реализует доступ к данным, обновление состояния и набор событий связанных с его обновлением, и по сути полностью изолирован от UI. Так что тут я с вами полностью согласен, чем меньше состояния внутри компонентов UI тем лучше.
Собственно, хорошо построенная архитектура в вебе, примерно этому и соответствует: бэкенд(модель данных)/фронтенд(UI для ее отображения). Поэтому если у вас есть проблемы с состоянием(в частности глобальном) в UI, то изначальный вопрос, зачем оно там взялось. (нет состояния - нет "разрывов" логики, что есть то и отобразили)
Да, тут конечно возникает часто необходимость локальности данных, так как ходить на каждый чих в бэкенд может быть дорого, но это вполне решается в рамках той же парадигмы: Глобальная модель данных <-синхронизация-> Локальная модель данных <-> Отображение UI.
Расскажу как решались подобные проблемы в десктопных UI(думаю и в вебе можно смастерить плюс-минус тоже самое).
Вся "архитектура" пилилась на два слоя, условно один слой глобального состояния и модели данных приложения, второй непосредственно UI.
Модель данных имела методы получения из нее и обновления состояния, а так же события обновления различных частей модели на которые мог подписаться любой желающий(стандартный signal-slot в Qt). Слой UI, состоял из относительно крупных компонентов, отображающих какие-то сильно связанные куски интерфейса, и которые внутри управляли уже базовыми примитивами UI(кнопки, лэйблы, и т.д.).
Компоненты UI подписывались на нужный для каждого из них набор событий из слоя данных, и вызывали его методы для модификации состояния. При изменении состояния, дергались связанные с ними события, которые прилетали ко всем подписанным компонентам UI, которые умели себя из этой модели данных обновить. UI старались максимально избавить от собственного состояния и перенести его в модель данных.
Если какие-то данные были внешними, то внутри модели данных после запроса на обновление, можно было куда-то сходить, и вызвать нужные события на обновление когда новые данные пришли и изменили модель.
Подобное решение было простое, как палка и достаточно легко масштабировалось.
PS: классический MVC паттерн как по мне, вообще не сильно полезная штука
У людей вообще в принципе не получается писать "надежные и поддерживаемые программы" в смысле гарантированного отсутствия багов, если они начинают превышать размер в 10К строк.
Даже с привлечением отдельных институтов, которые могут годами делать "математически обоснованную" формальную верификацию, для тех же 10К строк. И CoQ и прочие "облегчалки", в корне ничего не меняют, солверы взрываются, сложность верификации с определенного объема(обычно как раз те самые 3-10К) начинает расти экспоненциально. Особенно если мы говорим о реальной системе с побочными эффектами.
Есть реальные примеры, подобной верификации например seL4, и пэйпер, если кто-то думает что я преувеличиваю. https://www.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf
"seL4, a third-generation microkernel of L4 provenance, comprises 8,700 lines of C code and 600 lines of assembler. Its performance is comparable to other high-performance L4 kernels."
"The project was conducted in three phases. First an initial kernel with limited functionality (no inter- rupts, single address space and generic linear page ta-
ble) was designed and implemented in Haskell, while the verification team mostly worked on the verifi-cation framework and generic proof libraries. In a
second phase, the verification team developed the abstract spec and performed the first refinement while the development team completed the design, Haskell
prototype and C implementation. The third phase consisted of extending the first refinement step to the full kernel and performing the second refinement.
The overall size of the proof, including framework, libraries, and generated proofs (not shown in the table) is 200,000 lines of Isabelle script."
По поводу CStr и free, подозревая, что это защита от того, что могли быть использованы разные аллокаторы памяти внутри раста, и системной glibc.
Конечно я не большой специалист в вопросе, но тут есть как минимум два фактора, это деградация полупроводникового материала под воздействием излучения, и второй вероятность единичных сбоев под воздействием космической радиации.
Последний фактор даже в земных условиях имеет место быть, поэтому в сервера стараются ставить ECC память.
В общем случаи, процессор это изначально полностью детерминированная система, состоящая из десятков или сотен миллионов логических вентилей и ячеек памяти(триггеры, регистры, статическая память), к тому же практически всегда конвейеризированная. В принципе, достаточно единичного bit flip, в не удобном месте(как в логике так и памяти), чтобы это привело к катастрофическим последствиям, конечно не сгорит, но "зависнуть" или перевести систему в невалидное состояние может.
Если мы примем вероятность отсутствия сбоя в течении такта на единичном элементе p, то отсутствие сбоя во всех элементах это p^n(при n=10^7), или вероятность сбоя: 1 - p^n. Достаточно очевидно, что даже относительно не большое увеличение вероятности сбоя единичного элемента, может вести к катастрофическим последствиям для параметров надежности всей системы.
Единственная причина, почему эта махина относительно надежно работает, состоит в том, что она изначально была спроектирована, с учетом воздействия различных факторов в земных условиях. В том числе целостности сигнала, начиная от техпроцесса, и кончая DRC(design rule check), в процессе разработки.
Одним из ключевых "защитных" факторов, от космической радиации является магнитное поле земли, которое очевидно будет нелинейно менять ее интенсивность в зависимости от высоты. Поэтому low earth orbit и толстые стенки МКС, это совсем не тоже самое, что и спутник на более высокой орбите.
Уверен что никакую статистику собирать и не надо, так как это все должно довольно реалистично воспроизводиться в лабораторных условиях.
Чисто из моих наблюдений. Не компетентные программисты, на больших проектах, пишут одинаково не масштабируемый говнокод, что на Си, что на плюсах. При этом часто ловишь себя на мысле, уж лучше бы на плюсах писали, там хотя бы есть из коробки, не такие ужасные строки, контейнеры и управление ресурсами(RAII и умные указатели). Да и объектность, хотя бы в какой-то мере мотивирует разбрасывать функционал по классам, а не писать сплошную лапшу.
Или если вы предполагаете, подобный ход развития событий, лучше сразу взять какую ни буть Java или С#.
Такой код обычно, не плохо оптимизируется numba, приближаясь по скорости к нативному. Но разве это кого-то волнует, когда стоит цель переписать на раст.
Лично я не фанат раста, но еcли быть честным, то почти весь unsafe это взаимодействие со сторонними библиотеками, в частности PAM API. В этом собственно и лежит одна из проблем "переписывания" на раст, пока вся система не замкнута на раст или хорошо изолированна, будут торчать unsafe. Но вообще это проблема любого интеропа.
Вы правда думаете, что rad-hard ставят на спутники потому, что они там все "тупые" и ничего не понимают?
Наши бы вояки, к примеру, с удовольствием запустили бы обычные процы в космос, а не rad-hard, которых просто нет.
PS: вообще подход сэкономить 200K$ и повысить провал миссии из-за электроники на несколько порядков, эффективные менеджеры одобряют.
Да вы правы, сам язык около 150 страниц, я в какойто переформатированный драфт ткнулся.
я даже ради интереса скачал C99, сам язык - 70 страниц, +70 страниц библиотека. Но да, не 2000. "кресты" сам язык около 400 страниц.
Еще и "call" с "ret" и оптимизация в OoO. Плюсом дополнительный интероп с кодом с другим ABI, допилить TLS, и прочие манипуляции со стэком вроде эмуляции контекста и корутин. Особой потери не будет но в районе десятка процентов вполне.
Так осталось дело за малым, реализовать работоспособный прототип, в процессе чего возникнут еще подводные камни. Замерить падение производительности. И убедить людей это использовать. Но в среднем люди не очень любят, когда им предлагают лечить перхоть гильотиной.
PS: начать можно с анализа, можно ли в принципе сделать защищенный стек содержащий только адреса возврата, на x64.
Так речь шла про x86/x64 я не уверен, что защищенный стек там можно в принципе реализовать(защитой страниц, сегментов или чего угодно), даже если принять накладные расходы на второй стек для данных. А так да есть железки с защитой от подмены адресов возврата.
Это ломает кучу ABI. По поводу последствий подобного подхода надо смотреть на реальный прототип, хотябы исследовательский, которого нет, и думаю ни просто так. А не рассуждать о преимуществах сферического коня в ваккуме. Тем более что последствия от подобных уязвимостей в определенноц степени закрываются NX битом, но конечно не до конца.
Для устойчивой работоспособности данных компаний, скорее важны различные SCADA и промышленные системы.
К сожалению в x86/x64 один железнячный стек, а реализация в софте второго скорее всего ведет к различным неприятным последствиям, в плане производительности и совместимости. Данная концепция насколько я знаю нигде не была реализованна ни только M$.
Причем тут стэк и адреса возврата? Вообщето одним из основных нововведений защищенного режима была страничная адресация, позволяющая создать плоское защищенное виртуальное адресное пространство процесса. А сегменты это анахронизм, который давно закопали, и не в одной современной ОС, прежде всего *nix они не используются.
PS: если вы про аллокацию локальных переменных на стеке, то это стандартная реализация семантики большинства нативных языков программирования, в частности Си, и его потомков. Теоретически можно делать два стека один под адреса возврата, другой под данные, но такого в процессоре физически нет, и видимо концепция ни очень прижилась.
Под моделью данных я как раз имел ввиду, нормализованное хранилище состояния/данных приложения, а не стандартные model/view из qt. Слой данных реализует доступ к данным, обновление состояния и набор событий связанных с его обновлением, и по сути полностью изолирован от UI. Так что тут я с вами полностью согласен, чем меньше состояния внутри компонентов UI тем лучше.
Собственно, хорошо построенная архитектура в вебе, примерно этому и соответствует: бэкенд(модель данных)/фронтенд(UI для ее отображения). Поэтому если у вас есть проблемы с состоянием(в частности глобальном) в UI, то изначальный вопрос, зачем оно там взялось. (нет состояния - нет "разрывов" логики, что есть то и отобразили)
Да, тут конечно возникает часто необходимость локальности данных, так как ходить на каждый чих в бэкенд может быть дорого, но это вполне решается в рамках той же парадигмы: Глобальная модель данных <-синхронизация-> Локальная модель данных <-> Отображение UI.
Расскажу как решались подобные проблемы в десктопных UI(думаю и в вебе можно смастерить плюс-минус тоже самое).
Вся "архитектура" пилилась на два слоя, условно один слой глобального состояния и модели данных приложения, второй непосредственно UI.
Модель данных имела методы получения из нее и обновления состояния, а так же события обновления различных частей модели на которые мог подписаться любой желающий(стандартный signal-slot в Qt). Слой UI, состоял из относительно крупных компонентов, отображающих какие-то сильно связанные куски интерфейса, и которые внутри управляли уже базовыми примитивами UI(кнопки, лэйблы, и т.д.).
Компоненты UI подписывались на нужный для каждого из них набор событий из слоя данных, и вызывали его методы для модификации состояния. При изменении состояния, дергались связанные с ними события, которые прилетали ко всем подписанным компонентам UI, которые умели себя из этой модели данных обновить. UI старались максимально избавить от собственного состояния и перенести его в модель данных.
Если какие-то данные были внешними, то внутри модели данных после запроса на обновление, можно было куда-то сходить, и вызвать нужные события на обновление когда новые данные пришли и изменили модель.
Подобное решение было простое, как палка и достаточно легко масштабировалось.
PS: классический MVC паттерн как по мне, вообще не сильно полезная штука
Судя из статьи, расстояние все таки манхэттена, и считать его можно непосредственно в количестве клеток.