Hacker News Digest

Ironclad — это формально верифицируемый, реального времени, UNIX-подобный ядро операционной системы общего назначения и встраиваемых систем, написанное на SPARK и Ada. Проект полностью свободный и распространяется под лицензией GPLv3. Ключевые особенности включают POSIX-совместимый интерфейс, одновременное вытесняющее многозадачность, обязательный контроль доступа (MAC) и поддержку жёсткого реального времени.

Главное преимущество Ironclad — формальная верификация с помощью SPARK для критических компонентов, таких как криптография и MAC. Система полностью портативна и зависит только от GNU toolchain, что упрощает кросс-компиляцию. Проект поддерживает дистрибутивы для всех доступных архитектур, наиболее заметный из которых — Gloire. Ironclad всегда будет бесплатным для использования, изучения и модификации, а финансируется за счёт пожертвований и грантов от NLnet и Европейской комиссии.

• Участники сомневаются в степени формальной верификации Ironclad, сравнивая его с более строгими аналогами вроде seL4 и Tock, и указывают на отсутствие доказательства ключевых свойств ядра.
• Проект написан на SPARK и Ada, поддерживает x86_64 и RISC-V, но не ARM64; его лицензия включает бесплатную версию с возможностью коммерческого использования.
• Основные альтернативы: seL4 (быстрый и строго верифицируемый), Genode (POSIX-совместимый слой), Asterinas и Redox (Linux-совместимые ядра), а также ReactOS и SerenityOS.
• Критика включает медленную производительность по сравнению с seL4, отсутствие capability-based безопасности и потенциальные проблемы на уровне прошивки.
• Уточнено, что формальная верификация — это не тестирование, а математическое доказательство соответствия спецификации, а "бесплатность" ПО может относиться только к лицензии.

Автор экспериментирует с созданием простого брокера сообщений, используя только два UNIX сигнала вместо сложных систем вроде Kafka. Он объясняет, что сигналы обычно применяются для управления процессами, но предлагает использовать их для обмена сообщениями. Автор рассматривает различные формы IPC в UNIX, включая каналы, сокеты и файлы, а затем фокусируется на сигналах SIGUSR1 и SIGUSR2, которые являются пользовательскими и могут использоваться для собственных целей.

Основная идея заключается в представлении сообщений как последовательности битов, где каждый бит кодируется соответствующим сигналом (0 - один сигнал, 1 - другой). Это позволяет передавать данные между процессами, используя минимальные системные ресурсы. Автор демонстрирует, как можно "взломать" стандартное поведение сигналов для создания эффективной системы обмена сообщениями, опираясь на двоичное представление данных и возможность перехвата сигналов в коде на Ruby.

• Обсуждение показало, что статья вызвала бурную реакцию: от восторга до критики за clickbait-заголовок и «техническую» неточность.
• Комментаторы подчеркнули, что UNIX-сигналы не предназначены для передачи данных, не гарантируют очередность и могут терять сигналы при конкурентном доступе.
• Было отмечено, что вместо сигналов можно использовать уже готовые механизмы, такие как POSIX message queues.
• Некоторые отметили, что статья может быть интересна как учебный материал, но не как руководство к действию.
• В итоге, обсуждение показало, что читатели ожидают более честных и точных заголовков и отсутствия сенсационализма, даже в контексте развлекательных экспериментов.

Остановка потоков Linux требует аккуратного подхода, особенно при работе с низкоуровневыми потоками, созданными через pthread_create или std::thread. В отличие от запуска, корректное завершение потоков позволяет выполнить очистку ресурсов — освобождение памяти, блокировок, сброс логов. Идеального универсального решения не существует, но есть несколько подходов.

Простой метод — организация квази-активного ожидания в каждом потоке с проверкой флага остановки. Когда нужно завершить поток, флаг устанавливается в true, после чего вызывается pthread_join. Цикл не должен быть полностью неблокирующим, но должен завершаться за разумное время. Для потоков, блокирующихся на системных вызовах, используются сигналы для прерывания выполнения. Важно, что даже с этим подходом нужно учитывать обработку сигналов для корректной работы с буферизированным выводом.

• Проблема заключается в том, что POSIX не предоставляет безопасного механизма для остановки потока, и это приводит к тому, что разработчики вынуждены полагаться на pthread_cancel, который небезопасен и может привести к утечкам ресурсов или повреждению состояния.
• Попытки использовать SIGUSR1 и signalfd для обработки сигналов в пространстве пользователя не решают проблему, потому что большинство библиотек не ожидают, что их вызовы будут прерваны, и это может привести к повреждению состояния.
• Вместо этого, вместо попыток остановить поток, который может быть в любой точке, лучше структурировать код так, чтобы он мог реагировать на сигнал остановки, или использовать модель, где потоки не блокируются на системных вызовах, а вместо этого используют асинхронные вызовы и ожидают на poll/select/epoll/io_uring.
• Некоторые комментаторы отмечают, что в Linux существует io_uring, который позволяет прервать системный вызов, и что это может быть использовано для реализации остановки потока, но это не решает проблему, что не все вызовы могут быть прерваны таким образом.
• В конечном счёте, вместо попыток убить поток, который может быть в любой точке, лучше писать код так, чтобы он был отзывчив к сигналу остановки, и использовать модели, где потоки не блокируются на системных вызовах, а вместо этого используют асинхронные вызовы и ожидают на poll/select/epoll/io_uring.

Toybox — это минималистичная реализация стандартных утилит командной строки для Linux и Android, написанная на чистом C. Она создана как компактная и самодостаточная альтернатива BusyBox, с акцентом на простоту, корректность и соответствие стандартам POSIX. Проект включает основные инструменты вроде ls, cp, mv и многие другие, сохраняя при этом малый размер и избегая внешних зависимостей.

Разработка ведётся с упором на читаемость кода и портируемость, что делает Toybox полезной для встраиваемых систем, восстановительных сред и случаев, где важны предсказуемость и минимализм. Она часто используется в проектах типа Android Toybox, демонстрируя свою практическую ценность для современных ОС.

• Toybox — это альтернатива BusyBox с более разрешительной лицензией (0BSD/MIT-0), созданная для решения лицензионных проблем и использования в Android.
• Оба проекта предоставляют набор стандартных UNIX-утилит (ls, cp, mv и др.) в виде одного исполняемого файла, что экономит место на диске.
• Изначальная идея Toybox вызывала споры из-за отказа от copyleft, но была принята как компромисс для включения в ОС.
• Название Toybox, вероятно, отсылает к коллекции игрушек (аналогично BusyBox) и может быть связано с песней Soundgarden.
• Проект ценится за чистый код и пермиссивную лицензию, но пока не достиг полной функциональной parity с BusyBox.

Сокращённый перевод на русский (в 2 раза короче):

PDF-документ
Формат: PDF-1.6
Содержит:

• 1 страницу (612×792 pt)
• 4 объекта ресурсов (шрифты, изображения, цветовые пространства)
• 3 встроенных изображения (390×390 px, 8-бит, RGB)
• Потоки данных: сжатые FlateDecode, длина ~44 Кб и ~18 Кб
• Шрифты: TrueType (TT1–TT20)
• Изображения: Im1–Im4, интерполяция включена
• Структура: страница → ресурсы → содержимое → потоки

Итог:
Технический PDF с графикой и текстом, оптимизированный под визуализацию.

• Apple сертифицирует macOS как UNIX, чтобы избежать судебных исков за неправомерное использование торговой марки «Unix».
• Сертификация требует включения специального «Unix-режима» (case-sensitive FS, выключенный SIP и т.д.); тот macOS, что идёт на новых Маках, сертифицированным не является.
• Процесс дорог и непопулярен: большинство Linux-дистрибутивов и *BSD давно отказались от него, считая POSIX-совместимости достаточно.
• Участники обсуждения находят десятилетние баги (poll, fsync, pthread-часы), которые так и не исправлены, несмотря на формальное соответствие стандарту.
• Итог: сертификат нужен в основном маркетологам и юристам; разработчики ценят macOS за удобство и набор Unix-утилит, а не за штамп « Certified UNIX™».

curl 8.16.0 внедрил pthread_cancel, чтобы прерывать зависший getaddrinfo, но уже в следующем релизе функцию убирают: отмена потока приводит к утечке памяти.

glibc сначала резолвит имя, выделяя память, затем читает /etc/gai.conf, где встречается fopen — точка отмены. Если поток прервать на этом шаге, выделенные адреса не освобождаются, и утечка повторяется при каждом новом вызове.

Поскольку других «опасных» точек может быть ещё больше, а библиотека не гарантирует чистоту ресурсов, pthread_cancel признан неприемлемым. Возвращаемся к старому выбору: либо ждать pthread_join, либо пускать потоки «в свободное плавание» и накапливать их.

Кто не хочет тормозов — подключает c-ares, но тот не покрывает всех возможностей glibc.

• Проблема: стандартный POSIX-вызов getaddrinfo блокирующий, не имеет таймаута и плохо сочетается с pthread_cancel, что приводит к утечкам/дедлокам.
• Исторически DNS-запросы запускали в отдельном потоке/процессе, но 30 лет спустя ситуация не улучшилась.
• Альтернативы есть: getaddrinfo_a, c-ares, systemd-resolved, io_uring, но они либо glibc-специфичны, либо нетривиальны в кросс-платформенной разработке.
• Разработчики предлагают:
  – отказаться от pthread_cancel и использовать пул воркер-потоков с флагом «самоубийства»;
  – вынести DNS из libc в системный сервис;
  – дождаться нового POSIX-стандарта асинхронного резолвера.