[ASL] Semantics of throw statement

[maranget]

Hi @HadrienRenaud. the semantics of throw looks too eager in the concurrent case. Consider the following test:

ASL U

{}

type  Coucou of exception {};

func f(x:integer) => integer
begin
  if x == 0 then
    throw Coucou {  };  
  end
  return x;
end

func main() => integer
begin
  try
    let z = f(0);
    print(z);
  catch
    when Coucou =>
      print(1010);
  end
  return 0;
end

Executing the above test with herd7 U.litmus results in printing 1010 twice.

Even more serious we have a fatal error when the exception has an argument:

ASL T

{}

type  Coucou of exception {z:integer};

func f(x:integer) => integer
begin
  if x == 0 then
    throw Coucou { z=x };  
  end
  return x;
end

func main() => integer
begin
  try
    let z = f(0);
    print(z);
  catch
    when e:Coucou =>
      print (e.z);
  end
  return 0;
end

Running the test results in a fatal error:

% herd7 T.litmus
0
0
Contradiction on reg 0:thrown-1: loaded {z:0,} vs. stored 0

Fatal: File "T.litmus" Adios
Fatal error: exception File "herd/mem.ml", line 837, characters 16-22: Assertion failed

[maranget]

Thinking twice, it is normal for the print statement to be executed twice. However, the fatal error is an actual bug.

[maranget]

Here is a simpler example:

ASL U

{ }

type  Coucou of exception {};

func f(a:integer) => integer
begin
  let b = SomeBoolean();
  if b then
    throw Coucou { };  
  end
  return a;
end

func main() => integer
begin
  let x=0;
  try
    let z = f(x);
    print(z);
  catch
    when Coucou =>
      assert TRUE;
  end
  return 0;
end

Running the test above, we have:

% herd7 U.litmus
0
0
Warning: Uncaught exception: Coucou {}