On Thu, Oct 19, 2017 at 06:00:54PM +0200, Miroslav Benes wrote: > On Thu, 19 Oct 2017, Josh Poimboeuf wrote: > > > > Sounds nice, though I wonder what the obstacles are? > > Those GCC optimizations you mentioned below and which I didn't connect to > klp-convert itself. I have a bad feeling about the IPA stuff in general. An obj-based approach is cool in a way that it still works, and is sure to work, if the IPA assumptions that led to the optimisations still hold, but as soon as they break, you're screwed big time. For -fpatchable-function-entries I switched off IPA-RA, as especially on RISC there's _nothing_ you can do between functions without at least one scratch reg. But for live patching, I'd like the kernel to be compiled in the first place with 100% ABI adherence, IOW all IPA optimisations turned off. Does anyone have numbers on the performance impact? > Nothing serious aside from that, I hope. Nicolai is currently implementing > C parser for kernel sources. > > > > You could verify the result and its correctness. > > > > Does that mean it's easier to do code review? Or something else? > > Yes, the code review. > > > > It could also be beneficial if we'd like to pursue automatic > > > verification in the future. > > > > What do you mean by automatic verification? > > Formal verification. Theoretically we could have a formal specification of > our consistency model and we could prove/disprove whether a livepatch and > its implementation are correct with respect to it. It is a vague idea > though and I personally haven't got sufficient knowledge to do anything > about it. For example, if the patched functions and the fixes meet its criteria, you could use CMBC (http://www.cprover.org/cbmc/) to _prove_ that the live patch changes exactly what you claim to, and nothing else. Torsten -- To unsubscribe from this list: send the line "unsubscribe live-patching" in the body of a message to majordomo@xxxxxxxxxxxxxxx More majordomo info at http://vger.kernel.org/majordomo-info.html
