if Wq = K.Null_Wq then -- Ada equal
Wq := K.Create_Singlethread_Wq ("flash_led_wq");
end if;
if Wq /= K.Null_Wq then -- Ada not equal
K.Queue_Delayed_Work(Wq,
For all that fancy types Ada has, it is still plain pointers underneath. There are no destructors to release resources, no fancy error handling to avoid types.
Extra "unsafety" points in these series: "printk" security vulnerabilities, and standard headers re-implementation that'll likely break in subtle ways in future kernel versions.
- What if ... forgets this "Wq = K.Null_Wq" check : The goal was to KISS. Air bagging such trivial code never crossed my mind in regard to the original intent; Share Ada's raw power, no fuss.
- ... still plain pointers underneath ...: Well when you need to survive, the dirty blade is still an option. That is what keeps it so powerful too. If there were no pointers, another pal would come and say: "aargh, another sandboxed language...". Actually, Ada is healthy about pointers and I would think twice before getting rid of them completely.
- There are no destructors ...: Well yes, controlled types. You are welcome to give a try to bring them in kernel space. I did not have the time to even try. Maybe it is low hanging, really I dont know.
- Extra "unsafety"... "printk" security vulnerabilities : Were there claims to harden the Linux API? I do not recall.
- Extra "unsafety"... re-implementation ... likely break : To be fair, I think I repeated three times in the series a version of "we do not recommend re-implementation, reconstruction of APIs. wrappers inherit fixes, its only to show nuts and bolts, etc"
With all due respect, I think you should at least re-read the introduction and the "Linux Driver Experiment In Ada, But Why?" section. It gives a good common sense view of the intended scope of the series: no more, no less.
With all that said, addressing your points would make an interesting follow-up series. Maybe if I find the time or you decide to take up on the task we could see where it leads!
Thanks for chipping in.
You can get ownership tracking with SPARK, but you need to use proof techniques.
There are pointers in Ada, but it's not at all the same as in C. First, C pointers are really addresses, references and pointers in Ada. And pointers come in various flavors named/anonymous access-to-variable/constant/subprogram, pointing only to the heap or also to the stack, with accessibility levels depending on where the type is defined... which lead to fine-grain distinction of the various use cases with SPARK so that only correct use is provable.