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
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.
What’s your language enhancement?
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:
Limited+Possibly Discriminated, etc.The motivation/anticipated benefits:
Universal_* types.)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…
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.
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.
@markhermeling i wonder if you could try forking this and getting this to SPARK silver.
the api seems noisy but i think it would be cool
actually, taking a deeper look at the code, i don’t actually seem to see any actual async runtime thing going on? seems like its just blocking on async calls as far as i can tell, on both your fork and the OG code
Edit:
I think the main thing my brain is stuck on when desigining an async runtime (especially on top of Jorvik) is:
how would async await work?
in rust or c++, await is part of the syntax, but in Ada, it would have to be a function.
And how would you yield in a middle of a function? can you call nested await inside of another async function?
also if its work stealing, how would you move a current future/promise somewhere else?
I cant answer these questions, but I should have some tokens to spend over the weekend.
Okay, there is a lot of info here… Lets see if I can give you some useful info…
Semi-correct. AFAIK, the common RTS (Ada RunTime System) design used by the GNAT compiler is built on top of pthreads and will most likely be blocking.
Correct, Ada does not have the notion of async… The way tasks, threads or green-threads work is defined by the underlying RTS. AFAIK, Ada has no way of distinguishing between actual thread/tasks and async code… almost.
@joakim-strandberg presented… last year? an Ada compiler for MS-DOS that had two possible RTSes. It is important to note that MS-DOS only ran in single core systems, so there was only one possible execution thread. One was a time-slicing/scheduling RTS which would give some execution time to each task and another one was a cooperative RTS. IIRC (If I Recall Correctly), the cooperative RTS would allow for async/yield if a task declared a delay 0.0 (null delay), which the RTS would understand as a “ah, the task can be interrupted here now, so I can use whatever state it may have generated and let other tasks do some work, which can be based on the info generated by the task being interrupted”. This more or less makes it behave like an async/await kind of thing…
I do not know if anything that I wrote will be helpful to you… Best regards,
Fer
yeah i think im more so thinking if i want to create some sort of green thread system in ada on top of tasks/threads.
honestly i might just be overthinking this and we could just make promises protected objects
edit: i should mention the main thing im trying to think of is when we call an async function, we don’t block on that function, and we can switch over to another async future running at the same time
this seems like an interesting implementation of this idea
I do not quite understand why do you want this, in my view, inferior interface? The point is that stack-less co-routines are useless unless you already have a complicated state machine in the first place. With the stack added it becomes just Ada tasking which is a many times over a better model.
What is needed is an implementation of lightweight tasks on the basis of co-routines rather than OS threads. Ada allows this. In fact, early GNAT RTS that implemented tasks without OS threads.
The actual challenge is automated conversion of blocking calls to non-blocking call + yielding. Upon an I/O event the co-routine should be marked for re-scheduling. I think it is possible to do by supplying a special versions of I/O packages. Blocking calls can be a “bounded error” inside tasks with the “Coroutine” aspect.
I’d be down for something more idiomatic with Ada, do you have any examples in code of supplying special I/O packages?
I would also be interested with somehow replacing Ada’s task implementation with a custom one using green threads if that’s doable at all using SPARK
Okay doiokay doing a bit more research into this, replacing the default ADA task runtime with a custom one that’s built with green threads instead might be the way to go.
There was something similar to this called the Open Ravenscar Kernel but I can’t find any source repository’s for it.
There does seem to be a way to write a custom ada runtime but I’m not really sure how:
No, because there is no reason of doing that with a thread at hand. The thread can be physically blocked end of story.
But if we had a task backed by a co-routine, we could provide an alternative Ada.Text_IO for such tasks. Preferable selected automatically per the task aspect. The implementations there are rather straightforward. Say, under Windows:
delay 0.0) if the I/O is pending.Under Linux one can use poll() calls etc.
The standard library can provide some nice tagged root type for user-provided I/O, e.g. for sockets.
Interaction with proper tasks needs some consideration, e.g. how an entry call from a co-routine to a proper task is made etc.
this sounds basically excatly what I’m trying to do, but there is a big issue.
Jorvik/SPARK doesn’t allow you to spawn tasks during the runtime of the program. If i’m understanding correctly, they only allow for a fixed pool of tasks at the start of the program.
So if I did create a custom Ada runtime, there’s no way to prove code that uses that runtime, unless that client program also did a fixed static pool of Tasks, which I feel like would defeat the purpose of all of this.
The profile will be modified because the co-routines sharing the same task or a pool of tasks are scheduled in a certain way so that the standard assumptions do not apply to them. They have no priority of their own, get never preempted otherwise than through the carrier task etc.
how do i modify a profile like Jorvik to work with a custom RTS where I can (theoretically) spawn tasks whenever I want? Wouldn’t that cause some horrible errors that can’t be caught by SPARK if I get my assumptions wrong?