Can you directly implement stackful coroutines in GNAT Ada? (And can they be proven with SPARK?)

General
, ,
1

I’ve been looking into stackful coroutines lately for my “formally proven async runtime” stuff, and I found out about this little library called minicoro GitHub - edubart/minicoro: Single header stackful cross-platform coroutine library in pure C. · GitHub that does exactly that in C, albeit with a bunch of handwritten assembly.

Since GNAT is directly built on top of GCC, couldn’t a minicoro like library be written in pure Ada, and emit GCC intrinsics or IR? The only issue I see is if an fiber/coroutine somehow exhausted the stack, which means we would need some way to raise an compiler error if/when that happens.

2

A followup question: if I do have to resort to writing assembly anyways, is there a way I can formally prove that assembly does what I think it does using SPARK or some other tool?
(Especially to check if our fiber has too many stack allocated variables saved to it)

3

The last paper in my post here might be useful, take that paper and pop it into scholar.google.com and see if there’s anything there.

However, you could also combine that with the “using high level language as a cross assembler” (SPARK annotating the ‘assembly’ subprograms), and proving that.

4

Alright here’s my attempt at doing stackful SPARK proven coroutines (Note that a lot of this code is AI Generated so take this with a hefty grain of salt)

5

Cross-referencing @Fabien.C’s work.

Are these related to what you’ve asked about?

Note also de Rodat’s work referenced on the Github page above.

6

yes, i actually referenced these directly when working on this stuff, though I ultimately didn’t go the task way since that doesn’t work in Jorvik.

(also each of those required using a thread)