How to spawn a variable number of tasks on startup for SPARK?

General
,
1

Hello!

Messing around a bit more with Ada, but a problem I"m running into is spawning a variable number of tasks on startup (specifically aiming for a “thread per core”).

For whatever reason, I can’t seem to figure out a way to get this working with SPARK.

Is there some way to do this? Maybe passing in the CPU core amount through a CLI argument or something?

package Workers is


   Worker_Count : constant Positive := (I want Task Per CPU here)

   task type Worker;


   type Worker_Array is array (Positive range <>) of Worker;


  Workers : Worker_Array (1 .. Worker_Count);




end Workers;
2

I think the function Number_Of_CPUs in package System.Multiprocessors is what you’re after here.

3

AFAIK, SPARK can only work with tasks if they follow the Ravenscar and Jorvik profiles. Both profiles require tasks to be pinned to a CPU (no dynamic dispatch) and they cannot die. I do not know how you would be able to create an unbounded set of tasks on a core where you do not know how many tasks you have and how many cores you may run on…

You can read more about this on Concurrency and Real-Time - learn.adacore.com and Use the Jorvik Profile (CON02) - learn.adacore.com

Maybe have a compile-time evaluation of some formula/function that will allow the compiler to optimize the number out and not make it a runtime thing?

Best regards,
Fer

4 
Worker_Count : constant Positive := System.Multiprocessors.Number_Of_CPUs;
5

So I tried this but System.Multiprocessors does not work in spark

@damaki @OneWingedShark

6

Yeah, maybe if there was some way to see the number at compile time with a .env file or something? Not totally sure if that would work with SPARK

7

Okay I think the best shot here is to take these two files And I can either vendor them into my own project and slap a SPARK_Mode on them, or send a patch to GCC to add spark_mode on them.

8

This is not specific to SPARK. You can use GPRbuild to read external variables and inject those variables into the source code. I do not know if it uses specific GNAT features (preprocessor).

Alire for example generates an .ads file at build time that can be used by the application. That file takes external information and makes it available to your Ada application. You could take this other approach with something like Makefiles for example.

I hope this helps. Best regards,
Fer

9

Ah, looks like this file is not yet in SPARK. Instead of vendoring or trying to patch the runtime, I recommend instead wrapping this function whose spec is in SPARK but the body is hidden.

In your package spec (with SPARK_Mode => On):

function Number_Of_CPUs return System.Multiprocessor.CPU
with Global => null;

Then in your package body, you can hide the implementation from SPARK:

function Number_Of_CPUs return System.Multiprocessor.CPU
with SPARK_Mode => Off
is
begin
   return System.Multiprocessor.Number_Of_CPUs;
end Number_Of_CPUs;
10

Make a wrapper for System.Multiprocessors.Number_Of_CPUs, disable SPARK in the body.

11

Okay so that ended up working but now I have a bit of an awkward workaround.

Essentially, since I’d like for this to work on computers with differing levels of CPU cores, I have a Max Amount of Workers, and only a small subset of those get pinned to a CPU core, and the rest have to share a single leftover CPU core.

this is needed cuz Jorvik doesn’t allow for dynamic spawning of Tasks, so the best way around this is to just spawn an array of tasks and spawn more than I actually need to cover my bases here.

This state of affairs sucks especially if for example I was running this bit of code on something that has only 4 cores, which mean one core would have to run 30 tasks.

Is there any way to work around this or is this just how the cookie crumbles?

I figure if I’m stuck with this design decision, I could just make that leftover CPU core used for “low priority jobs” that don’t really need the fast thread pinning route.