Julia for real time, worried about the garbage collector

General Usage Performance
41

Just want to contribute some things to this wonderful discussion. I am new to Julia, but I come from the field of practice, and research about (hard) real-time systems and stumbled upon this thread randomly.

A hard-real time system is a system that performs every task within a strict given time frame, and I/O is serviced strictly within a small time window, not earlier, not later. Now, what you are proposing here is merely the setup for a real-time system. What you lack is guarantees in the form of formal proofs, that the execution of the algorithms and programs will respect the hard deadlines. You can’t provide these guarantees, especially on a Linux machine that runs on a multiprocessor system with shared memory and caches (pretty much every modern general purpose PC). What I mean is, even if you isolate the execution of an algo to the CPU, it is still not isolated, since it still uses a shared memory, which means any time the other cores access that memory, your CPU may be stalled. Cache coherency and collision is another issue that can stall your CPU execution for a nondeterministic amount of time. These are things that you have NO control over, unless you design your entire stack from the ground up to be hard deadline aware (read deterministic, which is very hard). That you have some empirical evidence to support some “real-time” performance on your setup is absolutely irrelevant.

To guarantee your system is hard real-time compliant, one usually needs to:

  1. Formally verify the correctness of the program
  2. Ensure that each task satisfies the given deadlines – i.e. use static scheduling
  3. Eliminate ANY task communication interference
  4. Analyze and fix a deterministic flow of data

That is something that is handled at the very bottom of the stack (read drivers and custom hardware). Entire hardware architectures are built just for this purpose, as well as RTOS kernels. Julia is way up the layers of the stack, with little to no control over these aspects. And that’s okay, because as far as I see, it addresses a completely different market. Furthermore, its not up to the language and its infrastructure that should address this issue, it is up to the designer. The language and its infrastructure should only provide the tools and capability to design the real-time system. Julia, unfortunately, does not provide these tools.

11 Likes
42

In psychophysical experiments, I usually just want to show the stimulus frames without dropping any, and generally deliver stimuli with low and predictable latency. Nobody dies if you drop frames or happen to have higher latency in a couple of trials, you can always throw those out. But of course it’s ideal to have that happen as little as possible. That’s what I’d call “real-time” in my field, and I’d also be interested if Julia can be useful here. Python and Matlab are widely used in this space

1 Like
43

Thanks for your insight, but I’d like to question what is meant by “correctness.” Something other than “the program will work?” I can believe that one can formally verify the number of machine cycles a code segment will take, but how much more can be proven?

For example, I imagine NASA uses hard real time, and probably tries very hard to verify their control systems. Yet the Mars Climate Orbiter still failed due to metric/Imperial units mismatch. Perhaps each engineer could claim their own subroutine had been “proven” correct, but the overall program was evidently not correct.

I’m certainly a believer in algorithmic correctness. But whatever is proven still relies on humans and their assumptions, e.g. that Intel floating point calculations are always correct.

This isn’t to diminish the importance of hard real-time. It’s just that I have heard talks about “formal verification of control systems,” say for a autonomous driving, that provide a guarantee of correctness and heavily imply safety. The problem is not whether the steering system is stable (which I still question because it assumes certain conditions that are hard to guarantee in real life). It’s whether the vision system has noticed that you’re driving into a semi truck.

44

I’m no expert, but formal verification isn’t some black science, if you’re interested in it, this is a possible place to start research (also try searching Hacker News for “verification”):

Regarding your questions about if it is possible to prove correctness of a computer program, I think it might be helpful to consider the program as any other difficult mathematical proof: it may be possible to prove some proposition, but it still only holds under some known assumptions.

EDIT: If I had to guess, I’d say that it’s not humanly possible to verify the software that Tesla or Waymo use for their self driving systems, and furthermore it stands no chance of ever being correct, because it’s (AFAIK) based on statistical methods.

2 Likes
45

@apo383

TL;DR - Without indulging into a long discussion about this, which clearly does not belong here, what we mean with correctness, is the adherence of the software to a predefined set of liveness and safety properties. It then boils down to how good the models that you use to perform a formal analysis are, and how good approximations to “reality” they are.

Long version:
From a pure software perspective, verifying correctness is accomplished by constructing a mathematical model (automata, FTS, petri nets) of the software, and specifying our informal specifications in a formal language, e.g. propositional logic, temporal logic, etc. Verification and model checking are then performed to verify that a) no unwanted state is reached (safety) and b) something good eventually is done by the system (liveness). It’s related to the so-called reachability problem. Theorem provers are also used to perform this task (e.g. COQ, Isabelle HOL, LEAN).

For real-time systems in particular, real-time behaviors are modeled using e.g data-flow graphs, max-pluss algebra, LPs, real-time calculus, etc. Analysis and scheduling is done by solving optimization problems.

Obviously, however, we deal with the real world, where our software interacts with the physical environment. We have an umbrella name for such systems: Cyber-physical systems. Its a very fresh research, with a lot of activity going on in there. Here we also take real-world phenomena and systems into account to perform analysis and verification.

Indeed, you are right that the crux is how good your models approximate reality, and how much margin of error can be tolerated. This was an active topic of my research for the past 4 years, and I can assure you that it is hard problem to tackle. Simple things such as the sampling rate can be the difference between making your controller stable/unstable, and whether the real-time deadlines are feasible. Yet, clearly a certain amount of jitter and deadline misses can be tolerated, see my answers (bottom) here: https://www.researchgate.net/post/How-do-i-derive-a-relationship-between-the-sampling-time-and-the-dead-time-of-a-real-time-system
https://www.researchgate.net/post/Why-is-proper-selection-of-sampling-important

4 Likes
46

Based on

I thought you were saying that Julia isn’t in a position to provide this kind of support. But then you said

Because you said “unfortunately” I’m now wondering if Julia could provide such tools without compromising its value proposition, but that it simply isn’t providing them at the moment. What tools would it need to provide?

1 Like
47

Julia depends on a “beefy” OS, like Linux. A Julia program therefore can not be hard real time because Julia can’t run on an RTOS or bare metal. I think.

Also, the way Julia does GC is quite incompatible with hard real time, I think.

48

To be more precise, when I talk about “tools” and “infrastructure”, I mainly refer to the low-level access of the tool-chain to the bare-bones and hardware (the HAL). Tools that C/C++ and Rust provide (in fact, I highly recommend Rust over C++ for safety stuff). Julia as a language and semantics (and syntax) is amazing, and it would be really nice to bring this kind of high-level of programming to, say embedded systems. The problem is that, when it comes to implementation, in its current state, you don’t have a complete control of the hardware resources, but someone correct me on this. To facilitate this, you would need to change the core philosophy of the language, i.e. you would have to give up GC, JIT compilation and optimization, and turn it into a low-level, AOT compiled language. This is IMHO a step backwards, and not forwards to what the language tries to achieve.

On the other hand, a direction would be to go the MicroPython way, and design a real-time/embedded systems specific Julia “kernel”. In that regard, there has been research on real-time GC, but it is in very infant stages. Even so, in its current state, I think MicroPython is fine for small embedded projects, but it is definitely not real-time worthy.

With that said, for me personally Julia provides tools for the design and analysis of real-time systems, and specifically the modeling part, i.e. amazing optimization packages, linear algebra, abstractions, and dynamical system modeling. I think this more than justifies its use in hard real-time systems :slight_smile:

EDIT: To complement my last point a bit more, I think Julia is an excellent language for hardware design (something like MyHDL). Its semantics, and more specifically its multiple dispatch and meta-programming, fit perfectly IMHO for the specification of hardware components, and I’m surprised that there has been little to no research in that domain yet.

6 Likes
49

I would keep an eye on StaticCompiler.jl:

Specifically, this PR: Basic rewrite for GPUCompiler by tshort · Pull Request #46 · tshort/StaticCompiler.jl · GitHub
And this write-up: Static compilation in Julia - Google Docs

1 Like