首页 文章

将Haskell用于相当大的实时系统:如何(如果?)?

提问于
浏览
55

我一直很想知道是否有可能将Haskell的强大功能应用到嵌入式实时世界,并且在google搜索中找到了Atom包 . 我假设在复杂的情况下,代码可能具有所有经典的C错误 - 崩溃,内存损坏等,然后需要将其追溯到导致它们的原始Haskell代码 . 所以,这是问题的第一部分:"If you had the experience with Atom, how did you deal with the task of debugging the low-level bugs in compiled C code and fixing them in Haskell original code ?"

我搜索了Atom的更多示例,this blog post提到了生成的C代码22KLOC(显然没有代码:),included example是一个玩具 . Thisthis引用有一些更实用的代码,但这就是结束的地方 . 我把"sizable"放在主题中的原因是,如果您可以分享使用300KLOC范围内生成的C代码的经验,我最感兴趣 .

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

(关于Haskell本身用于此目的的用法:从我在this blog post中读到的内容,Haskell中的垃圾收集和懒惰使其在调度方面具有相当不确定性,但也许在两年内发生了一些变化.Real world Haskell programming关于SO的问题是我最接近的问题可以找到这个主题)

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

5 回答

  • 4

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

    • 软实时(OS设备层,网络),其中1-5毫秒的响应时间似乎是合理的 . GHC生成快速代码,并且有足够的支持来调整GC和调度程序以获得正确的时序 .

    • 用于真实实时系统EDSL用于为其他语言生成代码,提供更强大的时序保证 . 例如 . Cryptol,Atom和Copilot .

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


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

    EDSLs

    Systems

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

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

  • 6

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

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

    我不会对函数编程和嵌入式系统感兴趣,你应该了解Erlang .

  • 4

    安德鲁,

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

  • 6

    我不认为Haskell或其他垃圾收集语言非常适合硬实时系统,因为GC倾向于将其运行时间分摊为短暂暂停 .

    在Atom中编写并不完全是在Haskell中编程,因为Haskell在这里可以看作纯粹是您正在编写的实际程序的预处理器 .

    我认为Haskell是一个很棒的预处理器,使用DSEL _716442知道Atom是否符合要求 . 如果它没有确定它是可能的(我鼓励任何人这样做!)实现DSEL .

    对于低级语言而言,像Haskell这样的非常强大的预处理器为通过代码生成实现抽象提供了巨大的机会,当实现为C代码文本生成器时,这些代码生成更加笨拙 .

  • 47

    我一直在欺骗Atom . 这很酷,但我认为它最适合小型系统 . 是的,它运行在卡车和公共汽车上,并实现真实世界,至关重要应用程序,但这并不意味着这些应用程序必然是大型或复杂的 . 它确实适用于硬实时应用程序,并且竭尽全力使每个操作都花费相同的时间 . 例如,有条件地执行可能在运行时间上不同的两个代码分支之一的if / else语句,它有一个“mux”语句,它总是在有条件地选择两个计算值之一之前执行两个分支(所以总数执行时间与选择的值无关 . 除了通过Atom monad传递的GADT值强制执行的内置类型(与C相当)之外,它没有任何重要的类型系统 . 作者正在研究一种分析输出C代码的静态验证工具,这很酷(它使用SMT求解器),但我认为Atom将受益于更多的源代码级功能和检查 . 即使在我的玩具大小的应用程序(LED手电筒控制器),我已经做了一些新手错误,有人更有经验的包可能会避免,但这导致错误的输出代码,我宁愿被编译器捕获而不是通过测试 . 另一方面,它仍然是0.1版本 . 因此无疑会有改进 .

相关问题