The runtime verification subsystem

Posted Jun 9, 2021 17:57 UTC (Wed) by bristot-memorial (guest, #61569)
Parent article: The runtime verification subsystem

A potential user of RV, that will feed the subsystem with models, seems to be the automotive case. Here [1] are the slides of the talk "A maintainable and scalable Kernel qualification approach for Automotive", presented at the last Elisa Workshop, where we explain how the RV can help in this effort.

https://bristot.me/files/linux_iso26262_approach.pdf

The runtime verification subsystem

Posted Jun 10, 2021 3:29 UTC (Thu) by alison (subscriber, #63752) [Link] (2 responses)

Thanks for posting that link.

BUG_ON() and WARN_ONCE() and their friends are ad hoc largely undocumented expressions of an underlying model. The new work will make the model explicit and encourage discussions about the logic as well as the implementation details.

The runtime verification subsystem

Posted Jun 11, 2021 15:26 UTC (Fri) by bristot-memorial (guest, #61569) [Link] (1 responses)

Exactly, an explicit model is the main benefit of the approach. For the wider audience: http://jasss.soc.surrey.ac.uk/11/4/12.html

The runtime verification subsystem

Posted Jun 12, 2021 20:56 UTC (Sat) by alison (subscriber, #63752) [Link]

> an explicit model is the main benefit of the approach.

The main advantage of an explicit model is that it will express the kernel's desired behavior. BUG_ON() etc. are needed because the kernel's actual behavior deviates from the model. One can envision a future where a patch that addresses the problem that triggers a backtrace would be required to include a diagram illustrating the deviation from the agreed model. Imagine how much easier such a practice would make reading Linux mailing lists!