Would it be possible to make a multithreaded runtime like Go goroutines or Rust’s Tokio with Ravenscar?

Projects Ideas
, ,
1

I just found out about ravenscar recently and it seems VERY interesting.

In rust and go, I’ve often run into hard to debug concurrency bugs and deadlocks, so I’m curious if it would be possible to build a multithreaded runtime like Go goroutines, Rust Tokio, or C++ Seastar on top of Ravenscar and have it formally proven

5 Likes
2

Yes-ish.
So, one of the difficulties is the runtime provides a lot of functions (for example Some_Type'Image( Some_Value )) which are used in the rest of the language. In order to make a runtime like you’re thinking of, and if I understand correctly, then what you need to do is first implement protected-types and tasking (SPARK-proven), then use those to provide the rest of the functionality. (It would probably be very worthwhile to take the opportunity to “factorize” common components/subcomponents, perhaps taking advantage of generics; it may be possible [I’m not sure here], also to produce a generic/set-of-generics such that instantiating them produces the runtime, although it must be admitted such extreme decomposition may be both unwieldy [on GNAT, due to the one compilation-unit per file restriction] and “more work than it’s worth”.)

I am working on a language enhancement that may be applicable; though it’s a ways off from proposal.

1 Like
3

What’s your language enhancement?

4

I’m working on a static, compile-time meta-language… well, cut up into 4 domain-specific meta-languages, the goal to be orthogonal, composable, and (taking inspiration from Aspect Oriented Programming) woven together:

  1. Linguistic — For instructing on the how the underlying object interfaces with the language, eg indexing, the “requires initialization” of Limited+Possibly Discriminated, etc.
  2. Noospheric — For collecting into a single place proofs, attaching them to some object or construct. (Ideally, these would be parameterized s.t. you could run SPARK on the meta-object and then simply check the thing you’re attaching to implements those and cut out some [re-]computation.)
  3. Reification — For describing moving from abstract to concrete, though possibly only to “less abstract”. Things like parameter-passing, generic-instantiation, representation clauses, etc.
  4. Structural — Essentially the ‘syntax’ level of things (not really, but “close enough for government work”).

The motivation/anticipated benefits:

  • Cleaning up the annotation sprawl of (eg) containers.
  • Making it possible to use user-defined indexing w/o (a) introducing otherwise unneeded types, (b) using so many aspects, thereby (c) decluttering the source.
  • Provide a way to reify the conceptual type-hierarchy in the LRM. (The scalar, compound, numeric classes; as well as the Universal_* types.)
  • Attaching to the above hierarchy, making attributes easily discoverable/self-documenting for newcomers.
  • Make it possible for the LRM to use forms that are themselves amiable to proof- and model-checking.
  • Make it possible for the LRM to have similar concepts or constructs “factored out”.
  • Facilitate language prototyping.
  • Facilitate language implementation.
2 Likes
5

I think this would be extremely interesting; Goroutines are pretty close with Tasking already, but Tokio would be more of lift. Is there a particular vertical or area you’d want to start with @ValorZard? That might make it more approachable…

1 Like
6

I mean the main thing for me is memory safe green threads and some sort of automatic deadlock detection that happens at either build time or SPARK check.

1 Like
7

Someone posted this library on reddit a month or so back that claims to be tokio like: GitHub - MaheshChandraTeja/Aion: Structured asynchronous runtime for Ada with futures, scheduling, timers, networking, channels, cancellation, and diagnostics. · GitHub

It was obviously unattended AI generated and very rust like. I didn’t like how many if statements with result checks were needed, especially unnecessary ones. I knew 120 lines for an echo server/client was excessive so I did a few passes with an AI to quickly see if it had potential to be cleaned up and… yes it cleaned up the library a ton. I don’t know if I’d use it in it’s current state though. The echo client/server reduced down to like 40 lines of code. check the PR. Definitely not perfect, but a more useable version.

4 Likes