From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1751912AbdJTNYg (ORCPT ); Fri, 20 Oct 2017 09:24:36 -0400 Received: from mx1.redhat.com ([209.132.183.28]:26324 "EHLO mx1.redhat.com" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1751579AbdJTNYe (ORCPT ); Fri, 20 Oct 2017 09:24:34 -0400 DMARC-Filter: OpenDMARC Filter v1.3.2 mx1.redhat.com 591AFFED4 Authentication-Results: ext-mx05.extmail.prod.ext.phx2.redhat.com; dmarc=none (p=none dis=none) header.from=redhat.com Authentication-Results: ext-mx05.extmail.prod.ext.phx2.redhat.com; spf=fail smtp.mailfrom=jpoimboe@redhat.com Date: Fri, 20 Oct 2017 08:24:32 -0500 From: Josh Poimboeuf To: Torsten Duwe Cc: Miroslav Benes , Joao Moreira , live-patching@vger.kernel.org, linux-kernel@vger.kernel.org, mmarek@suse.cz, pmladek@suse.com, jikos@suse.cz, nstange@suse.de, jroedel@suse.de, matz@suse.de, khlebnikov@yandex-team.ru, jeyu@kernel.org Subject: Re: [PATCH 0/8] livepatch: klp-convert tool Message-ID: <20171020132432.majphjzzfrbcrdos@treble> References: <20171011024615.y55lwbgpgo6b5dll@treble> <14124e34-04f7-950e-72fb-64f13e62f57e@suse.de> <20171019130146.uxjuhgn2t3yavgz2@treble> <20171019140338.pngwewyzllaw2wu5@treble> <20171019151522.5ih3egvzr3wm3h7r@treble> <20171020124432.GB20306@lst.de> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Disposition: inline In-Reply-To: <20171020124432.GB20306@lst.de> User-Agent: Mutt/1.6.0.1 (2016-04-01) X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-4.5.16 (mx1.redhat.com [10.5.110.29]); Fri, 20 Oct 2017 13:24:34 +0000 (UTC) Sender: linux-kernel-owner@vger.kernel.org List-ID: X-Mailing-List: linux-kernel@vger.kernel.org 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