From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from r-passerv.ralfj.de (r-passerv.ralfj.de [109.230.236.95]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 503D022170B for ; Wed, 26 Feb 2025 14:14:57 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=109.230.236.95 ARC-Seal:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1740579298; cv=none; b=J/rHU1bILnTNgT3G7oEFf0SElwLK6VBnagM9CYkOXXCzh1SlCW57NewKJIvh74ySnutLhdQ+vbXowP0t1197s8J/GEBtBg5thl4GXkSamCea4ws+ZwSLS2an9oYjETEp4oE8pZeouvkfoIaJqXPW/ouTUNMMRWlWWzNXfiznibg= ARC-Message-Signature:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1740579298; c=relaxed/simple; bh=coG8/tZzBytDDxqJEp/NCjNfmWL8rr4syevp4nIuyog=; h=Message-ID:Date:MIME-Version:Subject:To:Cc:References:From: In-Reply-To:Content-Type; b=BZ15w/xz6oR/DJ2yXHzmCEtHZvzgVQPxtPcSCaI5FA7Oe/egPjYvdtLrY1Ik/htvhTVcqZkQsmUqthDXwop6xOMItDZyjvJhZq2Y6LDYYE2jEAj3yTWu8L/sS2inio+TrdCqTVUDbspoNvTHmVo5CL/aMDCB8ig+9BBS7r9otT0= ARC-Authentication-Results:i=1; smtp.subspace.kernel.org; dmarc=none (p=none dis=none) header.from=ralfj.de; spf=pass smtp.mailfrom=ralfj.de; dkim=pass (1024-bit key) header.d=ralfj.de header.i=@ralfj.de header.b=llSTqnGU; arc=none smtp.client-ip=109.230.236.95 Authentication-Results: smtp.subspace.kernel.org; dmarc=none (p=none dis=none) header.from=ralfj.de Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=ralfj.de Authentication-Results: smtp.subspace.kernel.org; dkim=pass (1024-bit key) header.d=ralfj.de header.i=@ralfj.de header.b="llSTqnGU" DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; d=ralfj.de; s=mail; t=1740579295; bh=coG8/tZzBytDDxqJEp/NCjNfmWL8rr4syevp4nIuyog=; h=Date:Subject:To:Cc:References:From:In-Reply-To:From; b=llSTqnGUL8JOeW6QfSLsCl03gTTqLIZz82DepLZdR+nn7sAt7g4Cen28sIAZS/V5H eOJpe6LTsfrFGFvG54aFdb7Mofc2v6HRBfdsLAwpbXbOSTinySEbp0EGvxs/8YmqCw KOVs0mpWCx835aZLAZJ0OuaVf0q1Ix7pmHIM5haQ= Received: from [IPV6:2001:67c:10ec:5784:8000::87] (2001-67c-10ec-5784-8000--87.net6.ethz.ch [IPv6:2001:67c:10ec:5784:8000::87]) by r-passerv.ralfj.de (Postfix) with ESMTPSA id 805572052D08; Wed, 26 Feb 2025 15:14:55 +0100 (CET) Message-ID: <91dbba64-ade3-4e46-854e-87cd9ecaa689@ralfj.de> Date: Wed, 26 Feb 2025 15:14:54 +0100 Precedence: bulk X-Mailing-List: ksummit@lists.linux.dev List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 User-Agent: Mozilla Thunderbird Subject: Re: C aggregate passing (Rust kernel policy) To: Ventura Jack , Alice Ryhl Cc: Linus Torvalds , Kent Overstreet , Gary Guo , airlied@gmail.com, boqun.feng@gmail.com, david.laight.linux@gmail.com, ej@inai.de, gregkh@linuxfoundation.org, hch@infradead.org, hpa@zytor.com, ksummit@lists.linux.dev, linux-kernel@vger.kernel.org, miguel.ojeda.sandonis@gmail.com, rust-for-linux@vger.kernel.org References: <20250222141521.1fe24871@eugeo> <6pwjvkejyw2wjxobu6ffeyolkk2fppuuvyrzqpigchqzhclnhm@v5zhfpmirk2c> Content-Language: en-US, de-DE From: Ralf Jung In-Reply-To: Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit Hi all, > Tree borrows is, as far as I can tell, the successor to stacked borrows. > > https://perso.crans.org/vanille/treebor/ > "Tree Borrows is a proposed alternative to Stacked Borrows that > fulfills the same role: to analyse the execution of Rust code at > runtime and define the precise requirements of the aliasing > constraints." > > In a preprint paper, both stacked borrows and tree burrows are as > far as I can tell described as having false positives. > > https://perso.crans.org/vanille/treebor/aux/preprint.pdf > "This overcomes the aforementioned limitations: our evaluation > on the 30 000 most widely used Rust crates shows that Tree > Borrows rejects 54% fewer test cases than Stacked Borrows does." > > That paper also refers specifically to LLVM. > > https://perso.crans.org/vanille/treebor/aux/preprint.pdf > "Tree Borrows (like Stacked Borrows) was designed with this in > mind, so that a Rust program that complies with the rules of Tree > Borrows should translate into an LLVM IR program that satisfies > all the assumptions implied by noalias." > > Are you sure that both stacked borrows and tree borrows are > meant to be full models with no false positives and false negatives, > and no uncertainty, if I understand you correctly? Speaking as an author of both models: yes. These models are candidates for the *definition* of which programs are correct and which are not. In that sense, once adopted, the model *becomes* the baseline, and by definition has no false negative or false positives. > It should be > noted that they are both works in progress. > > MIRI is also used a lot like a sanitizer, and that means that MIRI > cannot in general ensure that a program has no undefined > behavior/memory safety bugs, only at most that a given test run > did not violate the model. So if the test runs do not cover all > possible runs, UB may still hide. That is true: if coverage is incomplete or there is non-determinism, Miri can miss bugs. Miri does testing, not verification. (However, verification tools are in the works as well, and thanks to Miri we have a very good idea of what exactly it is that these tools have to check for.) However, unlike sanitizers, Miri can at least catch every UB that arises *in a given execution*, since it does model the *entire* Abstract Machine of Rust. And since we are part of the Rust project, we are doing everything we can to ensure that this is the *same* Abstract machine as what the compiler implements. This is the big difference to C, where the standard is too ambiguous to uniquely give rise to a single Abstract Machine, and where we are very far from having a tool that fully implements the Abstract Machine of C in a way that is consistent with a widely-used compiler, and that can be practically used to test real-world code. Kind regards, Ralf