将Haskell用于大型实时系统:如何(如果？)？

Question

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

我搜索了Atom的更多示例,这篇博文提到了生成的C代码22KLOC(显然没有代码:),包含的示例是一个玩具.这个和这个引用有一些更实用的代码,但这是结束的地方.我在这个主题中加入"相当大"的原因是,如果您可以分享使用300KLOC +范围内生成的C代码的经验,我最感兴趣.

因为我是一名Haskell新手,显然可能有其他方法由于我未知的未知因素而未找到,所以在这方面任何其他自我教育的指针都会非常感激 - 这是问题的第二部分 - "在Haskell中进行实时开发会有什么其他实用方法(如果)？" 如果多核也在图片中,这是一个额外的加号:-)

(关于Haskell本身用于此目的的用法:从我在这篇博文中读到的内容,Haskell中的垃圾收集和懒惰使其在调度方面具有相当不确定性,但可能在两年内发生了一些变化.现实世界的Haskell编程问题在SO上是我能找到的最接近这个话题的人)

注意:上面的"实时"将更接近"硬实时" - 我很好奇是否可以确保主要任务未执行的暂停时间小于0.5ms.

Answer 1

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

• 软实时(OS设备层,网络),1-5毫秒响应时间似乎是合理的.GHC生成快速代码,并且有足够的支持来调整垃圾收集器和调度程序以获得正确的时序.
• 对于真正的实时系统,EDSL用于为其他语言生成代码,以提供更强大的时序保证.例如Cryptol,Atom和Copilot.

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

关键系统的一些例子,在某些情况下是由Galois编写的Haskell编写或生成的实时系统.

EDSLs

• Copilot:硬实时运行时监控器 - 用于实时航空电子设备监控的DSL
• Cryptol的等效性和安全性检查 - 一种用于关键系统加密组件的DSL

系统

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

Answer 2

在Haskell系统适合小内存并且可以保证亚毫秒暂停时间之前还需要很长时间.Haskell实现者社区似乎对这种目标似乎没有兴趣.

使用Haskell或Haskell之类的东西可以很好地编译成非常有效的东西; 例如,Bluespec编译为硬件.

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

Answer 3

安德鲁,

是的,通过生成的代码将问题调回原始源可能会很棘手.Atom提供的一个方法是探测内部表达式,然后留给用户如何处理这些探测器.对于车辆测试,我们构建一个发射器(在Atom中)并通过CAN总线将探测器流出.然后我们可以捕获这些数据,将其格式化,然后使用GTKWave等工具进行查看,无论是在后期处理还是实时处理.对于软件模拟,探针的处理方式不同.不是从CAN协议获取探测数据,而是对C代码进行挂钩以直接提升探测值.然后在单元测试框架(与Atom一起分发)中使用探测值来确定测试是通过还是失败并计算模拟覆盖范围.