Received: by 2002:a05:7412:8521:b0:e2:908c:2ebd with SMTP id t33csp1757851rdf; Sun, 5 Nov 2023 13:02:20 -0800 (PST) X-Google-Smtp-Source: AGHT+IFNYdhdYzUszc5IiWNGzTn4ZDFB0tiKx3b7F51l+sXNajy/bm4GEUirisMUkgj1m6/EiWFd X-Received: by 2002:a05:6871:8011:b0:1e1:e1f8:ea3e with SMTP id sk17-20020a056871801100b001e1e1f8ea3emr29616056oab.1.1699218140022; Sun, 05 Nov 2023 13:02:20 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1699218139; cv=none; d=google.com; s=arc-20160816; b=S4EkUkiHzzFyMGJxqy5lZsF3PW0SF4ZkaffbiMlOPRx0dzGGWYFcn4hFoiHPo7Nm+K odf+qjHOhSCAUSDBiLGNgok3xdVL68d16lCOsVhO/oFdrH/6WQwD/6CYlOg0BUphyFxD VgXdMH8Y93u8siSChN/c9BqxaN2NVM8JGBw8ZQlqlED9LPsRXLq+HEbdDgGPgG5C117H ALk/BkglZGabwd7s6qNQReKHDfZGq648sEZzapGZfvB4lS11sGii0BEVQjBYY2pzkVDG CXyHjKxMobBNXzUbCflIyxz2FrCwNJjnyUbWJ/R9tJyS0mf4HSLvU4QEQUsdqVDru3k8 YE5g== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-id:precedence:mime-version:message-id:date:user-agent :references:in-reply-to:subject:to:from; bh=vq7O3TUbSoBkx3MZ5DbuZSZiyByqg6wLdlaCecR6oD8=; fh=DE23xN5X/q5HwRELPjc5SwExIEaYC/W2+o6jadk5ehM=; b=bcW5BLQOyhtB2U0tTojqvWAQ69btzsDwiVLZDcrqYI3mwb1metgNnK05eOzm2YlhPt II9FdCqdXgMS2fPnptO37rqGR7Teg2XzWs0RsTZifjruKWEyiXJcypS1T+/PdZE6z7xE DPQUTqeTGyDN6UzXqySMQ+/delZvoGo5fa+pV6TBhKZzwTbjCMoI+X9KDdYVEYQuqOqE ZISeA9VAWaGgWH9pWvqjgqdDOeBbJ9CiUvRtbVcwyTXpQGJSQmWLED/SGD0aS0afqpqa YHhdCpUKfY/R8f7ZovxVGVdoMnvz9sMjQBA5LwlgPkeSjL6GKtZ61w56V8dPGIsT9MWn Q01A== ARC-Authentication-Results: i=1; mx.google.com; spf=pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 23.128.96.38 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org Return-Path: Received: from fry.vger.email (fry.vger.email. [23.128.96.38]) by mx.google.com with ESMTPS id u9-20020a656709000000b00563dfffe7b9si6632847pgf.810.2023.11.05.13.02.19 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sun, 05 Nov 2023 13:02:19 -0800 (PST) Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 23.128.96.38 as permitted sender) client-ip=23.128.96.38; Authentication-Results: mx.google.com; spf=pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 23.128.96.38 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org Received: from out1.vger.email (depot.vger.email [IPv6:2620:137:e000::3:0]) by fry.vger.email (Postfix) with ESMTP id B3032809C191; Sun, 5 Nov 2023 13:02:16 -0800 (PST) X-Virus-Status: Clean X-Virus-Scanned: clamav-milter 0.103.10 at fry.vger.email Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S229448AbjKEVB6 (ORCPT + 99 others); Sun, 5 Nov 2023 16:01:58 -0500 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:51634 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S229447AbjKEVB5 (ORCPT ); Sun, 5 Nov 2023 16:01:57 -0500 X-Greylist: delayed 596 seconds by postgrey-1.37 at lindbergh.monkeyblade.net; Sun, 05 Nov 2023 13:01:53 PST Received: from comms.drone (in.bow.st [71.19.146.166]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 01EA397 for ; Sun, 5 Nov 2023 13:01:52 -0800 (PST) Received: from homebase (unknown [IPv6:fe80::2259:21a4:f292:8bfb]) by comms.drone (Postfix) with ESMTPSA id AC187FDA7; Sun, 5 Nov 2023 20:51:52 +0000 (UTC) From: "Mathew\, Cherry G.*" To: Jonas Oberhauser , linux-kernel@vger.kernel.org Subject: Re: [RFC+Patch] Formal models as source of truth for Software Architects. In-Reply-To: <2defe3ff-90df-2627-dd19-0442a90b20a4@huaweicloud.com> (Jonas Oberhauser's message of "Mon, 30 Oct 2023 11:47:12 +0100") References: <85v8axxrmo.fsf@bow.st> <2defe3ff-90df-2627-dd19-0442a90b20a4@huaweicloud.com> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.3 (berkeley-unix) Date: Sun, 05 Nov 2023 20:49:22 +0000 Message-ID: <857cmw2ael.fsf@bow.st> MIME-Version: 1.0 Content-Type: text/plain X-Spam-Status: No, score=-0.8 required=5.0 tests=HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,SPF_HELO_NONE,SPF_PASS,T_SCC_BODY_TEXT_LINE, URIBL_BLOCKED autolearn=unavailable autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on fry.vger.email Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org X-Greylist: Sender passed SPF test, not delayed by milter-greylist-4.6.4 (fry.vger.email [0.0.0.0]); Sun, 05 Nov 2023 13:02:16 -0800 (PST) Hi Jonas, First of all, sorry for my late reply - I note with thanks, that you spent some time and attention on your email, so I wanted to spend some time composing a thoughtful reply. I'm replying in context below: >>>>> Jonas Oberhauser writes: [...] > A few years ago we also built systems to extract models from C > code (for TLA+ back then), but those systems are now totally > unused (and unmaintained) due to poor scalability of exploratory > state-based model checking. > And then there's the issue that many engineers don't know how to > write reasonable temporal assertions, especially not ones that can > give sufficient guarantees to be worth the extra effort and > maintenance. So my arrival at "D3" and spin was a progression of looking at what's available (in the open domain), current consensus around development methodology, and progress in hardware capacity. I've used TLA+ for protocol verification, and while it's great for that, I didn't see it translate to and from implementation code. The best I was able to do was to use a functional language to mirror the lambda calculus - see: https://github.com/byisystems/byihive for eg: One of the main motivations for my current "D3" path is to provide a cleaner separation between design and implementation - where the "Architect" role does design, and the "Engineer" role does implementation. This allows for each role to focus on what they do best, while the machine is tasked with maintaining functional equivalence. I suspect that your experience was due to the fact that engineers had to get involved in design, without understanding or consenting to this. > If we use a simplified model of what the system should be doing to > specify, then usually we are not looking for equivalence but only > for uni-directional simulation: the spec usually needs to have > more degrees of freedom than the implementation, which is just a > single implementation. So spin has two approaches - one uses the inline "C" to glue the spec as a sort of "test driver" for implementation code if required. The other uses a separate source level model extractor, to rebuild the implicit model in the implementation C code. I am leaning towards the latter, because it seems to help with streamlining the software development process as an iteration - which helps especially in early nascent stages of design & development. What I'm beginning to see is that once design "settles down", then the iterations become less disruptive. But initially, the Architect/Engineer hats need very good interaction. > What has worked well for us is anything that works > - directly on the code > - doesn't require learning any kind of math to find bugs with > - is scalable enough to find bugs on real code > - doesn't require a lot of extra effort from the engineers > (compared to the extra assurance you get) > - doesn't need to be adapted whenever the code changes Have you seen spoq ? https://www.usenix.org/conference/osdi23/presentation/li-xupeng They use this approach - one of the reasons I'm not fully convinced by this approach is because, I believe that the source of truth being in implementation code limits flexibility, for eg: reuse. If you notice my original patch, the model is a reference for both the NetBSD and Linux drivers - nothing stops it from further OSs (as long as the codeflow logic doesn't vary too much - and even then, the model could itself be made modular to accommodate different FSMs) > I find in software, usually blueprint and skyscraper are in some > sense the same thing. Or in some sense, the skyscraper is > extracted automatically by a compiler/interpreter and installation > system - we never actually dig anything ourselves, but have the > ability to experiment directly on the blueprint as we build it. > That's because languages already try to provide us reasonable > abstraction mechanisms by which we can simplify the code and make > it more "model-like". Can you give me an example of how this works/a pre-existing tool that helps with this simplification ? I'm actually currently looking at re-writing modex to do precisely this (but with the translation end-point being something close to the original model). > So writing the blueprint twice - once in some modelling language > and once in a language meant for execution - doesn't really > provide a lot of benefit. But it requires doing changes at two > levels whenever the software design changes. It just violates DRY. IMHO, this would be true if: a) The implementation language was expressive enough to cleanly encapsulate the model. b) If the toolchain around it were able to do model verification (eg: by exploring LTL bounds). I've heard good things about rustlang wrt. a), but not b) - would be keen to know more. > What makes sense in our experience is identifying properties you > would like the system to have and devising a specific checking > mechanism for that. For example, you might specify the protocol > of how the device communicates with the system and what > assumptions it has (like "don't start a second command while the > first one hasn't finished"), and then check that the driver code > obeys this policy. Then you can change the software code without > touching the protocol specification, and just re-verify. > In the easiest case, the protocol can be a mock device process > that is inserted via a form of dependency injection to talk to the > real driver code during verification, and if the code isn't too > complex you can exhaustively check several test cases. Ok, from what I understand, this is a "system model" - when I talk about D3, I'm purely talking about the software model. This model may be part of a larger scope "system model". Event-B http://www.event-b.org/index.html https://web-archive.southampton.ac.uk/deploy-eprints.ecs.soton.ac.uk/111/1/sld.ch1.intro.pdf is an interesting (closed) industry take on what you seem to be describing - and they seem to have taken a more "D3" like approach - I don't have much insight into their experiences though, although I'm speaking to one of their practitioners. > Only if the code is highly unreadable for specific reasons like > performance or talking to legacy ABIs, it can make sense to have > an "executable comment" that implements the same functional > behavior in a very concise, readable way (with crud > performance/mock APIs replacing the actual behavior), and check > that the real code and the "executable comment" do "the same > thing". I'm a bit skeptical about the "doxygen" approach (i've seen this in some versions of Java iirc, as well) - basically you're bypassing all the goodness that the language parser provides by hiding from it - I'm not sure how this is useful other than to shimmy in a specific bandaid fix. Which is fine, if you're fighting fires, but I think for a more structured approach, I'm not seeing what you're seeing, I'm afraid. Open to be signposted though. > The main issues I see when we look at it through the skyscraper > analogy is that usually people in other engineering disciplines > have CAD tools - backed by very powerful computers - to really > systematically and thoroughly check the design. What we usually > have is stress testing and some test suites built by hand that > miss many cases. Interestingly, I was surprised at the amount of compute available "off the shelf" - the other day I sent a model for help, saying with a bit of trepidation that that it might take about 25G of RAM and thrash the machine, so please be careful - the volunteer came back to me and said he has 128G RAM available, and 1TB RAM on a pinch! What takes an hour to run on my i5 + 16GB laptop, took him 3minutes! So in some sense, I believe we're nearing the "Deep Neural Nets" moment, when GPU computation took inference to the next level. > Anyways, that's my (limited) experience. > Hope it helps, Yes - thank you so much for your interest! I look forward to further comments - and also, if there are industry applications that benefit from the broad intersect, any signposts will be much appreciated! Best, -- MattC