From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (qmail 98177 invoked by alias); 2 Apr 2019 08:11:51 -0000 Mailing-List: contact gcc-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Archive: List-Post: List-Help: Sender: gcc-owner@gcc.gnu.org Received: (qmail 98165 invoked by uid 89); 2 Apr 2019 08:11:51 -0000 Authentication-Results: sourceware.org; auth=none X-Spam-SWARE-Status: No, score=-0.8 required=5.0 tests=AWL,BAYES_00,FREEMAIL_FROM,RCVD_IN_DNSWL_NONE,SPF_PASS autolearn=ham version=3.3.1 spammy=presented, HX-Received:Tue, HX-Google-DKIM-Signature:sender, dear X-HELO: mail-wr1-f52.google.com Received: from mail-wr1-f52.google.com (HELO mail-wr1-f52.google.com) (209.85.221.52) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with ESMTP; Tue, 02 Apr 2019 08:11:49 +0000 Received: by mail-wr1-f52.google.com with SMTP id q1so15377348wrp.0 for ; Tue, 02 Apr 2019 01:11:49 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlemail.com; s=20161025; h=mime-version:reply-to:sender:from:date:message-id:subject:to:cc; bh=a6GMfHe9BAJ3hrwEXaSP0ybXReg2EvPnP2SSseVLQ6Y=; b=DTyDFNZsUw3CGxm6dHDBgIt11/wQpVkBiRS4QqAhTvcVYIKjmrhnJrpDMBq46LZ/VX Jzrmnz4fGpjjK/GHBwLCh4/8+rmSVHDIfqCX8UK+chFfwXjmBfOCPcLPYmeP8sWQ0HrI 3wrHSq5IZ3sml8+CM0tSMZdTwDYRv2X4ahvYIyy7g54da1eB4Q28IbgkCUgQMn5bQhct +XkGFTs3ah47t4478jUfL2hCRtPqkVOcn/f+YzhxCmBfbQSH03oSH9hgRwTZwIvmC4GY f2Bfe6NrXaRGc8IPPG4EILBLwpdsdHDxuGjZ31lnd9lZ9qI+M9l28X1+Y89xPkJjW5IW g9rQ== MIME-Version: 1.0 Reply-To: Peter.Sewell@cl.cam.ac.uk Sender: p.m.sewell@googlemail.com Received: by 2002:a7b:c086:0:0:0:0:0 with HTTP; Tue, 2 Apr 2019 01:11:46 -0700 (PDT) From: Peter Sewell Date: Tue, 02 Apr 2019 08:11:00 -0000 Message-ID: Subject: C provenance semantics proposal To: gcc@gcc.gnu.org Cc: cl-c-memory-object-model Content-Type: text/plain; charset="UTF-8" X-SW-Source: 2019-04/txt/msg00022.txt.bz2 Dear all, continuing the discussion from the 2018 GNU Tools Cauldron, we (the WG14 C memory object model study group) now have a detailed proposal for pointer provenance semantics, refining the "provenance not via integers (PNVI)" model presented there. This will be discussed at the ISO WG14 C standards committee at the end of April, and comments from the GCC community before then would be very welcome. The proposal reconciles the needs of existing code and the behaviour of existing compilers as well as we can, but it doesn't exactly match any of the latter, so we'd especially like to know whether it would be feasible to implement - our hope is that it would only require minor changes. It's presented in three documents: N2362 Moving to a provenance-aware memory model for C: proposal for C2x by the memory object model study group. Jens Gustedt, Peter Sewell, Kayvan Memarian, Victor B. F. Gomes, Martin Uecker. This introduces the proposal and gives the proposed change to the standard text, presented as change-highlighted pages of the standard (though one might want to read the N2363 examples before going into that). http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2362.pdf N2363 C provenance semantics: examples. Peter Sewell, Kayvan Memarian, Victor B. F. Gomes, Jens Gustedt, Martin Uecker. This explains the proposal and its design choices with discussion of a series of examples. http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2363.pdf N2364 C provenance semantics: detailed semantics. Peter Sewell, Kayvan Memarian, Victor B. F. Gomes. This gives a detailed mathematical semantics for the proposal http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2364.pdf In addition, at http://cerberus.cl.cam.ac.uk/cerberus we provide an executable version of the semantics, with a web interface that allows one to explore and visualise the behaviour of small test programs, stepping through and seeing the abstract-machine memory state including provenance information. N2363 compares the results of this for the example programs with gcc, clang, and icc results, though the tests are really intended as tests of the semantics rather than compiler tests, so one has to interpret this with care. best, Peter (for the study group)