unofficial mirror of bug-gnu-emacs@gnu.org 
 help / color / mirror / code / Atom feed
From: Andrea Corallo via "Bug reports for GNU Emacs, the Swiss army knife of text editors" <bug-gnu-emacs@gnu.org>
To: Pip Cet <pipcet@gmail.com>
Cc: 46847@debbugs.gnu.org
Subject: bug#46847: 28.0.50; [native-comp] assume pseudo-insns should be verified
Date: Mon, 01 Mar 2021 20:12:15 +0000	[thread overview]
Message-ID: <xjf7dmqbpls.fsf@sdf.org> (raw)
In-Reply-To: <CAOqdjBc+ch3KY0ChrLBR3vWyS4eXQgUQQKHzeQRwMv18aFER9A@mail.gmail.com> (Pip Cet's message of "Mon, 1 Mar 2021 13:06:31 +0000")

Pip Cet <pipcet@gmail.com> writes:

> This is a wishlist item for the native-comp branch, though I consider
> the feature in question to be so essential that its absence also
> qualifies as a bug.
>
> The native-comp branch is emitting assume pseudo-insns. Those come in
> various forms, but their interpretation is clear: they express
> conditions which are meant to hold at runtime, and which the compiler
> may use to optimize code.
>
> I would like to add an optional compiler pass which asserts that the
> conditions are actually true at runtime. This is a basic safeguard
> that any assume() mechanism should have, and it's perfectly equivalent
> to the way eassume() becomes eassert() in debug builds of Emacs.
>
> Unfortunately, it turns out that while adding the compiler pass is
> easy, there are many failures because the assume pseudo-insns emitted
> at present are inconsistent or plain wrong. Some of these wrong
> assumes result in reproducible Lisp-to-native-code bugs today; others
> will not; for still others, we're not sure.

I think the issue might be that how assumes works has been
miss-understood here.

Assumes are working after SSA rename in the world of mvar ids, in
contrast we render code based on slot numbers.  Rendering assertions
based on assumes using the slot numbers (IIUC that's what your patch
did) certainly leads to inconsistencies, but that's a fundamental
miss-interpretation of how assumes are working.  This is probably also
why you often suggests assumes are inconsistent.

Anyway, for the reasons above rendering 1:1 assumes into run-time checks
is not easily possible.

OTOH a possible way, and that's what I want to do, would be to verify
just before each (non pseudo) insn actually rendered that the slots in
use there are consistent with the prediction.

One could even control that with a parameter and have a mode where we
just inject asserts on return insns not to bloat excessively the code.

Note: I'm not aware of any compiler emitting run-time checks to verify
its compile time predictions by why not.

I'll take this task as sounds like good verification/development cost
trade-off to me.  Will follow-up on this!

Thanks

  Andrea





  reply	other threads:[~2021-03-01 20:12 UTC|newest]

Thread overview: 11+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2021-03-01 13:06 bug#46847: 28.0.50; [native-comp] assume pseudo-insns should be verified Pip Cet
2021-03-01 20:12 ` Andrea Corallo via Bug reports for GNU Emacs, the Swiss army knife of text editors [this message]
2021-03-02  6:57   ` Pip Cet
2021-03-05 11:16     ` Andrea Corallo via Bug reports for GNU Emacs, the Swiss army knife of text editors
2021-03-05 16:09 ` Pip Cet
2021-03-05 19:36   ` Andrea Corallo via Bug reports for GNU Emacs, the Swiss army knife of text editors
2021-03-14 21:07   ` Andrea Corallo via Bug reports for GNU Emacs, the Swiss army knife of text editors
2024-03-20  9:30     ` Andrea Corallo
2024-03-20 13:05       ` Eli Zaretskii
2024-03-20 13:58         ` Andrea Corallo
2024-03-20 14:09           ` Eli Zaretskii

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

  List information: https://www.gnu.org/software/emacs/

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=xjf7dmqbpls.fsf@sdf.org \
    --to=bug-gnu-emacs@gnu.org \
    --cc=46847@debbugs.gnu.org \
    --cc=akrl@sdf.org \
    --cc=pipcet@gmail.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
Code repositories for project(s) associated with this public inbox

	https://git.savannah.gnu.org/cgit/emacs.git

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).