可逆言語Janus、そして最近のソフトウェアと可逆システム
Section: Technology
Tags: Reversible computing
Contents
可逆計算に興味を持ったきっかけ
可逆プログラミング言語 Janus
データ型
変数
グローバル変数
ローカル変数
演算
条件分岐
ループ
プロシージャ
可逆とは
最近の研究
Introduction
Behavioural Types
セッション型
振舞いコントラクト
Recovery
Reversibility and Object-Oriented Languages
Joule
ROOPL
Reversing Imperative Concurrent Programs
Reversible Debugger for Message Passing Systems
Control Theory
Conclusions
参考文献

可逆計算に興味を持ったきっかけ

私は、楽器やメロディーなどの曲に関する様々な情報が失われていない汎用的な音声フォーマットでは、どの情報をどの形式で保持するべきかについて研究しております。

その中で可逆計算を用いることで、２つのメリットを得られるのではないかと考えております。

  • リアルタイムで大規模な計算を行わないといけない課題に対して、まず事前に出力を用意しておき、リアルタイムで入力が変化した際に、必要となる計算が出力に近い場合は、従来のように始めから計算するのではなく、出力から逆計算を行うことで計算量を減らすことができる
  • 録音に類似したもの（出力）から重要な情報（入力）を取得できる可能性を秘めている

そのため私は現在可逆計算について調べており、これから最近の研究について説明します。

ただその前に、可逆とはどういうことなのかを可逆プログラミング言語についての具体的な説明をすることで、理解してもらおうと思います。

可逆プログラミング言語 Janus

Janus （読み方はわからない「じぇいなす」、「じゃあなす」、「やぬす」）とは、1982 年に Howard Derby と Christopher Lutz によって書かれた命令型の時間-可逆プログラミング言語1です。

現在では様々な拡張機能が提案されています。 これからは Janus86 を拡張した Michael Kirkedal Thomsen が管理しているインタプリタに基づいて説明していきます。

実際に実行するときにはインストールや会員登録等が不要な、コペンハーゲン大学が運営しているJanus のオンラインインタープリタを利用することをおすすめします。

データ型

Janus の型は、整数型とその配列のみあります。つまり浮動小数点数や構造体などは存在しません。

変数

また変数については、当初はグローバル変数のみ存在していたのですが、ローカル変数も作ることができます。

グローバル変数

グローバル変数は、mainプロシージャから定義されます。

procedure main()
  int natural[4] = {0, 1, 2, 3}
  // ...

グローバルな変数は、そのプログラムの入力や出力となり、重要な意味を持ちます。

ローカル変数

ローカル変数は、どのプロシージャでもlocalを用いて定義することができ、delocalするまで使用することができます。

procedure for_loop()
    local int i = 0
    // ...
    delocal int i = 0

グローバル変数とは違い、変数を開放する際には変数の値がdelocalで定義している値である必要があります。

ここが不可逆な言語との違いの一つです。変数が存在することの定義は行っても、変数を開放する際には値が何であるかまでは記述する必要がありませんでした。

そのため不可逆な言語では、基本的に上から順に実行されていきますが、下から順に実行することができません。

例えば、変数numに１を定義して、そこから更に２を足す C 言語のプログラムがあるとします。

void main() {
    int num = 1;
    num += 2
}

逆から実行しようとしても、その時点でnumの値がわからないためnum = ? + 2となり、未定義動作となってしまいます。

一方で Janus では、逆から実行する場合delocalが変数の定義になっており、実行することができます。

演算

先ほどの例には、演算を含んでいました。

Janus でも足し算のような演算を行うことができます。

procedure main()
    local int num = 1
    num += 2
    delocal int num = 3

逆から実行する場合は、変数numに３を定義しており、num -= 2をすることでnumが１となり、localで定義した値と一致します。

条件分岐

if文のような条件分岐も、fi条件を加えることで逆から実行できるようになります。

fi条件はif文を実行した後に判定され、その条件は真である必要があります。

例えば、ある数字が奇数の時には偶数に直すプログラムは、次のように書けます。

procedure to_even(int num, int odd)
    if (num % 2 = 1) then
        num += 1
        odd += 1
    fi odd = 1

procedure main()
    int num = 3
    int odd = 0
    call to_even(num, odd)

to_evenプロシージャを逆から実行する場合は、次のようになります。

    if even = 1 then
        even -= 1
        num -= 1
    fi num % 2 = 0

ループ

ifと同様に、条件が新たに加わります。

不可逆な言語のloopでは終了条件のみ記述していましたが、開始条件も加わります。

次の例は、1 から４までの値を足した総和を出力するプログラムです。

procedure add_until_five(int sum)
    local int i = 1
    from (i = 1) loop
        sum += i
        i += 1
    until (i = 5)
    delocal int i = 5

procedure main()
    int sum = 0
    call add_until_five(sum)

プロシージャ

Janus には関数はなく、プロシージャのみ存在し、上記していたように定義します。

callで呼び出すだけでなく、uncallで逆から実行することもできます。

条件分岐で例に挙げた奇数の場合偶数にするプログラムをcallした後にuncallすると、元の変数の値に戻ります。

procedure to_even(int num, int odd)
    if (num % 2 = 1) then
        num += 1
        odd += 1
    fi odd = 1

procedure main()
    int num = 3
    int odd = 0
    call to_even(num, odd)
    uncall to_even(num, odd)

可逆とは

このように可逆プログラミング言語では、逆からもプログラムを実行することができます。

プログラミングパラダイムや言語の水準などの分類ごとに、可逆を保証する範囲が違うので、具体的な定義については控えます。

最近の研究

それでは近年の可逆計算のソフトウェア周りの研究について、説明していきます。

具体的な内容としては、Janus の研究に携わっていらっしゃる横山先生にご連絡させていただき、その際にご紹介いただいた論文[2]2を引用しつつ補足を中心に紹介していきます。

またこれ以降では、この分野について学習中の私が論文の補足、そして引用を解釈し翻訳するので、間違えている所があればご教授ください。

この論文では、

  1. Introduction
  2. Behavioural Types
  3. Recovery
  4. Reversibility and Object-Oriented Languages
    1. Object Orientation and Data Structures
  5. Reversing Imperative Concurrent Programs
    1. Language and Program State
    2. Annotation, Inversion and Operational Semantics
  6. Reversible Debugger for Message Passing Systems
  7. Control Theory
  8. Conclusions

から成り立っています。

We survey the breadth of topics and recent activities on reversible software and systems including behavioural types, recovery, debugging, concurrency, and object-oriented programming.

総説論文であるため、それぞれ調査した内容の概要がまとめられており、それぞれの詳しい説明はあまり書かれておらず、技術などを理解するには論文を参照していかなければなりません。

応用的なソフトウェアの説明があるのだと思っていたのですが、実際には言語周りの内容が多く書かれていました。

それでは順番に軽く解説していきます。

Introduction

序論ではまず可逆計算の歴史について、説明しています。

次に、

ソフトウェアは可逆計算においてあらゆる面で中心的な役割をもっている。

と書かれており、ソフトウェアの重要性を訴えています。

これから説明する内容は、

より安全で信頼性の高い可逆的コンピューティングアプリケーションにつながる言語的抽象化とツールを提供する可能性を持っている。

と説明しています。

Behavioural Types

この章では、Behavioural Typesと可逆性について説明しています。

Behavioural Typesは直訳で振舞い型なのですが、調べてみても振舞い型という単語が出ている日本語の論文を見つけられませんでした。

正しい翻訳ではないかもしれませんが、ここでは振舞い型と呼ぶことにします。

論文[3]3によると、 振舞い型システムは「並列計算や分散計算に関連し、従来の入出力操作に加えて、インタフェース、通信プロトコル、コントラクトなどの概念を包含しており」、 ソフトウェアコンポーネントの振舞い型は「表現力豊かな型言語を用いて、期待される相互作用のパターンを指定しており」、 振る舞い型に関連する重要な概念として、「セッション型と振舞い型コントラクトがある」 と説明しています。

セッション型

イメージしにくかったので、まずセッション型の具体例で補足します。

上記の意味の「表現力豊かな型言語」に当てはまるであろう Rust にもセッション型のクレートが存在します。

そのサンプル4として、以下のように書けます。

extern crate session_types;
use session_types::*;
use std::thread;

type Server = Recv<i64, Send<bool, Eps>>;
type Client = <Server as HasDual>::Dual;

fn srv(c: Chan<(), Server>) {
    let (c, n) = c.recv();
    if n % 2 == 0 {
        c.send(true).close()
    } else {
        c.send(false).close()
    }
}

fn cli(c: Chan<(), Client>) {
    let n = 42;
    let c = c.send(n);
    let (c, b) = c.recv();

    if b {
        println!("{} is even", n);
    } else {
        println!("{} is odd", n);
    }

    c.close();
}

fn main() {
    let (server_chan, client_chan) = session_channel();

    let srv_t = thread::spawn(move || srv(server_chan));
    let cli_t = thread::spawn(move || cli(client_chan));

    let _ = (srv_t.join(), cli_t.join());
}

一見、普通の通信プロトコルであるように感じます。

しかしプロジェクトの説明4によると、「通信する 2 つのプロセスがその共有通信プロトコルを遵守しているかどうかを静的にチェックすることができるところ」が他と違います。

またセッション型を実装するには、「プロトコルの特定のアクションが行われたことをモデル化する方法が必要であるが、Rust ではムーブセマンティクスを用いることで、プロトコルのアクションが繰り返されないことを簡単に保証すること」ができます。

それでは、可逆性との関係についての話に入ります。

バイナリセッション型とマルチパーティセッション型では、それぞれモニタ機構の工夫や情報を追加することで可逆性を実現しています。

振舞いコントラクト

また振舞いコントラクト5とは、

  • クライアントとサーバーが相互作用する際に、期待される通信パターンを抽象的に記述したもの
  • コンプライアンスという概念を自然に備えている
    • クライアントとサーバーがコンプライアンスに準拠したコントラクトに従うとき、その相互作用は進行するか正常に完了することが保証される

と記述されています。

バックトラックを扱う取り消し可能なコントラクトと、推測的実行を扱う推論のコントラクトの 2 つの拡張が研究[5]5されており、同じコンプライアンスの概念をもたらします。

Recovery

分散プログラムは、オープンであること、スケーラブルであること、長時間動作すること、障害に対して寛容であることなどが要求される6ため、複雑になり安定した動作を行うことが難しいです。

そのため、

実行を監視するための適切な戦略を採用し、分散プログラムをより柔軟かつ堅牢にするための回復および適応メカニズムを組み込む必要がある。

しかし、

現在採用されている典型的なアプローチは、そのようなメカニズムをプログラムロジックに埋め込むことであり、抽出、比較、デバッグが困難である

と記述されています。

[6]6では、障害回復・適応策の設計に形式的な抽象化を用いるアプローチが提案されており、この抽象化は実装にとらわれないが、コード、監視、テストのアルゴリズム統合に適しています。

具体的には、学術界と産業界の両方で勢いを増しているメッセージパッシングプログラム（Erlang、Go、MPI など）で検討しています。

また[6]の実例7や、マルチパーティセッション型との統合8、共有メモリをもつ言語の因果一貫可逆性の概念に基づくロールバック演算子が定義9などの研究があります。

Reversibility and Object-Oriented Languages

本章と次章では、具体的なプログラミングパラダイムと可逆性について説明しています。

本章では、可逆性を持つオブジェクト指向プログラミングについて紹介しています。特に Joule10と ROOPL11の２つの言語を用いて説明しています。

特に可逆プログラミングは処理を書くのに従来より煩雑になるが、オブジェクト指向により、複雑な処理をまとめることができて、比較的簡単になるようになるみたいなことが書かれています。

Joule

Joule は、Janus をオブジェクト指向言語にした感じです。

レポジトリに、いくつかの Joule のプログラム とそれをコンパイルした Janus のプログラムが公開されています。

対応しているソースコードを見ることで、どのようにして実現されているか理解することができます。

以下はプログラム例です。

/*
Copyright (c) 2017, Ulrik Pagh Schultz, University of Southern Denmark
All rights reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:

1. Redistributions of source code must retain the above copyright notice, this
   list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright notice,
   this list of conditions and the following disclaimer in the documentation
   and/or other materials provided with the distribution.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR
ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

The views and conclusions contained in the software and documentation are those
of the authors and should not be interpreted as representing official policies,
either expressed or implied, of the University of Southern Denmark.
*/

abstract class Operator { // Defines an abstract interface
  abstract procedure apply(int var, int value);
}
class Add extends Operator {
  procedure apply(int var, int value) { var += value; }
}
class Sub extends Operator {
  procedure apply(int var, int value) { var -= value; }
}
class Twice extends Operator {
  &Operator op;
  Twice(&Operator op) { this.op := op; } // := only on null references
  procedure apply(int var, int value) {
    local &Operator op = this.op; // copy of reference, fewer indirections
    op.apply(var,value); op.apply(var,value); // Polymorphic call site
    delocal op == this.op;
  }
}
main twice[10] {
  local &Operator a = &Add.new(); local &Operator b = &Sub.new();
  local &Operator aa = &Twice.new(a); local &Operator bb = &Twice.new(b);
  local int x = 0;
  aa.apply(x,4); bb!apply(x,1);
  delocal x == 10;
  delocal &Twice!new(b) bb; delocal &Twice!new(a) aa;
  delocal &Sub!new() b; delocal &Add!new() a;
}

抽象abstractや継承extendsのような一般的なオブジェクト指向に実装されているものも実装されています。

最後から 4 行目はなぜdelocal x == 6;ではないのか疑問に思っています。

ROOPL

ROOPL にもレポジトリがあります。

以下はプログラム例12です。

class Node //Represents a single node in the list
    int data
    Node next //Reference to next node in the list
    //Constructor method
    method constructor(int d, Node n)
        data ^= d
        next <=> n
    //Accessor & mutator methods
    method add(int out)
        out += data
    method sub(int out)
        out -= data
    method xor(int out)
        out ^= data
    method swap(int out)
        out <=> data
    method swapNext(Node out)
        out <=> next

class Iterator //Iterator interface
    int result
    //Abstract method
    method run(Node head, Node next)
        skip
    //Accessor
    method get(int out)
        out <=> result

class ListBuilder
    int n //The length of the list to build
    Iterator it //The iterator instance to run
    Node empty //Helper node
    //Constructor method
    method constructor(int len, Iterator i)
        n += len
        it <=> i
    method build(Node head)
        if n = 0 then
            if head != nil then
                call it::run(head, empty) //List is done, run the iterator
            else skip
            fi head != nil
        else
            //Not yet done, construct next node
            construct Node next
                call next::constructor(n, head)
                n -= 1
                call build(next)
                n += 1
                uncall next::constructor(n, head)
            destruct next
        fi n = 0

class Sum inherits Iterator
    int sum
    method run(Node head, Node next)
        call head::add(sum)
        call head::swapNext(next)
        if next = nil then
            result += sum //Finished
        else
            call run(next, head) //More work to do
        fi next = nil
        uncall head::swapNext(next) //Return list to original state
        uncall head::add(sum)

class Program
    int result //Final result
    Node empty //Helper node
    method main()
        local int n = 5 //List length
        construct Sum it //Construct iterator
            construct ListBuilder lb //Construct list builder
                call lb::constructor(n, it)
                call lb::build(empty) //Build & iterate
                uncall lb::constructor(n, it)
            destruct lb
            call it::get(result) //Fetch result
        destruct it
        delocal n = 5

また ROOPL をさらに拡張したROOPL++というものも存在します。

Reversing Imperative Concurrent Programs

命令型言語の可逆化は長年研究されているが、その正しさについては欠落していることが多く、証明についての論文が増えていると書かれています。

まず第１節では可逆にするために必要なこと、第２節では更に並列処理ではどのようものが必要かについて述べられています。

そして第３,4 節では、正しさの証明について書かれています。

第５節では、可逆性がデバッグにも役に立つことを示しています。

Reversible Debugger for Message Passing Systems

WG2 の関連する研究スレッドでは、いわゆる因果一貫性（causal-consistent）アプローチを使用して、並行メッセージパッシング・アプリケーションのデバッグの問題に取り組んでいると書かれています。

Control Theory

可逆制御の課題は、不可逆な制御対象との相互作用であり、制御対象が可逆的であっても（例えば流体の運動）、それを反転させる能力は制御できないことが多い13です。

2 つの異なる現実的な例として、1 つは大規模アンテナアレイにおけるリソース管理、もう 1 つは水中音響通信における波の時間反転を通して、無線通信の応用設定における可逆制御の要素を探っています14。

前者では、可逆ペトリネットに基づく大型高周波アンテナアレイの新しい分散最適化手法の提案をしています。そして後者では、水中音響通信のための可逆的なハードウェアアーキテクチャの開発を行っています。

Conclusions

最後に結論では、「可逆性と回復パターンと呼ばれるものの相互作用は、さらに調査される価値があり、ソフトウェア開発における可逆性の統合は、まだ初期段階にある」と記述されています。

参考文献

Footnotes

  1. Christopher Lutz. Janus: a time-reversible language. 1986. Letter to R. Landauer. http://tetsuo.jp/ref/janus.html ↩

  2. Mezzina, C.A. et al. (2020). Software and Reversible Systems: A Survey of Recent Activities. In: Ulidowski, I., Lanese, I., Schultz, U., Ferreira, C. (eds) Reversible Computation: Extending Horizons of Computing. RC 2020. Lecture Notes in Computer Science(), vol 12070. Springer, Cham. https://doi.org/10.1007/978-3-030-47361-7_2 ↩

  3. Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. 2016. Foundations of Session Types and Behavioural Contracts. ACM Comput. Surv. 49, 1, Article 3 (March 2017), 36 pages. https://doi.org/10.1145/2873052 ↩

  4. session-types, Copyright (c) 2015 Thomas Bracht Laumann Jespersen, Philip Munksgaard, Released under the MIT license. see https://opensource.org/licenses/MIT ↩ ↩2

  5. Franco Barbanera, Ivan Lanese, Ugo de'Liguoro, A theory of retractable and speculative contracts, Science of Computer Programming, Volume 167, 2018, Pages 25-50, ISSN 0167-6423, https://doi.org/10.1016/j.scico.2018.06.005 ↩ ↩2

  6. Cassar, I., Francalanza, A., Mezzina, C.A., Tuosto, E.: Reliability and fault-tolerance by choreographic design. In: Francalanza, A., Pace, G.J. (eds.) Proceedings Second International Workshop on Pre- and Post-Deployment Verification Techniques, PrePost@iFM 2017. EPTCS, vol. 254, pp. 69–80 (2017) ↩ ↩2

  7. Francalanza, A., Mezzina, C.A., Tuosto, E.: Reversible choreographies via monitoring in Erlang. In: Bonomi, S., Rivière, E. (eds.) DAIS 2018. LNCS, vol. 10853, pp. 75–92. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-93767-0_6 ↩

  8. Neykova, R., Yoshida, N.: Let it recover: multiparty protocol-induced recovery. In: 26th International Conference on Compiler Construction, pp. 98–108. ACM (2017) ↩

  9. Giachino, E., Lanese, I., Mezzina, C.A., Tiezzi, F.: Causal-consistent rollback in a tuple-based language. J. Log. Algebr. Methods Program. 88, 99–120 (2017) ↩

  10. Schultz, U.P., Axelsen, H.B.: Elements of a reversible object-oriented language. In: Devitt, S., Lanese, I. (eds.) RC 2016. LNCS, vol. 9720, pp. 153–159. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40578-0_10 ↩

  11. Haulund, T., Mogensen, T.Æ., Glück, R.: Implementing reversible object-oriented language features on reversible machines. In: Phillips, I., Rahaman, H. (eds.) RC 2017. LNCS, vol. 10301, pp. 66–73. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-59936-6_5 ↩

  12. TueHaulund / ROOPLC, Copyright (c) 2016 , Released under the MIT license. see https://opensource.org/licenses/MIT ↩

  13. Siljak, H.: Reversibility in space, time, and computation: the case of underwater acoustic communications. In: Kari, J., Ulidowski, I. (eds.) RC 2018. LNCS, vol. 11106, pp. 346–352. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99498-7_25 ↩

  14. Siljak, H.: Reversible computation in wireless communications. In: Ferreira, C., Lanese, I., Schultz, U., Ulidowski, I. (eds.) Reversible Computation: Theory and Applications. LNCS, vol. 12070. Springer, Heidelberg (2020) ↩