clarify the stance on optimisations that change "exceptional behaviour"

[mraleph]

This request is motivated by an optimisation CL submitted by an external contributor. This optimisation attempts to strengthen array bounds checks with constant indices so that a dominating check makes subsequent checks redundant, so that for example in the code:

  static bool isIdentity(Matrix4 a) {
    assert(a != null);
    return a.storage[0] == 1.0 // col 1
        && a.storage[1] == 0.0
        && a.storage[2] == 0.0
        && a.storage[3] == 0.0
        && a.storage[4] == 0.0 // col 2
        && a.storage[5] == 1.0
        && a.storage[6] == 0.0
        && a.storage[7] == 0.0
        && a.storage[8] == 0.0 // col 3
        && a.storage[9] == 0.0
        && a.storage[10] == 1.0
        && a.storage[11] == 0.0
        && a.storage[12] == 0.0 // col 4
        && a.storage[13] == 0.0
        && a.storage[14] == 0.0
        && a.storage[15] == 1.0;
  }

There would be a single bounds check checking that a.storage has at least 16 elements.

As I was reviewing this CL I realised that this optimization is not semantics preserving because bounds checks throw RangeError which contains a lot of information about the failed check (failed index as well as bounds). This information is available both via toString as well as getters on the RangeError class - which makes this optimisation observable.

int badIndex(List a) {
  try {
    a[0];
    a[1];
  } on RangeError catch (e) {
    return e.invalidValue;
  }
}

bool checksReordered() => badIndex([]) != 0;

So far we have been largely avoiding adding optimisations that can alter observable behaviour to the Dart VM (the only exceptions I know about are obfuscation and dwarf stack traces - which are observable through StackTrace.toString but fortunately public documentation for StackTrace.toString gives us some leeway for doing so ("The exact format of the string representation is not final.")

That is why I would like to have some discussions with the language around semantic preservation around exceptional cases like the one above - so that we have framework for evaluating optimisations like this one.

I also think this might be a good opportunity to put a formal language framework around dart2js optimization levels which are not as semantic preserving as Dart VM. (/cc @sigmundch)

/cc @lrhn @leafpetersen @eernstg

[sigmundch]

I also think this might be a good opportunity to put a formal language framework around dart2js optimization levels which are not as semantic preserving as Dart VM

Sounds great. For reference, here is a description of the dart2js non-semantic preserving optimizations: https://github.com/dart-lang/sdk/blob/207b68d5b47d8b966b084a662a0b4eadff64ac24/pkg/compiler/lib/src/dart2js.dart#L948, similar to your example, they only deviate if the original program was not error free.

[eernstg]

I think it's fair to say that the optimization here is not observable according to the language, because the language has no notion of RangeErrors, it only says

It is a dynamic error to attempt to access a list using an index that is not a member of its set of indices.

So we could say that it is not a language question, simply because the language doesn't consider any dynamic error inappropriate for an index-out-of-range event, so the program still behaves as specified.

But if we insist that the difference is observable (say, from a core lib perspective), the tricky part is that it is difficult to place the responsibility: It isn't actually an implementation choice made by the class whose code throws the RangeError.

But it seems likely to me that there are some much more observable consequences of this optimization: How do we know that evaluation of a.storage[0] == 1.0 and so on has no side effects?

So what we'd need is (perhaps) a developer controlled opt-in mechanism (like a command line option) which enables a specific optimization, and leaves it up to the developer to decide that this optimization performs an acceptable transformation of this program.

[leafpetersen]

I'm not sure I agree that this is not observable from a language standpoint - the compiler is in some sense providing an implicit implementation of a piece of Dart code that looks something like "throw RangeError(....)" which does have specified semantics, but I'm not too hung up on it either. @mraleph are you thinking of something along narrow lines (e.g. just saying that certain things about RangeErrors are not observable) or broader (e.g. saying that the compiler is free to re-order or combine the exceptions that it generates in certain ways that are only observable in certain delimited ways)?

[rakudrama]

For this specific case the developer can 'opt-in' to the optimization relatively trivially by writing a line of code.

I have considered taking a pass over the vector_math library to add 'bounds assertions' of the form a[15];.

static bool isIdentity(Matrix4 a) {
  assert(a != null);
  a[15];
  return a.storage[0] == 1.0 // col 1
      && a.storage[1] == 0.0
      && a.storage[2] == 0.0
      ...
}

I never got around to it but I would be happy to review pull requests of this nature.

[mraleph]

I'm not sure I agree that this is not observable from a language standpoint.

I strongly believe that if I can write a valid Dart program that changes its output depending on optimisation flags then optimisation is observable from the language standpoint - unless language adds additional provisions which permit specific changes in behaviour.

@mraleph are you thinking of something along narrow lines

I just want to have some clarity on our general position - so far Dart VM and dart2js represent two parts of the spectrum:

• Dart VM optimisations never change behaviour of the program (with exception of StackTrace.toString contents - but those are considered opaque for all intents and purposes).
• dart2js optimisations can change behaviour of the program.

In some sense dart2js is the production compiler that forgoes specification compliance for the sake of performance and code size.

I guess my question is: should we change the specification in such a way that makes dart2js a compliant compiler simultaneously permitting VM to perform similar kind of optimisations? Do we want that?

I don't feel strongly one way or another - fwiw I appreciate Dart VM compliance because it makes it easier to reason about the semantics of any given program and programs behave the same way in all execution modes. So resolving this issue with a statement that we want all our compilers to be compliant with exception of dart2js which just exists in a special place is fine by me as well.

[eernstg]

@rakudrama wrote:

add 'bounds assertions' of the form a[15];.

That would certainly be a helpful program change (I'm assuming that it's added by a developer, not by the optimization), because we could then hope to have a situation where there is no reordering of effects, and it's simply known that a bunch of range checks are guaranteed to succeed (so they can be eliminated). However, as I mentioned, I can't see how these optimizations could be safe in the first place:

How would it be known by the compiler that there is any connection between evaluating a[_] and evaluating a.storage[_], and why does the compiler know that the evaluation of a.storage[_] doesn't have any side effects?

Do we have extra knowledge, like: the dynamic type of a is exactly Matrix4, and the compiler can know the implementation of each method of a because Matrix4 is declared in a system library? Given that it seems to live at https://github.com/google/vector_math.dart/blob/master/lib/src/vector_math/matrix4.dart, it doesn't look like there are many special guarantees for Matrix4 that a compiler would know about.

If we don't have that then I can't see how we'd guarantee that we do not encounter an implementation of Matrix4 whose storage getter returns a different Float32List from time to time, such that we can't assume that it has a length which is guaranteed to be at least 16.

@mraleph wrote:

should we change the specification in such a way that makes dart2js a compliant compiler

Maybe we can avoid adding new properties to dart2js where it optimizes in ways that observably change the behavior of the program. A developer-written check like a[15]; might be sufficient for a lot of cases. We could then tell developers that they can do this, and it would be really nice if we could avoid optimizations-that-change-the-semantics whenever possible.

[lrhn]

I strongly believe that if I can write a valid Dart program that changes its output depending on optimisation flags then optimisation is observable from the language standpoint - unless language adds additional provisions which permit specific changes in behaviour.

If the language semantics allow both behaviors, then it's underspecified. That's OK in some cases, but not something we actively aim for.

If not, then this thing is not an "optimization", it's a bug in the compiler.

Dart2js have some deliberate performance enhancing bugs. That doesn't make it valid Dart behavior, just something they are getting away with in the name of performance. That's my personal position. I think they should fix their bugs and not just ignore parts of the language because it's inconvenient. It's not the frog compiler.

[rakudrama]

@eernstg wrote:

Do we have extra knowledge

dart2js is a whole-program compiler, so in the usual case when there are no classes extending or implementing Matrix4, it can tell there are no effects.

dart2js can't tell the length is always 16 if this constructor is used, which unfortunately usually happens. Some code (example, example) have already been written to index 15 first.

[eernstg]

@rakudrama wrote:

dart2js is a whole-program compiler ... can tell there are no effects.

Right, and the optimization CL that was mentioned initially in this issue was on the vm, but the world is may be similarly closed there as well.

But then, assuming that we have whatever extra knowledge is needed, we still have two approaches: Allow some optimizations (@lrhn would say bugs) that do not preserve the observable behavior of programs, or require every optimization to be unobservable.

@lrhn wrote:

If the language semantics allow both behaviors, then it's underspecified.

I think that's a bit unrealistic, and I actually do not think it's a goal to specify the behavior of programs fully. For instance, we probably won't specify precisely whether and when an out-of-memory error will occur, nor exactly how many clock cycles it will take to run a specific program with a specific input, and we explicitly specify that a few things are implementation specific. So "specified behavior" will be a range in the semantic space, not a single point.

So perhaps the real question is whether the differences in behavior is within the boundary of specified behavior or not, rather than whether it's observably identical with and without any given optimization.

But I'd still prefer that we ask developers to add a[15] in front of a loop, or to reorder operations on indices such that the first one has a range check that implies success for a number of subsequent range checks, rather than having the compiler look into a set of range checks that are known to occur in the future and hoisting one of them up in front of the others. The former is much more cleanly unobservable, and that is definitely a useful property of an optimization.