Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use non-deterministic precision for float operations that do not have guaranteed precision #3555

Open
RalfJung opened this issue May 4, 2024 · 6 comments · May be fixed by #4156
Open

Use non-deterministic precision for float operations that do not have guaranteed precision #3555

RalfJung opened this issue May 4, 2024 · 6 comments · May be fixed by #4156
Assignees
Labels
A-shims Area: This affects the external function shims C-enhancement Category: a PR with an enhancement or an issue tracking an accepted enhancement E-good-first-issue A good way to start contributing, mentoring is available

Comments

@RalfJung
Copy link
Member

RalfJung commented May 4, 2024

As per rust-lang/rust#124609, these operations behave non-deterministically, so we should implement that in Miri. The apply_random_float_error function (currently only used for x86 intrinsics) could be used to do that.

@RalfJung RalfJung added C-enhancement Category: a PR with an enhancement or an issue tracking an accepted enhancement A-shims Area: This affects the external function shims E-good-first-issue A good way to start contributing, mentoring is available labels May 4, 2024
@RalfJung
Copy link
Member Author

This should also be used for fast-math and "algebraic" float operations.

@LorrensP-2158466
Copy link

Hi, i would like to try this. I have 2 questions though. Do you mean that we should add the float_error to this part of the code?

https://github.com/rust-lang/miri/blob/95558badc942353582b742b30950412d46d69a06/src/intrinsics/mod.rs#L247C1-L263C18

And should we use the same magnitude as the x86 instrinics?

// Apply a relative error with a magnitude on the order of 2^-12 to simulate the

@RalfJung
Copy link
Member Author

Yes, all of those there except for sqrt should apply a float error.

There's no fixed value for the magnitude of the error so we might as well pick the same as the x86 intrinsic.

@LorrensP-2158466
Copy link

@rustbot claim

@LorrensP-2158466
Copy link

Hi, I think I successfully implemented it for all but 2 match arms because I don't know how to do it nicely. It is about the f*_algebraic operations:

  | "fadd_algebraic"
  | "fsub_algebraic"
  | "fmul_algebraic"
  | "fdiv_algebraic"
  | "frem_algebraic"
  => {
      let [a, b] = check_arg_count(args)?;
      let a = this.read_immediate(a)?;
      let b = this.read_immediate(b)?;
      let op = match intrinsic_name {
          "fadd_algebraic" => mir::BinOp::Add,
          "fsub_algebraic" => mir::BinOp::Sub,
          "fmul_algebraic" => mir::BinOp::Mul,
          "fdiv_algebraic" => mir::BinOp::Div,
          "frem_algebraic" => mir::BinOp::Rem,
          _ => bug!(),
      };
      let res = this.binary_op(op, &a, &b)?;
      // `binary_op` already called `generate_nan` if necessary.
      this.write_immediate(*res, dest)?;
  }

I don't know how I can nicely implement this.
I thought about converting to a scalar int to_scalar_int() and then matching on the float type converting to that type, applying the error, and then writing the scalar. But maybe there is a better way?

And the f*_fast operation. It says this in the code:
https://github.com/rust-lang/miri/blob/c2a376121b7756c73b250bdba82f92d8a47c25a4/src/intrinsics/mod.rs#L424C1-L426C51

Should I follow the second comment from RalfJung or this comment in the code?

Also, is this the conventional way of asking for help? Or is Zullip used more? Or another way?

Thanks for the help!

@RalfJung
Copy link
Member Author

I don't think I quite understand what the problem is. I would propose you open a PR that implements this for one or two (blocks of) shims, so that we can give feedback on a concrete implementation, and hopefully that will help clarify these things as well.

Regarding asking for help, Zulip is a good place for that. :)

Should I follow the second comment from RalfJung or this comment in the code?

Note that this refers to different non-determinism than what the issue is about. That comment is about making the NaN payload bits and sign non-deterministic.

@LorrensP-2158466 LorrensP-2158466 linked a pull request Jan 27, 2025 that will close this issue
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-shims Area: This affects the external function shims C-enhancement Category: a PR with an enhancement or an issue tracking an accepted enhancement E-good-first-issue A good way to start contributing, mentoring is available
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants