haskell - 将 Haskell 用于大型实时系统 : how (if? )？

Question

我一直想知道是否有可能将 Haskell 的强大功能应用于嵌入式实时世界，并且在谷歌搜索中找到了 Atom包裹。我假设在复杂的情况下，代码可能具有所有经典的 C 错误 - 崩溃、内存损坏等，然后需要追溯到原始的 Haskell 代码
导致他们。所以，这是问题的第一部分:“如果你有使用 Atom 的经验，你是如何处理在编译的 C 代码中调试低级错误并在 Haskell 原始代码中修复它们的任务的？”

我为 Atom 搜索了更多示例，this blog post提到了生成的 C 代码 22KLOC(显然没有代码:)，included example是玩具。 This和 this引用有一些更实用的代码，但这就是结束的地方。我在这个主题中加上“相当大”的原因是，如果您可以分享您在 300KLOC+ 范围内使用生成的 C 代码的经验，我最感兴趣。

由于我是 Haskell 新手，显然由于我的未知数，我可能没有找到其他方法，因此将不胜感激任何其他在该领域进行自我教育的指针 - 这是问题的第二部分 - “在 Haskell 中进行实时开发的其他一些实用方法(如果)是什么？”。如果多核也在图片中，那是一个额外的好处:-)

(关于为此目的使用 Haskell 本身:从我在 this blog post 中读到的内容来看，Haskell 中的垃圾收集和懒惰使得它在调度方面相当不确定，但也许在两年内发生了一些变化。Real world Haskell programming 关于 SO 的问题是我能找到的最接近这个主题的)

注:上面的“实时”更接近“硬实时”-我很好奇是否可以确保主任务未执行时的暂停时间低于 0.5 毫秒。

Answer 1

在 Galois，我们使用 Haskell 做两件事:

软实时(操作系统设备层、网络)，其中 1-5 毫秒的响应时间是合理的。 GHC 生成快速代码，并为调整垃圾收集器和调度程序以获得正确的时间提供大量支持。

对于真正的实时系统，EDSL 用于为提供更强时序保证的其他语言生成代码。例如。 Cryptol、Atom 和 Copilot。

所以要小心区分 EDSL(Copilot 或 Atom)和宿主语言(Haskell)。

一些关键系统的例子，在某些情况下，实时系统，无论是由 Haskell 编写还是生成，由 Galois 制作。

EDSL

Copilot: A Hard Real-Time Runtime Monitor -- 用于实时航空电子设备监控的 DSL

Equivalence and Safety Checking in Cryptol -- 关键系统加密组件的 DSL

系统

HaLVM -- 用于嵌入式和移动应用程序的轻量级微内核

TSE -- 跨域(安全级别)网络设备