使用Haskell构建大型实时系统：如何实现（如果可以）？

Question

我一直很好奇是否可以将Haskell的优势应用于嵌入式实时世界，并在搜索中发现了Atom包。在复杂情况下，代码可能会出现所有经典的C错误 - 崩溃、内存损坏等，这些错误需要追踪到原始的Haskell代码。因此，这是第一个问题的一部分：“如果您有Atom的使用经验，如何处理编译后的C代码中低级bug的调试任务并修复Haskell原始代码中的错误？”

我搜索了更多关于Atom的例子，这篇博客文章提到了22KLOC的C代码（显然没有代码:)），包含的示例是一个玩具。这个和这个参考资料有更实际的代码，但这就是结束的地方。我之所以在主题中加入“可观”的原因是，我最感兴趣的是您分享使用300KLOC+生成的C代码的经验。

作为一个Haskell新手，显然可能会有其他我由于未知无法知晓的方法，因此在该领域进行自我教育的任何其他指针都将不胜感激 - 这是问题的第二部分 - “使用Haskell进行实时开发的其他实用方法是什么（如果有）？” 如果多核也在考虑范围内，那就更好了 :-)

（关于使用Haskell本身的目的：从这篇博客文章中我所阅读到的，Haskell中的垃圾回收和惰性使得其在调度方面相对不确定，但也许两年后情况会有所改变。 Real world Haskell programming 的SO问题是我能找到的与此主题最接近的问题）

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

- Andrew Y

Answer 1

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

• 软实时（操作系统设备层、网络），其中1-5毫秒的响应时间是可行的。 GHC 生成快速的代码，并且有足够的支持来调整垃圾收集器和调度器以获得正确的时间。
• 对于真正的实时系统，使用EDSL为其他提供更强时间保证的语言生成代码。例如 Cryptol、Atom 和 Copilot。

因此请注意区分 EDSL（Copilot 或 Atom）与主机语言（Haskell）。

---

Galois 所编写或从 Haskell 生成的关键系统的一些示例，在某些情况下是实时系统。

EDSLs

• Copilot：一个硬实时运行时监控器 -- 用于实时航空电子监控的 DSL
• Cryptol 中的等价性和安全检查 -- 用于关键系统的密码组件的 DSL

系统

• HaLVM -- 用于嵌入式和移动应用程序的轻量级微内核
• TSE -- 跨域（安全级别）网络设备

- Don Stewart

---

太棒了，非常感谢！是的，我理解EDSL作为代码生成器和宿主语言本身之间的区别 - 如果我在问题的文本中表述不清楚，那我很抱歉。我将其归类为“在Haskell中”是因为使用像Haskell这样更严格的语言，人们可能（？）避免更多“机械式”的错误，例如边界检查、双重释放等，假设足够的语义在EDSL中得到表达 - 这是我正在尝试理解其真假的猜测之一。 - Andrew Y

Answer 2

在有一个适合小内存并能够保证亚毫秒暂停时间的Haskell系统出现之前，还需要很长时间。Haskell实现者社区似乎对这种目标不感兴趣。

使用Haskell或类似Haskell的东西编译成非常高效的东西是一种健康的兴趣；例如，Bluespec可以编译成硬件。

我认为它不能满足您的需求，但如果您对函数式编程和嵌入式系统感兴趣，应该了解Erlang。

- Norman Ramsey

---

对于bluespec的链接点个赞，将比较它与Lava的区别 - 据我所读，两者具有相似的功能。Erlang: 是的，这是我开始研究的另一件事情，但它似乎更倾向于“柔性”实时性方面。 - Andrew Y

你也可以看看 Ocaml。它是一种函数式语言，如果你想用于算法，甚至支持惰性求值，但并不强制要求所有内容都采用惰性求值。我似乎听说过它被用于实时系统，尽管我自己没有这样做过。总之，它应该比 Erlang 更快更小。 - Chuck

OCaml、Erlang和Haskell都被用于软实时。但是它们都不能保证响应时间，例如。在我们工作中使用的一个系统中，我们很高兴地发现在Haskell中的网络设备上有约1毫秒的响应时间，这就是大致的范围。调整GC设置以最小化噪音也很有用。 - Don Stewart

感谢提到OCaml。从我尝试使用OCaml编写代码的主观感受来看，我的感觉有些复杂。简单的加法示例需要我记住额外的语言特性，这让我感到有些负担；而使用Haskell进行实验则需要我记住可以更简洁地表达事物的语言特性（比如列表推导式），或者是一些非常特殊的功能（例如单子）。这是主观的，我需要更多的经验才能获得更多的理解，但第一印象很难改变。 :) - Andrew Y

提到Ocaml：如果正确性/可验证性是感兴趣的话，那么CertiCoq可能是值得考虑的东西。从最初的发布论文中可以看出：“这项正在进行中的工作应该很快就会产生一个有用的编译器（用于编译您在Coq中证明正确的Gallina程序），高效（在编译时间上），优化（与Ocaml竞争），验证（具有Coq中的证明），兼容（与C和Ocaml兼容），以及优雅。” - Stefan Schmidt

Answer 3

安德鲁，

通过生成的代码回溯到原始源代码来调试问题可能会很棘手。Atom提供了一种探测内部表达式的方法，然后将其留给用户如何处理这些探测。对于车辆测试，我们在Atom中构建了一个发射器，并通过CAN总线传输探针。然后，我们可以捕获这些数据，格式化它，然后使用像GTKWave这样的工具查看它，无论是在后处理还是实时处理中。对于软件模拟，探针的处理方式不同。而是通过钩子将探针值直接提取到C代码中。然后，在单元测试框架（Atom分发）中使用探针值来确定测试是否通过或失败以及计算模拟覆盖范围。

- Tom

Answer 4

我一直在尝试Atom。它非常酷，但我认为它最适合小型系统。是的，它可以在卡车和公交车上运行，并实现真实世界中的关键应用程序，但这并不意味着这些应用程序一定是大型或复杂的。它真正适用于硬实时应用程序，并竭尽全力使每个操作花费完全相同的时间。例如，它没有if/else语句，而是有一个“mux”语句，在条件选择两个计算值之前总是执行两个分支（因此无论选择哪个值，总执行时间都相同）。它没有任何重要的类型系统，除了通过Atom单子传递的内置类型（可与C的类型相比）来强制执行GADT值。作者正在开发一个静态验证工具，分析输出的C代码，这非常酷（它使用SMT求解器），但我认为Atom将受益于更多的源级功能和检查。即使在我的玩具大小的应用程序（LED手电筒控制器）中，我也犯了许多新手错误，而更有经验的人可能会避免这些错误，但这导致了有缺陷的输出代码，我宁愿编译器捕捉到这些错误，而不是通过测试。另一方面，它仍然是版本0.1.x，因此无疑会有改进。

- solrize

---

+1，非常感谢分享。期待下一个版本的到来！ :-) - Andrew Y

Answer 5

我认为Haskell或其他垃圾回收语言并不适合于硬实时系统，因为GC倾向于将其运行时间分摊到短暂的暂停中。

在Atom中编写并不完全等同于使用Haskell编程，因为在这里，Haskell可以被视为您正在编写的实际程序的预处理器。

我认为Haskell是一个非常棒的预处理器，像Atom这样使用DSEL可能是创建大型硬实时系统的好方法，但我不知道Atom是否符合要求。如果不符合，我相信（并鼓励任何人这样做！）可以实现一个DSEL来满足要求。

对于低级语言拥有一个非常强大的预处理器（如Haskell）打开了通过代码生成实现抽象的巨大机会，而当作为C代码文本生成器实现时则更加笨拙。

- Peaker

---

我很好奇您是否有使用该组合的工作经验。就像我所说的，元编程方面看起来很诱人，但我担心元错误及其与更低级别的“普通”错误之间的关系。由于在现场，您只会拥有C代码的符号，乍一看，似乎将它们解开回到更高级别的代码似乎有点棘手。 - Andrew Y

Atom很可能是创建大型硬实时系统的绝佳方式，如果它提供语法、变量、函数和类型系统，那么它不算真正的“预处理器”。在这一点上，Atom实际上成为一个具有自定义代码生成器的语言。至于创建大型系统：Atom被用于美国城市街道上行驶的公交车和垃圾车中。请参见Eaton在CUFP的演讲。如果将Haskell EDSL放到街头使用还没有准备好生产，我不知道还有什么可以了。 - Don Stewart

@dons：好的，至少在我的书中这个得到了+1，感谢你的评论分享实际经验。是时候休息一下并进行更多的练习了。 - Andrew Y