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

发布于 2024-07-30 15:01:06 字数 1425 浏览 2 评论 0原文

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

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

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

(关于 Haskell 本身用于此目的的用法:从我在 这篇博文,Haskell 中的垃圾收集和惰性使其在调度方面变得相当不确定,但也许两年后有些事情发生了变化。真实世界的Haskell编程关于SO的问题是我能找到的最接近这个主题的问题)

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

I've been curious to understand if it is possible to apply the power of Haskell to embedded realtime world, and in googling have found the Atom package. I'd assume that in the complex case the code might have all the classical C bugs - crashes, memory corruptions, etc, which would then need to be traced to the original Haskell code that
caused them. So, this is the first part of the question: "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 ?"

I searched for some more examples for Atom, this blog post mentions the resulting C code 22KLOC (and obviously no code:), the included example is a toy. This and this references have a bit more practical code, but this is where this ends. And the reason I put "sizable" in the subject is, I'm most interested if you might share your experiences of working with the generated C code in the range of 300KLOC+.

As I am a Haskell newbie, obviously there may be other ways that I did not find due to my unknown unknowns, so any other pointers for self-education in this area would be greatly appreciated - and this is the second part of the question - "what would be some other practical methods (if) of doing real-time development in Haskell?". If the multicore is also in the picture, that's an extra plus :-)

(About usage of Haskell itself for this purpose: from what I read in this blog post, the garbage collection and laziness in Haskell makes it rather nondeterministic scheduling-wise, but maybe in two years something has changed. Real world Haskell programming question on SO was the closest that I could find to this topic)

Note: "real-time" above is would be closer to "hard realtime" - I'm curious if it is possible to ensure that the pause time when the main task is not executing is under 0.5ms.

如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。

扫码二维码加入Web技术交流群

发布评论

需要 登录 才能够评论, 你可以免费 注册 一个本站的账号。

评论(5

一个人练习一个人 2024-08-06 15:01:06

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

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

因此要小心区分 EDSL(Copilot 或 Atom)与宿主语言(Haskell)。


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

EDSL

系统

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

At Galois we use Haskell for two things:

  • Soft real time (OS device layers, networking), where 1-5 ms response times are plausible. GHC generates fast code, and has plenty of support for tuning the garbage collector and scheduler to get the right timings.
  • for true real time systems EDSLs are used to generate code for other languages that provide stronger timing guarantees. E.g. Cryptol, Atom and Copilot.

So be careful to distinguish the EDSL (Copilot or Atom) from the host language (Haskell).


Some examples of critical systems, and in some cases, real-time systems, either written or generated from Haskell, produced by Galois.

EDSLs

Systems

  • HaLVM -- a lightweight microkernel for embedded and mobile applications
  • TSE -- a cross-domain (security level) network appliance
原来是傀儡 2024-08-06 15:01:06

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

人们对使用 Haskell 或类似 Haskell 的东西编译成非常高效的东西有浓厚的兴趣; 例如,Bluespec 编译为硬件。

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

It will be a long time before there is a Haskell system that fits in small memory and can guarantee sub-millisecond pause times. The community of Haskell implementors just doesn't seem to be interested in this kind of target.

There is healthy interest in using Haskell or something Haskell-like to compile down to something very efficient; for example, Bluespec compiles to hardware.

I don't think it will meet your needs, but if you're interested in functional programming and embedded systems you should learn about Erlang.

爱要勇敢去追 2024-08-06 15:01:06

Andrew,

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

Andrew,

Yes, it can be tricky to debug problems through the generated code back to the original source. One thing Atom provides is a means to probe internal expressions, then leaves if up to the user how to handle these probes. For vehicle testing, we build a transmitter (in Atom) and stream the probes out over a CAN bus. We can then capture this data, formated it, then view it with tools like GTKWave, either in post-processing or realtime. For software simulation, probes are handled differently. Instead of getting probe data from a CAN protocol, hooks are made to the C code to lift the probe values directly. The probe values are then used in the unit testing framework (distributed with Atom) to determine if a test passes or fails and to calculate simulation coverage.

帥小哥 2024-08-06 15:01:06

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

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

我认为 Haskell 是一个非常棒的预处理器,并且使用像 Atom 这样的 DSEL 可能是创建大型硬实时系统的好方法,但我不知道 Atom 是否符合要求。 如果没有,我很确定有可能(并且我鼓励任何这样做的人!)实现一个 DSEL。

对于低级语言来说,拥有像 Haskell 这样非常强大的预处理器,为通过代码生成实现抽象打开了一个巨大的机会之窗,而当实现为 C 代码文本生成器时,代码生成则要笨拙得多。

I don't think Haskell, or other Garbage Collected languages are very well-suited to hard-realtime systems, as GC's tend to amortize their runtimes into short pauses.

Writing in Atom is not exactly programming in Haskell, as Haskell here can be seen as purely a preprocessor for the actual program you are writing.

I think Haskell is an awesome preprocessor, and using DSEL's like Atom is probably a great way to create sizable hard-realtime systems, but I don't know if Atom fits the bill or not. If it doesn't, I'm pretty sure it is possible (and I encourage anyone who does!) to implement a DSEL that does.

Having a very strong pre-processor like Haskell for a low-level language opens up a huge window of opportunity to implement abstractions through code-generation that are much more clumsy when implemented as C code text generators.

君勿笑 2024-08-06 15:01:06

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

I've been fooling around with Atom. It is pretty cool, but I think it is best for small systems. Yes it runs in trucks and buses and implements real-world, critical applications, but that doesn't mean those applications are necessarily large or complex. It really is for hard-real-time apps and goes to great lengths to make every operation take the exact same amount of time. For example, instead of an if/else statement that conditionally executes one of two code branches that might differ in running time, it has a "mux" statement that always executes both branches before conditionally selecting one of the two computed values (so the total execution time is the same whichever value is selected). It doesn't have any significant type system other than built-in types (comparable to C's) that are enforced through GADT values passed through the Atom monad. The author is working on a static verification tool that analyzes the output C code, which is pretty cool (it uses an SMT solver), but I think Atom would benefit from more source-level features and checks. Even in my toy-sized app (LED flashlight controller), I've made a number of newbie errors that someone more experienced with the package might avoid, but that resulted in buggy output code that I'd rather have been caught by the compiler instead of through testing. On the other hand, it's still at version 0.1.something so improvements are undoubtedly coming.

~没有更多了~
我们使用 Cookies 和其他技术来定制您的体验包括您的登录状态等。通过阅读我们的 隐私政策 了解更多相关信息。 单击 接受 或继续使用网站,即表示您同意使用 Cookies 和您的相关数据。
原文