The same way you would modify the compiler and SPARK prover?
Co-routines are scheduled in a more deterministic way than time-shared ones. They also cannot do certain things normal tasks can. From that follow the restrains one have to put on them in order to, for example, prevent deadlocks. I believe that for co-routines one could lift the constraint that a task cannot be started dynamically. If not, then not.
On the other hand the number of entries might be zero. One normally does not communicate with co-routines and access discriminant would probably suffice for most applications.
It is a serious thing. You should probably start penning an AI.
From my experience I can say that co-routines would be far more useful than all Ada amendments put together since Ada 2005. Implementation of communication protocols in an asynchronous data-driven way is extremely tedious and error-prone.
You can write package specs with SPARK annotations enabled (SPARK_Mode => On) and the appropriate contracts, then hide the package bodies from SPARK using SPARK_Mode => Off. This allows the package to be used from SPARK code, but allows for more freedom in the implementation.
However, I’m planning on rewriting the whole thing by hand since I’ve proven that this can all work under SPARK (except for the assembly/C FFI), and I don’t want to share the code publicly until I have done so. As such, if you would like access to this repository, DM me (or just respond with your github username on this thread I guess) and I can add you to the repository and you can take a look.
I wouldn’t mind if you would want to fork the repository and make it public if you want either, as long as you credit me of course lol.
I’m curious if you guys can figure out a way to either remove the assembly or make the remaining C FFI SPARK provable
Well, I was wondering if having some fixed set of workers via Tasks, and then functions to schedule work atop those Tasks, would make sense. In that case, you can have your semi-natural uncolored call styles, and then Tasks/Protected Objects would take care of the work behind the scenes. It likely would be gnarly versus just using Tasks directly, but it could be interesting as well.
The use cases are massively concurrent computations:
Network server. The number of sockets is far greater than the number of system threads.
Number crunching. For example a parallel multiplication of large arbitrary precision numbers. A worker set based implementation is easily beaten by a non-parallel algorithm. (see a test in the Simple Components)
Otherwise, certainly an implementation of co-routines should support a pool of carrier tasks backed by OS threads. However that would make SPARK proofs harder, I guess.
I feel you. However, as far as I know, even AdaCore has had to verify some of their C/ASM for some systems just because that was the only way to do it. For example, the boot system for an MCU is generally written in ASM. Yes, it is a small file, but you just cannot write that in Ada (unless you do a ton of hacks to your code, compiler and linker) and it would most likely just be Ada calling some inlined assembly. So, do not feel bad about it.
Also, you can have proven code that runs on top of unproven C/ASM code but still guard against it. If you want some examples of that, please, take a look at SPARKlib and its C bindings.
Actually, this is another thing that is done in the industry. You get an accepted/certified OS (VxWorks, PikeOS, RTMES…) and use thorse primitives. That way, you know that your code is using certified code and you can proof things on top of that. So this is not too bad tbh.
If you do not want a full OS implementation, use a library, such as LibUV https://libuv.org/ which is used by a large number of projects and it is very mature.
One (basic and obvious) tip. Try to minimise the global state. If you cannot, then try to change the “global” state to scoped state. By scoped, try to make it so that global state becomes “package level” or “task family level” or “different structs instead of a single struct with a lot of data” or vice versa (this last point). It can sometimes help.
I can’t find it now but I came across commentary a while back from a long time ago on the mailing list about GNAT saying something like
After much work from University… we have finally replaced Ada threads with Posix threads. They’re slightly less light weight but the OS compatibility benefits are welcome.
(username: Irvise)