The OpenNET Project / Index page

[ новости /+++ | форум | теги | ]



Индекс форумов
Составление сообщения

Исходное сообщение
"Выпуск глобальной децентрализованной файловой системы IPFS 0..."
Отправлено Sw00p aka Jerom, 26-Фев-21 19:37 
> Это значит, который позволяет промышленным образом получать гарантированный результат.

Я так и не увидел определение проблемы.


> Если ты делаешь malloc/free то уже могут возникнуть проблемы. Ты мог выделить
> память, и не освободить её после того, как она пекратила быть
> нужной. Даже если ты не делаешь malloc/free проблемы могут возникнуть: скажем
> ты можешь вернуть из функции указатель на локальную память, и получить
> use-after-free. Как ты доказываешь, что этого нет?

Ты, ты, ты - так чья это проблема если всюду ты? Повторяю, когда мы говорим "что ты забыл освободить" или "ты освободил уже освобожденное" - это проблемы твои, не мои (не CS). И как мне доказать, что "ты" не допустил этих проблем? Да лекго, я потребую от тебя оценку "пространственную" твоего алгоритма, запущу на исполнение и замерю занимаемое "пространство". Нынешнее поколение забыли, что такое отладка, что такое снять дамп памяти и т.д. потому-что именно отладка прокажет весь процесс исполнения, где на каком шагу алгоритма что должно храниться в той или иной ячейки памяти. Поэтому корректные алгоритмы на асм, без процесса пошаговой отладки, пишутся крайне редко. И все время "программиста" уходит на отладку, а не написание строчек кода.

> Это бажный алгоритм. В "прошлые" разы -- это в смысле когда мы
> обсуждали rust'овые гарантии safety? Безопасность -- это не то же самое,
> что и безбажность. Если я в расте разворачиваю Result'ы при помощи
> unwrap, то при любой ошибке я получаю панику и принудительное завершение
> программы. Если я собрал растовый код с проверкой на выход за
> границы, то у меня гарантированно не будет buffer-overflow, но программа может
> выпадать в панику, когда индекс за границы выходит. Это тоже всё
> баги программы. Но "безопасные" баги.

"Бажный" алгоритм придумывает "бажный" мозг "программиста". Это не проблема CS. Вам говорят взял (alloc) потом верни (free), чья это проблема если вы не следуете этому правилу? Любое нарушение правил по сути баг, а кто их нарушает? даже в случае с UB, вам говорят не делайте так, а то будет UB, а вы что? Одни и теже грабли.

> Там я приводил примеры, когда mem-leak'и могут оказываться опасными. Для большинства приложений
> они имеют пониженную опасность, потому как первый приоритет у багов, позволяющих
> злоумышленнику запустить произвольный код на системе и захватить полный контроль над
> системой. Но хапануть злоумышленного кода -- это не для всех программ
> актуально, а для некоторых ООМ означает полный провал.

Размышления о последствиях "багов" не тема разговора. Так как тут все специфично, системно зависимо.

> Ты строишь в голове конструктивное доказательство.
> Даже если ты делаешь это в уме и очень неформально: суть
> в том, что ты делаешь это таким образом, что ежели я
> скажу тебе "докажи свою оценку", ты легко сможешь выкатить строгое доказательство
> её.

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

> Но это википедия, не надо относиться к ней излишне серьёзно.

Вы не согласны с определением ассимтотической сложности алгоритмов? Дайте свое определение.


> Бывает. Но попробуй какой-нибудь нетривиальный синтаксис парсить, и доказать, что время
> работы парсера не будет убегать в бесконечность.

зачем далеко ходить, возьмите регексы, как вы думаете там есть понятия recursion limit? И зачем такие ограничения?

> Это может работать если ты предположишь, что у тебя нет проблем с
> mm, типа mem-leak'ов. То есть если ты исходно заложишь предположение о
> том, что у тебя программа безбажна, то ты докажешь, что она
> безбажна. Нет ничего удивительного в этом, а? А теперь попробуй доказать,
> что ни при каком входе программа не течёт памятью.

Повторяю, доказывается "пространственной" оценкой, а как получить эту оценку? - пошагово исполните алгоритм и смотрите какое "пространство" (память) он будет занимать. То есть алгоритм необходимо отладить в прямом смысле слова, сколько ячеек памяти занято и построить график зависимости от объема входных данных, это и будет оценкой. Повторите сей эксперимент несколько раз на разных входных параметрах. Это называется анализ алгоритма.


> У тебя есть детерминированный алгоритм поиска багов в программах? И какова асимптотическая
> сложность этого алгоритма от SLOC? Я утверждаю, что у тебя нет
> детерминированного алгоритма не только для поиска всех багов, но даже для
> поиска багов относящихся к mm, таких как use-after-free, double-free и memory-leak.

Отладка и еще раз отладка, а без отладки - тупо сравнить вот выделил тебе N байт, а ты вернул N-1, о чем это говорит? Алгоритм разве должен выяснить где ты это допустил? А зачем когда есть отладка и этим делом должен заниматься "программист". Скажите, что у меня еще нет и алгоритма который сам создает алгоритмы, ой как весело будет.

> То что у тебя есть, либо не ловит всего, либо предмет
> той самой проблемы останова: ты не сможешь доказать, что твой алгоритм
> остановится когда-нибудь.

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

> Ты не ответил на вопрос: на чём основана твоя вера? Ты просто
> веришь? Или как-то доказываешь?

Вера удел дураков, как и удача. Выше я описал, про оценку и доказательство (применяемого к методу оценки).

> Я уверен, что ты доказываешь. Пускай неформально,
> пускай ты не пишешь на листочке сложных доказательств непонятными математическими значками.
> Но доказываешь. Ты проделываешь в своей голове рассуждения вида: вот тут
> мы выделяем память Q, и сохраняем указатель на неё в структуре
> A... Больше отсюда указатель мы никуда не копируем, и структура A
> освобождает Q либо в деструкторе, либо раньше. Значит, если мы докажем,
> что память структуры A освобождается законным для языка путём (то есть
> так, чтобы деструктор отработал), то мы можем забыть про Q, с
> ней тоже всё будет ок.

Нет я так не рассуждаю, выделение, указатель, структура, деструктор (что за страшное слово) - все это часные случаи со своими вытекающими следствиями. Ассимптотику на то и придумали, чтобы охватить все эти случаи и не касаться их конкретно.

> Ты гоняешь в своей голове рассуждения по типу этого. Ну, точнее, тут
> одно из двух: либо гоняешь, либо быдлокодер. Я ставлю на первое.

Нет не гоняю и гонять не хочу, потому что я не ограничиваю себя в таких рассуждениях конкретными языками, структурами, умными указателями и т.д. Грубо говоря, рассуждать нужно по Тьюрингу.

> Но есть ли у тебя способ взяв код, выстроить достаточное количество
> таких рассуждений, чтобы утверждать что в программе нет проблем с mm
> (то есть нет use-after-free, double-free и memory-leak, я не включаю сюда
> buffer-overflow, потому что про него как раз можно выстроить конечной протяжённости
> рассуждения, которые докажут наличие или отсутствие).

В терминах машины Тьюринга таких понятий нет.

 

Ваше сообщение
Имя*:
EMail:
Для отправки ответов на email укажите знак ! перед адресом, например, !user@host.ru (!! - не показывать email).
Более тонкая настройка отправки ответов производится в профиле зарегистрированного участника форума.
Заголовок*:
Сообщение*:
  Введите код, изображенный на картинке: КОД
 
При общении не допускается: неуважительное отношение к собеседнику, хамство, унизительное обращение, ненормативная лексика, переход на личности, агрессивное поведение, обесценивание собеседника, провоцирование флейма голословными и заведомо ложными заявлениями. Не отвечайте на сообщения, явно нарушающие правила - удаляются не только сами нарушения, но и все ответы на них. Лог модерирования.



Партнёры:
PostgresPro
Inferno Solutions
Hosting by Hoster.ru
Хостинг:

Закладки на сайте
Проследить за страницей
Created 1996-2024 by Maxim Chirkov
Добавить, Поддержать, Вебмастеру