7 ms·

Okay, now prove that your program written in Lisp will not miss cycles regardless of the data sent to it for at least the length of the mission. The issue is i

Okay, now prove that your program written in Lisp will not miss cycles regardless of the data sent to it for at least the length of the mission. The issue is in being able to prove a program is deterministic. Wildcards like schedulers and garbage collectors sharing resources with code that needs to be real time are notoriously difficult to properly set bounds on behavior. If you aren't doing that then it's not hard real time.

OliverM 4y ago
Are there proofs for other languages/runtimes available? I'd love to see the level of rigour needed to demonstrate that
- WJW 4y ago
  One thing I know of is the CoPilot language/library/thingy from NASA (no relation to Githubs copilot), which can takes in code in a Haskell DSL and outputs code that is guaranteed to run in constant memory and uses an equal number of cycles each loop. See it here: https://copilot-language.github.io/ https://copilot-language.github.io/ Also if you ever find yourself needing to write hard real-time code for your arduino, check out my blog post about the arduino-copilot library at https://wjwh.eu/posts/2020-01-30-arduino-copilot.html https://wjwh.eu/posts/2020-01-30-arduino-copilot.html :)
  - OliverM 4y ago
    Thank you, your blog post was a pleasure to read. CoPilot looks great!
- Ono-Sendai 4y ago
  My programming language Winter has bounded memory and space usage: https://github.com/glaretechnologies/winter https://github.com/glaretechnologies/winter, for at least a subset of the language.
kaba0 4y ago
Why would it be hard? If anything a fat runtime makes it easier - see hard-real time JVMs used in military tech. Hard real time is not too hard in general as it is usually combined with quite low performance-requirements. Boundedness itself is the important property, as opposed to soft-real time which is much more finicky (video games, audio).
- pizlonator 4y ago
  Hard real time GC is hard. The RTGC applications in military tech that I had heard of were on the soft end of hard real time. It was mission critical, not safety critical. Maybe there’s something newer that I hadn’t heard about though. Some of the really bad problems are: - How to make GC operations like allocation have the level of determinism that hard RT programmers want. - How to prove that your GC can keep up with allocation rate while at the same time also only taking a deterministic amount of your time. Not saying it can’t be done. It’s just hard.
  - lisper 4y ago
    > Hard real time GC is hard. Hard real time is hard, full stop. If you have malloc and free you will encounter the exact same real-time challenges as you will with GC. Heck, you don't even need malloc and free. All you need is a WHILE loop to make hard-real-time extremely challenging.
    - pizlonator 4y ago
      GC makes hard real time harder. Way worse than malloc. GC usually works by amortization. 99.99% of allocations are hella fast and then there’s that one that triggers a one second GC that stops the world. There are algorithms to “spread out” the GC cycle over some span of time during which you interleave the GC and your actual code. But then proving that this is schedulable in the worst case is hell. So much hell. I get that real time is hard anyway already. GC just makes it worse.
      - lisper 4y ago
ajross 4y ago
That's... not really a correct description of "hard real time". All system architectures have performance edge cases. The idea of a "hard" real time system is that those be known and fully characterized, and that they can be mapped to equally-fully-characterized application requirements. That way you know all the failure modes ahead of time. Not all aspects of a real time system need latency control like you're imagining. It's entirely possible to imagine, say, an aircraft autopilot or self-driving system (something that needs ~100ms round-trip latencies to approximate a human pilot) being implemented using a garbage collected runtime, as long as you can guarantee those GC pauses are acceptably small (lots of such systems exist). The same would be a very hard ask of a piston engine controller, where the timing needs are closer to 100us. Nonetheless the (again to pick an arbitrary example) logging/telemetry subsystem of that engine controller doesn't need that. So as long as you have an OS that can partition the engine tasks from the low priority stuff in a reliable way, you can still imagine a Lisp/Java/.NET/Go/whatever runtime being used there. Real time is a design philosophy, not a tech stack.
naasking 4y ago
Deterministic programs are great, but that's not a prerequisite for hard realtime. A hard realtime system only needs to be guaranteed to satisfy a schedule.
- jacquesm 4y ago
  I read that as 'deterministic within the context of the hard real time portion' and that is a prerequisite otherwise you may end up overrunning your slot leading to a possible cascade of problems.
  - naasking 4y ago
    It's not a prerequisite in that case either, as long as all possible execution paths fall within the time budget you're fine. Making the execution path deterministic is one way to do that and makes analysis simpler, but it's not the only way.
    - jacquesm 4y ago
      A single loop with an undetermined end condition and you're toast. So that's why having deterministic behavior is a thing to strive for because it allows you to make a guarantee. If all of your code paths are 'straight through' you just tally up the longest sections and if that's below your budget then you know you are going to be ok in all situations.
      - pgorczak 4y ago
        … if you’re running a single task at a time. Usually multiple tasks need exclusive access to shared resources. And they might be triggered by external inputs which are non-deterministic, making the number of possible system states you need to check intractable.
        jacquesm 4y ago
        Yes, hard real time is hard. So don't multi-task, use as simple a scheduler as you can afford and make sure all your time critical paths are limited. I've built quite a few hard real time systems (machine control, mostly) and the penalty for messing that up would be either a toolstrike, loss of a workpiece, loss of a machine or loss of limb or life so I'm aware of the pitfalls and would definitely not want a multi-tasking OS as the core for anything hard real time. For soft real time that works fine, but for hard real time you need absolute control. In an extreme case that can mean a separate CPU running with all interrupts disabled (and NMI tied) so that you will never be surprised. Another CPU can handle concurrent stuff.
hajile 4y ago
The halting problem says that you cannot make this guarantee for ANY sufficiently complex program. Even a mere 9kloc L4 kernel (of intentionally not-so-dense C-code) took many man years to prove. EDIT: Has anyone ever offered such a proof for a program that is just 100kloc? What about 1mloc? Do people actually believe that most non-trivial "realtime" programs are provably realtime?
- School-Cotton 4y ago
  No it doesn’t. It says there are some programs for which you can’t make this guarantee.
- willis936 4y ago
  It's a high standard, but it is the standard for safety-critical systems. Nothing has changed about the problem, so the goal posts should stay where they are despite what new tools we have.
- tralarpa 4y ago
  That might be the reason why the JPL coding standard says: "All loops shall have a statically determinable upper-bound on the maximum number of loop iterations. It shall be possible for a static compliance checking tool to affirm the existence of the bound. An exception is allowed for the use of a single non-terminating loop per task or thread where requests are received and processed. Such a server loop shall be annotated with the C comment: /* @non-terminating@ */."
  - hajile 4y ago
    It took around 5-10 man-years to verify the L4 kernel using a theorem prover and that's just 8700 LOC plus 600 lines of assembly. Without such a theorem solver, it is all just "best practices" then hoping for the best.
    - ducktective 4y ago
      Is there a tech stack or language that allows us to write formally proven and real-time (bounded-time tasks) for embedded systems? What if we can be lenient on these conditions (like soft real time, 500ms bounds)? I'm looking for something like shell scripting (easy and functional) + busybox set of utilities + language built-ins to write concurrent applications. Like an OS with a specialized shell scripting language. Does something like this exist?
samatman 4y ago
Lua gets used on more embedded systems than you might expect, since it's small, fast, and doesn't need floats. You turn the garbage collector off, tune the allowed step size, and trigger collection in steps when it's allowed. Having the Lua VM and GC around is not the hard part of getting hard real time guarantees out of such a system. With Lua, those parts get written in C for the most part. With Common Lisp it's possible to use one language for both parts. At least as I'm told, by those who should know, I've not tried writing any CL which wasn't comfortably high level.
- outworlder 4y ago
  Lua is one of those amazing technologies that one wonders why it isn't just about everywhere. Complex configuration files, embedded scripts, even browser scripting should all have been done in Lua. (Or Lisp, but people have less of a visceral reaction when they see Lua syntax) Theoretically some Common Lisp implementations could have GC disabled. Like you, I have not tried that in practice.
  - Karrot_Kream 4y ago
    In my experience, Lua is everywhere, for some definition of everywhere :P I see it all over the place in so many different settings, embedded, high level scripting, gaming, etc etc
  - pdimitar 4y ago
    I agree and I already used Lua successfully for scripting. My gripe with it is: no easy parallelism and I don't mean OS threads. I suppose it's not a priority for them, sadly.
- melony 4y ago
  Wdym Lua has no floats? Lua defaults to doubles (big floats) not integers.
  - LeifCarrotson 4y ago
    As of Lua 5.3 (from 2015), Lua has both doubles and integers. The famous book "Programming in Lua", still often used and quoted, did apply to 5.2, which had only doubles.
lisper 4y ago
> notoriously difficult to properly set bounds on behavior Actually it's trivial: just put a bound on the amount of available memory and do a worst-case analysis to GC it all. The hard part is not engineering the system to have a bound, it is engineering the system so that the bound is reasonable for practical use.
deleted 4y ago
[deleted]

OliverM 4y ago

Are there proofs for other languages/runtimes available? I'd love to see the level of rigour needed to demonstrate that

WJW 4y ago
One thing I know of is the CoPilot language/library/thingy from NASA (no relation to Githubs copilot), which can takes in code in a Haskell DSL and outputs code that is guaranteed to run in constant memory and uses an equal number of cycles each loop. See it here: https://copilot-language.github.io/ https://copilot-language.github.io/ Also if you ever find yourself needing to write hard real-time code for your arduino, check out my blog post about the arduino-copilot library at https://wjwh.eu/posts/2020-01-30-arduino-copilot.html https://wjwh.eu/posts/2020-01-30-arduino-copilot.html :)
- OliverM 4y ago
  Thank you, your blog post was a pleasure to read. CoPilot looks great!
Ono-Sendai 4y ago
My programming language Winter has bounded memory and space usage: https://github.com/glaretechnologies/winter https://github.com/glaretechnologies/winter, for at least a subset of the language.

kaba0 4y ago

Why would it be hard? If anything a fat runtime makes it easier - see hard-real time JVMs used in military tech. Hard real time is not too hard in general as it is usually combined with quite low performance-requirements. Boundedness itself is the important property, as opposed to soft-real time which is much more finicky (video games, audio).

pizlonator 4y ago
Hard real time GC is hard. The RTGC applications in military tech that I had heard of were on the soft end of hard real time. It was mission critical, not safety critical. Maybe there’s something newer that I hadn’t heard about though. Some of the really bad problems are: - How to make GC operations like allocation have the level of determinism that hard RT programmers want. - How to prove that your GC can keep up with allocation rate while at the same time also only taking a deterministic amount of your time. Not saying it can’t be done. It’s just hard.
- lisper 4y ago
  > Hard real time GC is hard. Hard real time is hard, full stop. If you have malloc and free you will encounter the exact same real-time challenges as you will with GC. Heck, you don't even need malloc and free. All you need is a WHILE loop to make hard-real-time extremely challenging.
  - pizlonator 4y ago
    GC makes hard real time harder. Way worse than malloc. GC usually works by amortization. 99.99% of allocations are hella fast and then there’s that one that triggers a one second GC that stops the world. There are algorithms to “spread out” the GC cycle over some span of time during which you interleave the GC and your actual code. But then proving that this is schedulable in the worst case is hell. So much hell. I get that real time is hard anyway already. GC just makes it worse.
    - lisper 4y ago

ajross 4y ago

That's... not really a correct description of "hard real time". All system architectures have performance edge cases. The idea of a "hard" real time system is that those be known and fully characterized, and that they can be mapped to equally-fully-characterized application requirements. That way you know all the failure modes ahead of time. Not all aspects of a real time system need latency control like you're imagining. It's entirely possible to imagine, say, an aircraft autopilot or self-driving system (something that needs ~100ms round-trip latencies to approximate a human pilot) being implemented using a garbage collected runtime, as long as you can guarantee those GC pauses are acceptably small (lots of such systems exist). The same would be a very hard ask of a piston engine controller, where the timing needs are closer to 100us. Nonetheless the (again to pick an arbitrary example) logging/telemetry subsystem of that engine controller doesn't need that. So as long as you have an OS that can partition the engine tasks from the low priority stuff in a reliable way, you can still imagine a Lisp/Java/.NET/Go/whatever runtime being used there. Real time is a design philosophy, not a tech stack.

naasking 4y ago

Deterministic programs are great, but that's not a prerequisite for hard realtime. A hard realtime system only needs to be guaranteed to satisfy a schedule.

jacquesm 4y ago
I read that as 'deterministic within the context of the hard real time portion' and that is a prerequisite otherwise you may end up overrunning your slot leading to a possible cascade of problems.
- naasking 4y ago
  It's not a prerequisite in that case either, as long as all possible execution paths fall within the time budget you're fine. Making the execution path deterministic is one way to do that and makes analysis simpler, but it's not the only way.
  - jacquesm 4y ago
    A single loop with an undetermined end condition and you're toast. So that's why having deterministic behavior is a thing to strive for because it allows you to make a guarantee. If all of your code paths are 'straight through' you just tally up the longest sections and if that's below your budget then you know you are going to be ok in all situations.
    - pgorczak 4y ago
      … if you’re running a single task at a time. Usually multiple tasks need exclusive access to shared resources. And they might be triggered by external inputs which are non-deterministic, making the number of possible system states you need to check intractable.
      - jacquesm 4y ago
        Yes, hard real time is hard. So don't multi-task, use as simple a scheduler as you can afford and make sure all your time critical paths are limited. I've built quite a few hard real time systems (machine control, mostly) and the penalty for messing that up would be either a toolstrike, loss of a workpiece, loss of a machine or loss of limb or life so I'm aware of the pitfalls and would definitely not want a multi-tasking OS as the core for anything hard real time. For soft real time that works fine, but for hard real time you need absolute control. In an extreme case that can mean a separate CPU running with all interrupts disabled (and NMI tied) so that you will never be surprised. Another CPU can handle concurrent stuff.

hajile 4y ago

The halting problem says that you cannot make this guarantee for ANY sufficiently complex program. Even a mere 9kloc L4 kernel (of intentionally not-so-dense C-code) took many man years to prove. EDIT: Has anyone ever offered such a proof for a program that is just 100kloc? What about 1mloc? Do people actually believe that most non-trivial "realtime" programs are provably realtime?

School-Cotton 4y ago
No it doesn’t. It says there are some programs for which you can’t make this guarantee.
willis936 4y ago
It's a high standard, but it is the standard for safety-critical systems. Nothing has changed about the problem, so the goal posts should stay where they are despite what new tools we have.
tralarpa 4y ago
That might be the reason why the JPL coding standard says: "All loops shall have a statically determinable upper-bound on the maximum number of loop iterations. It shall be possible for a static compliance checking tool to affirm the existence of the bound. An exception is allowed for the use of a single non-terminating loop per task or thread where requests are received and processed. Such a server loop shall be annotated with the C comment: /* @non-terminating@ */."
- hajile 4y ago
  It took around 5-10 man-years to verify the L4 kernel using a theorem prover and that's just 8700 LOC plus 600 lines of assembly. Without such a theorem solver, it is all just "best practices" then hoping for the best.
  - ducktective 4y ago
    Is there a tech stack or language that allows us to write formally proven and real-time (bounded-time tasks) for embedded systems? What if we can be lenient on these conditions (like soft real time, 500ms bounds)? I'm looking for something like shell scripting (easy and functional) + busybox set of utilities + language built-ins to write concurrent applications. Like an OS with a specialized shell scripting language. Does something like this exist?

samatman 4y ago

Lua gets used on more embedded systems than you might expect, since it's small, fast, and doesn't need floats. You turn the garbage collector off, tune the allowed step size, and trigger collection in steps when it's allowed. Having the Lua VM and GC around is not the hard part of getting hard real time guarantees out of such a system. With Lua, those parts get written in C for the most part. With Common Lisp it's possible to use one language for both parts. At least as I'm told, by those who should know, I've not tried writing any CL which wasn't comfortably high level.

outworlder 4y ago
Lua is one of those amazing technologies that one wonders why it isn't just about everywhere. Complex configuration files, embedded scripts, even browser scripting should all have been done in Lua. (Or Lisp, but people have less of a visceral reaction when they see Lua syntax) Theoretically some Common Lisp implementations could have GC disabled. Like you, I have not tried that in practice.
- Karrot_Kream 4y ago
  In my experience, Lua is everywhere, for some definition of everywhere :P I see it all over the place in so many different settings, embedded, high level scripting, gaming, etc etc
- pdimitar 4y ago
  I agree and I already used Lua successfully for scripting. My gripe with it is: no easy parallelism and I don't mean OS threads. I suppose it's not a priority for them, sadly.
melony 4y ago
Wdym Lua has no floats? Lua defaults to doubles (big floats) not integers.
- LeifCarrotson 4y ago
  As of Lua 5.3 (from 2015), Lua has both doubles and integers. The famous book "Programming in Lua", still often used and quoted, did apply to 5.2, which had only doubles.

lisper 4y ago

> notoriously difficult to properly set bounds on behavior Actually it's trivial: just put a bound on the amount of available memory and do a worst-case analysis to GC it all. The hard part is not engineering the system to have a bound, it is engineering the system so that the bound is reasonable for practical use.

deleted 4y ago

[deleted]