Received: by 2002:a05:6a10:206:0:0:0:0 with SMTP id 6csp2114214pxj; Wed, 19 May 2021 23:59:26 -0700 (PDT) X-Google-Smtp-Source: ABdhPJw39DUfgAJIyaz4ssYQkKqO8a7kKGiNCQ7GiK/MidgkrDQXM57iECmLojP1/DRdHdFK3bvR X-Received: by 2002:a05:6402:1207:: with SMTP id c7mr3383122edw.387.1621493966112; Wed, 19 May 2021 23:59:26 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1621493966; cv=none; d=google.com; s=arc-20160816; b=LiZszihour/RwXujIHd/xYOY659iY+SRvROAu9isoRc1O9QSZ1ye7qEcmdP8TkihKn 6esFTxuokwF3ewF9Ky22+zwq5+WW4neq7WJgmYZ6sPQm4ZaBj84I5CVrlqAbk0iz8Phz Xl53RkGTF69RsotB8Xwkdv6Ck5UfoAUh5ODRMALVmnK8EnM7fE6jIH/+THSjc3j4JDGO 88CNxl7GMdXYhAzUtLP9JU3XFtcrMpvYoaPOrRnxHuPngqWlhwlstEzqwU2pY1mu9/9m cI4DOTB3C1bsXiVpgG0J1aNBJmxF8B0k0fo6qQ//BHIlg3efU167ZAYwlYkiktKof4PL O3iw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-id:precedence:content-transfer-encoding:content-language :in-reply-to:mime-version:user-agent:date:message-id:from:references :cc:to:subject:dkim-signature; bh=9tEv83ZtFMHbXTaEtn+9i7YCHaEzdnQPBIaLpxqVr78=; b=kv5J5XJcFusbn6dIkbHc832uK2Lt2IXka4pUdPPqGflzkAggy1YiOCP/AISAnj+MEm jyMs4vf/WtV54eTljU3TOZ3ykjmLX1m5J5yQrDCSk1RO4w9u3ijeVBPe9erEbw41CXMx as+mJZa4CX5EO4U6NkhhbnZ8A9Q4pBDehQI9TACl+sSu8jsiWQu8uPRYSp1E9dMT++21 UDdOfT36hhAlZQ4vRC2VWgbk6DfPdLTMSmvHILv4/cT6vR4bj/Ovi4kAptljH6MnoF8J CJy9QtDBUC39bP+ziZ7mMD3VFwj3cHHnpvSiysdTBRVVpGR1++cEhUwct7JpVy43osmk YdtA== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@redhat.com header.s=mimecast20190719 header.b=aNwwmVaO; spf=pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 23.128.96.18 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=redhat.com Return-Path: Received: from vger.kernel.org (vger.kernel.org. [23.128.96.18]) by mx.google.com with ESMTP id b4si1498309eds.344.2021.05.19.23.59.02; Wed, 19 May 2021 23:59:26 -0700 (PDT) Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 23.128.96.18 as permitted sender) client-ip=23.128.96.18; Authentication-Results: mx.google.com; dkim=pass header.i=@redhat.com header.s=mimecast20190719 header.b=aNwwmVaO; spf=pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 23.128.96.18 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=redhat.com Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S231193AbhETG4S (ORCPT + 99 others); Thu, 20 May 2021 02:56:18 -0400 Received: from us-smtp-delivery-124.mimecast.com ([216.205.24.124]:58944 "EHLO us-smtp-delivery-124.mimecast.com" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S231237AbhETG4F (ORCPT ); Thu, 20 May 2021 02:56:05 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=redhat.com; s=mimecast20190719; t=1621493683; h=from:from:reply-to:subject:subject:date:date:message-id:message-id: to:to:cc:cc:mime-version:mime-version:content-type:content-type: content-transfer-encoding:content-transfer-encoding: in-reply-to:in-reply-to:references:references; bh=9tEv83ZtFMHbXTaEtn+9i7YCHaEzdnQPBIaLpxqVr78=; b=aNwwmVaOOt0LMpB+kdAX+Vl4pm7ZsABBOLww3gCG7isUZy60nqG+/YGU80k//OJ6Lm6mCp 80OkdJAzCNBLKfhSQtwmUsGF0NEEmVb0peY5aqQT6dOSLhkgoeqsu+yYHHpy1GaFIzpgI2 govukGnE4GKe/7rm3Axo+pFln26+Mlk= Received: from mail-ej1-f70.google.com (mail-ej1-f70.google.com [209.85.218.70]) (Using TLS) by relay.mimecast.com with ESMTP id us-mta-61-vKAB4UWmN6C0olnK9bgCSg-1; Thu, 20 May 2021 02:54:42 -0400 X-MC-Unique: vKAB4UWmN6C0olnK9bgCSg-1 Received: by mail-ej1-f70.google.com with SMTP id la2-20020a170906ad82b02903d4bcc8de3bso4578300ejb.4 for ; Wed, 19 May 2021 23:54:42 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:subject:to:cc:references:from:message-id:date :user-agent:mime-version:in-reply-to:content-language :content-transfer-encoding; bh=9tEv83ZtFMHbXTaEtn+9i7YCHaEzdnQPBIaLpxqVr78=; b=rcF4n8tm6L2JLhryLrt+OZaCq94YbF1uTjqydWkYR3Zdr3DKW1rKW27WG9UDAX3xuQ gxnwbSI/Jye7rOIq1lKTPkLJ4SrFEhmROW4r2DXveYF/UGuAlewXZXyc2DfskH9WCglL dPiQAMpwnTVAyB7IB/bdOQ6ZKUqDe3ULt7b2cweIChe8lqB6S0JCxoc0hpvmII7mLGo6 7W0+8Nwgj43hdnPgyAwQvaBEkvvCIXT3TngrrrYFgHP7OvWgKASh8sDIkUaFaLjXnb4v 2thLn+Ke3VpRym/b0Xb5XW3OmUxfzjHXFs3pG22zW3VAmhU6fNPyf3FhUdSohe4/BEd4 htjQ== X-Gm-Message-State: AOAM530Ck85HO/Xwgpg5mKR/5QwqFUMT4SXirzedPJLK1+O/MfL0DtKD 8qto9zhKkTv+bQzd6k8uYjkLGYdRgId3YzrbrFEh4UM90n72Fvjn6iQe4H7Sxf/KViFM/ceCWO+ RH80t/B7PPuAbiWI+K1RLjzt0 X-Received: by 2002:a17:906:fa93:: with SMTP id lt19mr3200253ejb.14.1621493681154; Wed, 19 May 2021 23:54:41 -0700 (PDT) X-Received: by 2002:a17:906:fa93:: with SMTP id lt19mr3200227ejb.14.1621493680938; Wed, 19 May 2021 23:54:40 -0700 (PDT) Received: from x1.bristot.me (host-87-19-51-73.retail.telecomitalia.it. [87.19.51.73]) by smtp.gmail.com with ESMTPSA id hz10sm909238ejc.40.2021.05.19.23.54.39 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 19 May 2021 23:54:40 -0700 (PDT) Subject: Re: [RFC PATCH 01/16] rv: Add Runtime Verification (RV) interface To: Randy Dunlap , linux-kernel@vger.kernel.org, Steven Rostedt Cc: Tommaso Cucinotta , Kate Carcia , Jonathan Corbet , Ingo Molnar , Mauro Carvalho Chehab , Thomas Gleixner , Peter Zijlstra , Will Deacon , Catalin Marinas , "Paul E. McKenney" , Joel Fernandes , Mathieu Desnoyers , Gabriele Paoloni , Juri Lelli , Clark Williams , linux-doc@vger.kernel.org References: <90c917eb-f0a8-3ef5-b63d-d88c1f6919a1@infradead.org> From: Daniel Bristot de Oliveira Message-ID: Date: Thu, 20 May 2021 08:54:39 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.10.1 MIME-Version: 1.0 In-Reply-To: <90c917eb-f0a8-3ef5-b63d-d88c1f6919a1@infradead.org> Content-Type: text/plain; charset=utf-8 Content-Language: en-US Content-Transfer-Encoding: 7bit Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org On 5/19/21 8:10 PM, Randy Dunlap wrote: > On 5/19/21 4:36 AM, Daniel Bristot de Oliveira wrote: >> diff --git a/kernel/trace/rv/Kconfig b/kernel/trace/rv/Kconfig >> new file mode 100644 >> index 000000000000..e8e65cfc7959 >> --- /dev/null >> +++ b/kernel/trace/rv/Kconfig >> @@ -0,0 +1,13 @@ >> +# SPDX-License-Identifier: GPL-2.0-only >> +# >> +menuconfig RV >> + bool "Runtime Verification" >> + depends on TRACING >> + default y if DEBUG_KERNEL > > No need for default y. There are other reasons to use DEBUG_KERNEL > without wanting RV turned on. yes, you are right, I will remove it. >> + help >> + Enable the kernel runtime verification infrastructure. RV is a >> + lightweight (yet rigorous) method that complements classical >> + exhaustive verification techniques (such as model checking and >> + theorem proving). RV works by analyzing the trace of the system's >> + actual execution, comparing it against a formal specification of >> + the system behavior. > > And in the cover/patch 00: > tlrd: > should be > tl;dr: > or at least > tldr: > :) Ack! Thanks! -- Daniel