Return-Path: Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1754935AbcKUQK5 (ORCPT ); Mon, 21 Nov 2016 11:10:57 -0500 Received: from mx2.suse.de ([195.135.220.15]:57268 "EHLO mx2.suse.de" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1753056AbcKUQKz (ORCPT ); Mon, 21 Nov 2016 11:10:55 -0500 Date: Mon, 21 Nov 2016 17:10:33 +0100 From: Cyril Hrubis To: Dmitry Vyukov Cc: linux-api@vger.kernel.org, LKML , Michael Kerrisk-manpages , Thomas Gleixner , Sasha Levin , Mathieu Desnoyers , scientist@fb.com, Steven Rostedt , Arnd Bergmann , carlos@redhat.com, syzkaller , Kostya Serebryany , Mike Frysinger , Dave Jones , Tavis Ormandy Subject: Re: Formal description of system call interface Message-ID: <20161121161032.GB27353@rei.lan> References: <20161107103819.GA11374@rei.lan> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.24 (2015-08-30) Sender: linux-kernel-owner@vger.kernel.org List-ID: X-Mailing-List: linux-kernel@vger.kernel.org Content-Length: 885 Lines: 23 Hi! > Description of "returns fd or this set of errors" looks simple and useful. > Any test system or fuzzer will be able to verify that kernel actually returns > claimed return values. Also Carlos expressed interested in errno values > in the context of glibc. > I would do it from day one. > > Re more complex side effects. I always feared that a description suitable > for automatic verification (i.e. zero false positives, otherwise it is useless) > may be too difficult to achieve. I'm afraid it may be as well. I would expect that we will end up with something quite complex with a large set of exceptions from the rules. > Cyril, Tavis, can you come up with some set of predicates that can be > checked automatically yet still useful? > We can start small, e.g. "must not alter virtual address space". I will try to thing about this a bit. -- Cyril Hrubis chrubis@suse.cz