Received: by 2002:a25:6193:0:0:0:0:0 with SMTP id v141csp626035ybb; Sat, 28 Mar 2020 06:43:45 -0700 (PDT) X-Google-Smtp-Source: ADFU+vuup0Ppo1eQEfOacR2a0QoFwDl0R/9y7zkaoFaNX3omKW1/T39YP9eBdoQCbHvkxW8wrgCC X-Received: by 2002:a9d:27c7:: with SMTP id c65mr2865317otb.318.1585403025655; Sat, 28 Mar 2020 06:43:45 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1585403025; cv=none; d=google.com; s=arc-20160816; b=QEF4pWUtY8b6kiPd4O5KH3fPpDhOV6dCo0nJsPq5cH2LNE8NageHAvvgob0wJ18ea4 8mdl44tJLO+33hGusa1kSCUaXqXoBVDvRU3D0zuTjCuNhZvkyTNMjbthjCQup6TlWVFY uQA9kU7LHf+fsAsh2ScMqaS4WRRLyWd2489BkxHGH4Vm4M4zHYO1G7VY3RfqWBeeR1em 8J+TlIhf9CCMmohIOghiuje9Rwtn6oO9Wis3ZXIB1NqqvOSCYOVRFzp4ii048yxKQhpJ 8wro0zGATjlYyzi5XW2Q33GYu5nRMUi/SQmZu/XTmLr0/lrUarJ3Kjs+9obzJFwhgHfp 5lpg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-id:precedence:sender:mime-version:user-agent:references :message-id:in-reply-to:subject:cc:to:from:date; bh=VINd1N6XQdkBdHzdFJjx4vFzKBxWthzf5qjJI+DQwJE=; b=DyZwvTOyK8zfwEpolvmY8ePAJkqdWbazdEEhwhJCgzZzKRECdvSs8U+Ye1JTq0w2CJ AfRqUzBbJzM2IeUEG5ilm/KU/hiZ/JBk7mAd6v+3I/nOdFn89D37jVguhFwqsLyVtb6K giIlVGc9Qotw9z02Zlh9Gru7WdyQhPjdK3NlGgjT9v6CmAcIyXce/WxPmVCmu4eRqvad 4TS6ueH/8K2E5JZltI19vh2+gC7J6cTq8okxPyI7zgoOofa29ec425rx/3+5QGpWnMZV HysUMUygLy6ymnSs06/PUqFJ9841+9OREnd5b2pB7dd2C1NGjwp67lIwpyf7r3OtjV4v TmSw== ARC-Authentication-Results: i=1; mx.google.com; spf=pass (google.com: best guess record for domain of linux-kernel-owner@vger.kernel.org designates 209.132.180.67 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org Return-Path: Received: from vger.kernel.org (vger.kernel.org. [209.132.180.67]) by mx.google.com with ESMTP id c20si4032513otr.39.2020.03.28.06.43.31; Sat, 28 Mar 2020 06:43:45 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of linux-kernel-owner@vger.kernel.org designates 209.132.180.67 as permitted sender) client-ip=209.132.180.67; Authentication-Results: mx.google.com; spf=pass (google.com: best guess record for domain of linux-kernel-owner@vger.kernel.org designates 209.132.180.67 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1726380AbgC1NnA (ORCPT + 99 others); Sat, 28 Mar 2020 09:43:00 -0400 Received: from mail2-relais-roc.national.inria.fr ([192.134.164.83]:42773 "EHLO mail2-relais-roc.national.inria.fr" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1726290AbgC1NnA (ORCPT ); Sat, 28 Mar 2020 09:43:00 -0400 X-IronPort-AV: E=Sophos;i="5.72,316,1580770800"; d="scan'208";a="442756603" Received: from abo-173-121-68.mrs.modulonet.fr (HELO hadrien) ([85.68.121.173]) by mail2-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 28 Mar 2020 14:42:57 +0100 Date: Sat, 28 Mar 2020 14:42:56 +0100 (CET) From: Julia Lawall X-X-Sender: jll@hadrien To: Markus Elfring cc: Michel Lespinasse , Coccinelle , linux-mm@kvack.org, Davidlohr Bueso , Peter Zijlstra , Hugh Dickins , LKML , Liam Howlett , Jason Gunthorpe , Matthew Wilcox , Ying Han , David Rientjes , Andrew Morton , Laurent Dufour , Vlastimil Babka Subject: Re: [Cocci] [v3 05/10] mmap locking API: Checking the Coccinelle software In-Reply-To: <590dbec7-341a-3480-dd47-cb3c65b023c7@web.de> Message-ID: References: <20200327225102.25061-1-walken@google.com> <20200327225102.25061-6-walken@google.com> <3c222f3c-c8e2-660a-a348-5f3583e7e036@web.de> <590dbec7-341a-3480-dd47-cb3c65b023c7@web.de> User-Agent: Alpine 2.21 (DEB 202 2017-01-01) MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="8323329-169149080-1585402977=:3005" Sender: linux-kernel-owner@vger.kernel.org Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org This message is in MIME format. The first part should be readable text, while the remaining parts are likely unreadable without MIME-aware tools. --8323329-169149080-1585402977=:3005 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8BIT On Sat, 28 Mar 2020, Markus Elfring wrote: > >> How will corresponding software development resources evolve? > > > > I don't think I understand the question, or, actually, are you asking > > me or the coccinelle developers ? > > I hope that another communication approach can eventually increase > the chances for a better common understanding of development challenges. > > The code from a mentioned source file can be reduced to the following > test file. > https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/tree/arch/mips/mm/fault.c?id=69c5eea3128e775fd3c70ecf0098105d96dee330#n34 > > // deleted part > static void __kprobes __do_page_fault(struct pt_regs *regs, unsigned long write, > unsigned long address) > { > struct vm_area_struct * vma = NULL; > struct task_struct *tsk = current; > struct mm_struct *mm = tsk->mm; > // deleted part > retry: > down_read(&mm->mmap_sem); > vma = find_vma(mm, address); > if (!vma) > goto bad_area; > // deleted part > } > // deleted part > > > Application of the software “Coccinelle 1.0.8-00029-ga549b9f0” (OCaml 4.10.0) > > elfring@Sonne:~/Projekte/Coccinelle/Probe> spatch --parse-c do_page_fault-excerpt3.c > … > NB total files = 1; perfect = 1; pbs = 0; timeout = 0; =========> 100% > nb good = 15, nb passed = 1 =========> 6.25% passed > nb good = 15, nb bad = 0 =========> 100.00% good or passed > > > The discussed transformation approach can also be reduced for a test > to the following script for the semantic patch language. > > @replacement@ > expression x; > @@ > -down_read > +mmap_read_lock > ( > - & > x > - ->mmap_sem > ) > > > elfring@Sonne:~/Projekte/Coccinelle/Probe> spatch use_mmap_locking_API_3.cocci do_page_fault-excerpt3.c > > > The desired diff is not generated so far. > How would you like to fix this situation? Who exactly do you think "you" is? I will look at it, but it is not very polite to ask a user of Coccinelle such a question. julia > > Regards, > Markus > _______________________________________________ > Cocci mailing list > Cocci@systeme.lip6.fr > https://systeme.lip6.fr/mailman/listinfo/cocci > --8323329-169149080-1585402977=:3005--