Quotes of the week

Posted May 3, 2019 6:39 UTC (Fri) by mjthayer (guest, #39183)
In reply to: Quotes of the week by roc
Parent article: Quotes of the week

To what extent is it feasible to write code which is valid C but more amenable to static correctness analysis?

Quotes of the week

Posted May 3, 2019 6:41 UTC (Fri) by mjthayer (guest, #39183) [Link] (1 responses)

Which I suppose is more or less what all the MISRA and other people are trying.

Quotes of the week

Posted May 3, 2019 23:23 UTC (Fri) by roc (subscriber, #30627) [Link]

MISRA disallows, among other things, dynamic memory allocation. MISRA and similar schemes are far too limited to use for the Linux kernel.

Quotes of the week

Posted May 3, 2019 23:30 UTC (Fri) by roc (subscriber, #30627) [Link] (1 responses)

Either you write in an incredibly restricted subset of C that is totally infeasible for something like the Linux kernel, or you write in a larger subset of C with annotations to help the static analyzer/verifier prove absence of classes of bugs. The problem with the latter approach is that even though a C compiler might compile your code, you're not really writing C anymore, you're writing a superset of a subset of C that everyone other than the C compiler needs to understand. And is twisting the syntax and semantics of your language so that a C compiler can compile it really worthwhile, or should you take the opportunity to fix some of the bad C decisions?

It's possible that creating your own language that's a bit like Rust but looks more like C unlocks some incrementality benefits for Linux (while having some pretty major costss). It's hard to tell without doing experiments.

Quotes of the week

Posted May 6, 2019 23:09 UTC (Mon) by logang (subscriber, #127618) [Link]

We already do the latter approach in the kernel to a small extent. We have a number of annotations[1] that are checked by sparse and also understandable by code reviewers.

I think it would be a great idea to do more annotated static analysis if people can come up with good cases where it will work.

Also, I feel like it would be of a significant value to add much of the same functionality that sparse is doing now to GCC and maybe eventually the C spec so that it's more widely available and developers can get the appropriate errors without needing to run a seperate tool, or wait for a build bot.

[1] https://elixir.bootlin.com/linux/latest/source/include/li...