I don't like coding but I really liked Ada, and I'm very new to it. So could you please clarify these points to me?
If you have a computer with a single non-threaded CPU, tasking will still be single-CPU. The same of course applies to forking in C or C++.
Question: Do you think Ada tasking provides any benefits over forking in this scenario?
I also want to know why SPARK prohibits tasking (I know it's for safety, but how exactely, how can prohibiting tasking improves safety.)
My third and last question, if I want to provide "safe tasking" (in Ada), what limitations on tasks could I envision would be required to make using them (tasks) "Safe".
Thank you,
1) Yes. The easiest argument being that Ada tasks run in the same process context, making tasks/threads somewhat faster than separate processes. The language level inter-task communication and synchronisation features are another reason.
2) Only some versions of SPARK prohibit tasking. RavenSPARK (2005) allows tasking, and allows formal reasoning about tasking. The problem with tasking is that it is hard to reason formally about, especially with the ambitions of the SPARK team (proving correctness).
3) You could consider limiting yourself to the Ravenscar profile. But plain Ada tasking is already relatively safe (even if it can't prevent you from writing nice dead-locks).