Использование Haskell для значительных систем реального времени: как (если?)?

Мне было любопытно понять, можно ли применить силу Haskell к встроенному миру в реальном времени, а в googling нашли Atom. Я предполагаю, что в сложном случае код может иметь все классические ошибки C - сбои, повреждение памяти и т.д., Которые затем должны быть отслежены до исходного кода Haskell, который вызвали их. Итак, это первая часть вопроса: "Если у вас был опыт работы с Atom, как вы справились с задачей отладки низкоуровневых ошибок в скомпилированном C-коде и исправления их в исходном коде Haskell?"

Я искал еще несколько примеров для Atom, этот пост в блоге упоминает полученный C-код 22KLOC (и, очевидно, никакого кода:), включенный пример - игрушка. Этот и этот содержит немного более практичный код, но это и заканчивается. И причина, по которой я ставлю "значительную" тему, мне больше всего интересно, если вы можете поделиться своим опытом работы с сгенерированным кодом C в диапазоне 300KLOC +.

Поскольку я новичок Haskell, очевидно, что могут быть другие способы, которые я не нашел из-за моих неизвестных неизвестных, так что любые другие указатели на самообразование в этой области были бы весьма признательны - и это вторая часть вопрос - "какие будут другие практические методы (если) для развития в реальном времени в Haskell?". Если многоядерность также находится на картинке, это дополнительный плюс:-)

(Об использовании самого Haskell для этой цели: из того, что я читал в этот пост в блоге, сбор мусора и лень в Haskell делает это скорее недетерминированное планирование, но, может быть, через два года что-то изменилось. Реальный мир программирования Haskell вопрос о SO был самым близким, что я мог найти в этой теме)

Примечание: "в реальном времени" выше будет ближе к "жесткому реальному времени". Мне любопытно, можно ли гарантировать, что время паузы, когда основная задача не выполняется, менее 0,5 мс.

Ответ 1

В Galois мы используем Haskell для двух вещей:

Мягкое реальное время (уровни устройств ОС, сети), где время отклика 1-5 мс правдоподобно. GHC генерирует быстрый код и имеет большую поддержку для настройки GC и планировщика, чтобы получить правильные тайминги.
для реальных систем реального времени EDSL используются для генерации кода для других языков, которые обеспечивают более надежные гарантии времени. Например. Cryptol, Atom и Copilot.

Поэтому будьте осторожны, чтобы отличить EDSL (Copilot или Atom) от языка хоста (Haskell).

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

EDSLs

Copilot: жесткий монитор времени выполнения в реальном времени - DSL для мониторинга авионики в реальном времени
Эквивалентность и проверка безопасности в Cryptol - DSL для криптографических компонентов критических систем.

Системы

HaLVM - легкое микроядро для встроенных и мобильных приложений.
TSE - сетевое устройство междоменного уровня (уровень безопасности)

Ответ 2

Эндрю

Да, может быть сложно отладить проблемы сгенерированным кодом до исходного источника. Одна вещь, которую предоставляет Atom, - это средство для исследования внутренних выражений, а затем уходит, если до пользователя, как обрабатывать эти зонды. Для тестирования транспортных средств мы создаем передатчик (в Atom) и передаем зонды через шину CAN. Затем мы можем записать эти данные, сформировать его, а затем просмотреть его с помощью таких инструментов, как GTKWave, либо в пост-обработке, либо в режиме реального времени. Для моделирования программного обеспечения зонды обрабатываются по-разному. Вместо того, чтобы получать данные зонда из протокола CAN, крючки делаются с кодом C, чтобы напрямую поднять значения зонда. Значения зонда затем используются в единичной тестовой структуре (распределенной с Atom), чтобы определить, проходит ли тест или не выполняется, и для расчета охвата моделирования.

Ответ 3

Прошло много времени, прежде чем появится система Haskell, которая вписывается в небольшую память и может гарантировать периоды паузы в миллисекундах. Сообщество разработчиков Haskell просто не интересуется этой целью.

Существует здоровый интерес к использованию Haskell или что-то вроде Haskell, чтобы скомпилировать что-то очень эффективное; например, Bluespec компилируется на оборудование.

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

Ответ 4

Я не думаю, что Haskell или другие сборники с мусором очень хорошо подходят для систем с жестким режимом реального времени, поскольку GC, как правило, амортизирует их время выполнения в короткие паузы.

Запись в Atom не является точно программированием в Haskell, так как Haskell здесь можно рассматривать как чисто препроцессор для конкретной программы, которую вы пишете.

Я думаю, что Haskell - потрясающий препроцессор, и использование DSEL, такого как Atom, вероятно, отличный способ создать значительные системы реального времени, но я не знаю, подходит ли Atom к законопроекту или нет. Если это не так, я уверен, что это возможно (и я призываю всех, кто это делает!) Реализовать DSEL, который делает.

Наличие очень сильного препроцессора, такого как Haskell для языка низкого уровня, открывает огромное окно возможностей для реализации абстракций с помощью генерации кода, которые гораздо более неуклюжи, когда они реализуются как генераторы текста кода C.

Ответ 5

Я обманывал Atom. Это довольно круто, но я думаю, что это лучше всего для небольших систем. Да, он работает в грузовиках и автобусах и реализует реальные критически важные приложения, но это не означает, что эти приложения обязательно являются большими или сложными. Это действительно для приложений с жестким режимом реального времени и подходит для того, чтобы каждая операция выполняла то же самое время. Например, вместо инструкции if/else, которая условно выполняет одну из двух ветвей кода, которая может отличаться в времени выполнения, она имеет оператор "mux", который всегда выполняет обе ветки до условного выбора одного из двух вычисленных значений (так что общая время выполнения такое же, какое выбрано значение). У него нет какой-либо значительной системы типов, кроме встроенных типов (сопоставимых с C), которые применяются через значения GADT, переданные через монаду Atom. Автор работает над инструментом статической проверки, который анализирует выходной код C, который довольно крут (он использует решатель SMT), но я думаю, что Atom выиграет от большего количества функций и проверок на уровне исходного кода. Даже в моем приложении размером с игрушку (контроллер светодиодного фонарика) я сделал несколько ошибок новичка, которых мог избежать кто-то более опытный с пакетом, но это привело к ошибковому выходному коду, который я бы предпочел поймать компилятором а не через тестирование. С другой стороны, он все еще находится в версии 0.1.что-то, что, несомненно, приближаются улучшения.