Stream: git-wasmtime

Topic: wasmtime / PR #3561 Update aarch64 backend's ISLE code to...


view this post on Zulip Wasmtime GitHub notifications bot (Nov 24 2021 at 18:55):

cfallin requested alexcrichton for a review on PR #3561.

view this post on Zulip Wasmtime GitHub notifications bot (Nov 24 2021 at 18:55):

cfallin opened PR #3561 from aarch64-isle-rule-explicit-ordering to main:

In this comment I noted a potential subtle issue with the way that a few rules were written that is fine now but could cause some unexpected pain when we get around to verification.

Specifically, a set of rules of the form

    (rule (A (B _)) (C))
    (rule (A _) (D))

should, under any reasonable "default" rule ordering scheme, fire the more specific rule (A (B _)) when applicable, in preference to the second "fallback" rule.

However, for future verification-specific applications of ISLE, we want to ensure the property that a rule's meaning/validity is not dependent on being overridden by more specific rules. In other words, if a rule specifies a rewrite, that rewrite should always be correct; and choosing a more specific rule can give a better compilation (better generated code) but should not be necessary for correctness.

This is an admittedly under-document part of the language, though in the pending #3560 I added a note about rule ordering being a heuristic that should hopefully make this slightly clearer. Ultimately I want to have tests that choose non-default rule orderings and differentially fuzz in order to be sure that we're following this principle; and of course once we're actually doing verification, we'll catch issues like this upfront.

Apologies for the subtle footgun here and hopefully the reasoning is clear enough :-)

<!--

Please ensure that the following steps are all taken care of before submitting
the PR.

Please ensure all communication adheres to the code of conduct.
-->

view this post on Zulip Wasmtime GitHub notifications bot (Nov 24 2021 at 18:57):

cfallin edited PR #3561 from aarch64-isle-rule-explicit-ordering to main:

In this comment I noted a potential subtle issue with the way that a few rules were written that is fine now but could cause some unexpected pain when we get around to verification.

Specifically, a set of rules of the form

    (rule (A (B _)) (C))
    (rule (A _) (D))

should, under any reasonable "default" rule ordering scheme, fire the more specific rule (A (B _)) when applicable, in preference to the second "fallback" rule.

However, for future verification-specific applications of ISLE, we want to ensure the property that a rule's meaning/validity is not dependent on being overridden by more specific rules. In other words, if a rule specifies a rewrite, that rewrite should always be correct; and choosing a more specific rule can give a better compilation (better generated code) but should not be necessary for correctness.

This is an admittedly under-documented part of the language, though in the pending #3560 I added a note about rule ordering being a heuristic that should hopefully make this slightly clearer. Ultimately I want to have tests that choose non-default rule orderings and differentially fuzz in order to be sure that we're following this principle; and of course once we're actually doing verification, we'll catch issues like this upfront.

Apologies for the subtle footgun here and hopefully the reasoning is clear enough :-)

<!--

Please ensure that the following steps are all taken care of before submitting
the PR.

Please ensure all communication adheres to the code of conduct.
-->

view this post on Zulip Wasmtime GitHub notifications bot (Nov 24 2021 at 19:09):

cfallin updated PR #3561 from aarch64-isle-rule-explicit-ordering to main.

view this post on Zulip Wasmtime GitHub notifications bot (Nov 24 2021 at 19:17):

alexcrichton submitted PR review.

view this post on Zulip Wasmtime GitHub notifications bot (Nov 24 2021 at 19:57):

cfallin merged PR #3561.


Last updated: Dec 23 2024 at 13:07 UTC