GNATのrequeue-with-abortはバグってるんじゃないかと言う説

この前遊んでいたら見つけてしまったrequeue-with-abortの挙動がおかしい件をYTさんに聞いてみたところ、やはりどうもバグのような雰囲気なので、アドバイスに従ってcomp.lang.adaに投げてみた。

問題のコードはこちら。

with Ada.Text_IO; use Ada.Text_IO;

procedure Req is
   task T is
      entry Original_Call;
      entry Requeued_Call;
   end T;

   task body T is
   begin
      loop
      accept Original_Call do
         Put_Line ("Original Call...");
         -- takes three seconds
         delay 3.0;
         Put_Line ("Original Call Done");
         requeue Requeued_Call with abort;
      end Original_Call;

      -- inifinity loop
      loop
         delay 10.0;
      end loop;

      -- will be never accepted
      accept Requeued_Call do
         Put_Line ("Requeued_Call");
      end Requeued_Call;
      end loop;
   end T;

begin
   select
      T.Original_Call;
   or
      -- just wait 1 second
      delay 1.0;
      Put_Line ("Aborting");
   end select;
   Put_Line ("Parent Done");
end Req;

with abort付のrequeueならば、呼び出し元の制限時間がリキューされた呼び出しに対しても有効になるはずである。実際、上のコードでdelay 3.0の部分が無ければ、1秒以内にacceptされないRequeued_Callはキャンセルされる。

しかし、なぜか最初に呼び出したエントリの実行中に制限時間を超えてしまうと、キューに並んだままいつまで経ってもキャンセルされなくなってしまう。上の例だと、親がdelay 1.0で1秒後まで待つのに対して、Original_Callは即座にacceptされるため、この時点ではキャンセルは行われない(これ自体は問題ない)。しかし、Original_Callの実行には3秒かかかり、この段階で呼び出し元の制限時間に到達する。つまり、requeueに到達した時点で既に制限時間を過ぎている。そして、リキューされたRequeued_Callは、その後の無限ループでタスクが止まるため一生acceptされず、呼び出しはキューにとどまることになる。本来ならば、キューにとどまったままacceptされなければ、大元のtimedな呼び出しに基づいてキャンセルが発生するべきだと思われるのだが、GNATの実装ではそれが行われない。

RMを読む範囲では、この動作の根拠となる仕様は見つからない。がしかし、制御構造の基礎に近い部分にこのようなバグが残っているとは中々思えないので、どうにもこうにも判断が難しい。バグに見えるが、もしかしたら何か理由があってこのような動作なのかもしれない。

2日ぐらい経って現在17messagesで、「どうもバグっぽいけれど、language lawyerに聞いてみないとなんとも」という雰囲気になっている。

私の説明が下手だったために、問題を勘違いさせてしまった人が居たのが心苦しい。

とりあえず、言われた通りにAda-Commentsに投げてみて、公式見解を伺ってみようと思う。