Ada 202x (19日目) - Globalその1
===============================

.. post:: Dec 19, 2019
   :tags: ada, ada_2022

.. role:: strike

続き。

これまでのあらすじ
------------------

Ada 202xでは複数のスレッドが同期なしで同じ変数にアクセスしていないことを検証できます。
具体的には各変数ごとに読み取り(in)と書き込み(out)のアクセスが衝突しているかがチェックされます。

さて、コンパイラが自動でチェックするにも限りがあります。
具体的には翻訳単位や可視性の壁があります。
これらの壁を越えるためにはパッケージの内側で何にアクセスしているかを外に向けて示す必要があります。

グローバル変数アクセスの表明
----------------------------

Globalアスペクト(グローバル変数)
++++++++++++++++++++++++++++++++

``Global`` アスペクトを通じてサブプログラムがアクセスしているグローバル変数を表明することができます。

.. code-block:: ada

 package Pkg1 is
    G : Integer;
    function Get_G return Integer
      with Global => in G;
    procedure Set_G (Value : in Integer)
      with Global => out G;
    procedure Incr_G
      with Global => in out G;
    procedure Unrelated
      with Global => null;
 end Pkg1;

.. code-block:: ada

 package body Pkg1 is
    
    function Get_G return Integer is
    begin
       return G; -- in
    end Get_G;
    
    procedure Set_G (Value : in Integer) is
    begin
       G := Value; -- out
    end Set_G;
    
    procedure Incr_G is
    begin
       G := G + 1; -- in out
    end Incr_G;
    
    procedure Unrelated is
    begin
      null;
    end Unrelated;
    
 end Pkg1;

割と特殊な文法です。

``null`` はグローバル変数にアクセスしていないということです。
``all`` と書きますと全てのグローバル変数にアクセスしていると見做されます。
どのグローバル変数にアクセスしているかがわからない場合が ``all`` ですね。

``Global`` を指定しないときのデフォルトは、``Pure`` なパッケージでは ``Global => null``、それ以外では ``Global => in out all`` となります。

一般にグローバル変数にアクセスしていない関数をリエントラント(再入可能)と呼び他のスレッドのことを気にせず使える性質とされています。
``Global`` アスペクトでは、リエントラントではないがこれとこれは同時に使っても大丈夫、みたいなことも表現できるわけですね。

それでは ``G`` を外からは見えない場所へ移動してみましょう。

.. code-block:: ada

 package Pkg1 is
    function Get_G return Integer
      with Global => in Pkg1;
    procedure Set_G (Value : in Integer)
      with Global => out Pkg1;
    procedure Incr_G
      with Global => in out Pkg1;
    procedure Unrelated
      with Global => null;
 private
    G : Integer;
 end Pkg1;

.. container:: strike

 ``Global => private of Pkg1`` で ``Pkg1`` にある隠されたグローバル変数にアクセスしているという意味です。

``Global => Pkg1`` で ``Pkg1`` にある全てのグローバル変数にアクセスしているという意味です。

なおこの ``Global`` アスペクトはSPARKでも使用されており全体を通じての整合性が検証されます。
そちらでは仮想のグローバル変数(状態)を宣言できたり状態間の関係を示せたりとより細かく制御できるよう拡張がなされています。

Ada 202xの範囲ではSPARKほど細かいことはできませんので、グローバル変数ではないがアクセスが競合していないかチェックしたいもの、例えばリンクするライブラリの内部状態やOSやCPUの持っている状態等はいずれかのパッケージに代表させればよいと思います。
細かく分けたいならそのための空パッケージを作ったりもありでしょうか。

スレッド間での衝突検証では同期なしにアクセスしている場合と同期を行ってアクセスしている場合を区別する必要があります。
きちんと同期を行っている場合は複数スレッドからアクセスされても問題ありませんが、同期なしにアクセスしているスレッドが混じると危険です。

同期を行っている場合は\ :strike:`変数名の前に` ``synchronized`` を書きます。
(また予約語を再利用している……。)

.. code-block:: ada

 package Pkg2 is
    S : Integer;
    procedure Sync_Incr_S
      with Global => in out synchronized;
 end Pkg2;

.. code-block:: ada

 package body Pkg2 is
    
    protected Prot is
       procedure Incr_S;
    end Prot;
    
    protected body Prot is
       
       procedure Incr_S is
       begin
          S := S + 1; -- in out
       end Incr_S;
       
    end Prot;
    
    procedure Sync_Incr_S is
    begin
       Prot.Incr_S;
    end Sync_Incr_S;
    
 end Pkg2;

グローバル変数が複数ある場合は括弧で囲いaggregate式のように書きます。

.. code-block:: ada

 package Pkg2 is
    X, Y : Integer;
    procedure Set_X_As_Y
      with Global => (out X, in Y);
 end Pkg2;

.. code-block:: ada

 package body Pkg2 is
    
    procedure Set_X_As_Y is
    begin
       X := Y;
    end Set_X_As_Y;
    
 end Pkg2;

``Nonblocking`` 同様に ``generic`` の引数として渡されたサブプログラムの ``Global`` を参照できます。

.. code-block:: ada

 generic
    with function F (X : Integer) return Integer;
 function G return Integer
   with
     Nonblocking => F'Nonblocking,
     Global      => F'Global;

 function G return Integer is
 begin
    return F (0);
 end G;

複数まとめるときは ``&`` 演算子を使います。
(配列を真似ていると思われます。
ただし ``[`` ``]`` は使えません……。)

.. code-block:: ada

 generic
    with function F1 (X : Integer) return Integer;
    with function F2 (X : Integer) return Integer;
 function G return Integer
   with
     Nonblocking => F1'Nonblocking and F2'Nonblocking,
     Global      => F1'Global & F2'Global;

 function G return Integer is
 begin
    return F1 (F2 (0));
 end G;

.. container:: inserted

 genericの引数との論理積は常に取られるようになりましたので、このようにわざわざ書く必要はなくなりました。

長くなりましたので今日はこの辺にして残りは後日とさせてください。
(例によって小出し。)

関連AI
------

- `AI12-0302-1`_ **Default Global aspect for language-defined units**

.. container:: strike

 - `AI12-0079-1`_ **Global-in and global-out annotations**
 - `AI12-0303-1`_ **Some constants must be covered by Global aspects; extensibility**
 - `AI12-0310-1`_ **Specifying private parts of packages in aspect Global**

所感
----

``Nonblocking`` と並んで標準ライブラリの定義のほとんどに ``with Global`` が付きまくってノイズです。

.. _`AI12-0079-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0079-1.txt
.. _`AI12-0302-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0302-1.txt
.. _`AI12-0303-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0303-1.txt
.. _`AI12-0310-1`: http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0310-1.txt