On Fri, Oct 20, 2017 at 02:44:32PM +0200, Torsten Duwe wrote: > 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. Huh? The obj-based approach (e.g., kpatch, bin-diff) inherently detects such changes. Or am I misunderstanding? If so, please elaborate. > 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? I agree that would be the best option. I don't think anyone has measured it because we don't know how to get the compiler to do that :-) My guess is that it will be something close to negligible. > > 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. Can it also prove that the patch is applied in a safe manner? -- Josh -- 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
